Verificación formal con Lean: demuestra la corrección del One-Time Pad
Introduction to Formal Verification with Lean Part 1
En este tutorial práctico, aprenderás los fundamentos de Lean, un asistente de pruebas y lenguaje de programación funcional, mientras verificas formalmente el protocolo One-Time Pad (OTP). El autor, ingeniero criptográfico, te guía paso a paso: desde definir bitstrings y la operación XOR hasta probar sus propiedades (conmutatividad, asociatividad, elemento identidad, auto-inversa) y demostrar que OTP es un cifrado de Shannon según las definiciones de Boneh y Shoup. Ideal para quienes se inician en verificación formal aplicada a criptografía.
Si la prueba es compilada por Lean, eso significa que es correcta (asumiendo confianza en el compilador de Lean).