ProVerif: verificación automatizada de protocolos
Especifique y verifique con ProVerif las propiedades del handshake de TLS.
ProVerif: verificación automatizada de protocolos es una lección gratuita de Cryptology Academy en CoddyKit. Esta es la lección 3 de 4. Puedes leer la lección completa abajo gratuitamente — luego la practicas en el navegador con un editor de código integrado y un tutor de IA 24/7. Forma parte de la ruta de aprendizaje de Cryptology Academy, y tu progreso se sincroniza en la web y la app de CoddyKit. El curso de Cryptology Academy incluye 4 lecciones en total.
¿Qué es ProVerif?
ProVerif (Bruno Blanchet, 2001) es un verificador automatizado de protocolos criptográficos. Recibe un protocolo descrito en cálculo pi aplicado y decide automáticamente las propiedades de confidencialidad y autenticación.
Cómo funciona ProVerif
ProVerif traduce el protocolo a cláusulas de Horn y aplica un algoritmo basado en resolución para deducir qué puede aprender el atacante. Si se puede derivar un hecho de confidencialidad, el protocolo está comprometido; de lo contrario, se demuestra que es seguro.
Lenguaje de entrada de ProVerif
Los protocolos se describen de forma declarativa: se declaran canales, tipos, funciones (enc, dec, sign, verify), ecuaciones (dec(enc(m,k),k)=m) y procesos que se comunican a través de canales.
Declaración de primitivas criptográficas
Ejemplo de declaraciones de ProVerif:
(* Symmetric encryption *)
fun senc(bitstring, key): bitstring.
fun sdec(bitstring, key): bitstring.
equation forall m: bitstring, k: key; sdec(senc(m, k), k) = m.
(* Asymmetric encryption *)
fun pk(skey): pkey.
fun aenc(bitstring, pkey): bitstring.
fun adec(bitstring, skey): bitstring.
equation forall m: bitstring, sk: skey; adec(aenc(m, pk(sk)), sk) = m.Escritura de un proceso de protocolo sencillo
Modele a Alice y Bob como procesos paralelos:
(* Alice sends nonce to Bob, encrypted *)
let Alice(skA: skey, pkB: pkey) =
new na: nonce;
out(c, aenc((na, pk(skA)), pkB));
in(c, m: bitstring);
let nb = adec(m, skA) in
out(c, aenc(nb, pkB)).
(* Main process: run attacker with full channel control *)
process
new skA: skey; new skB: skey;
out(c, pk(skA)); out(c, pk(skB)); (* publish public keys *)
(Alice(skA, pk(skB)) | Bob(skB, pk(skA)))Especificación de consultas de seguridad
ProVerif comprueba consultas como:
(* Secrecy: attacker cannot learn na *)
query attacker(na).
(* Authentication: if Bob completes, Alice started *)
query event(BobFinished(nb)) ==> event(AliceStarted(nb)).Interpretación de los resultados de ProVerif
ProVerif muestra "RESULT ... is true" (seguridad demostrada) o "RESULT ... is false" e imprime una traza de ataque a modo de contraejemplo que muestra los mensajes del atacante. La traza muestra exactamente cómo funciona el ataque.
Verificación de TLS 1.3 con ProVerif
Bhargavan et al. (2016) utilizaron ProVerif para analizar un modelo de TLS 1.3. Encontraron y documentaron un ataque contra el mecanismo de reanudación 0-RTT, que se solucionó antes de finalizar el RFC.
Limitaciones: aproximación y bucles
ProVerif calcula una sobreaproximación: puede informar de ataques falsos (decir "false" cuando el protocolo es realmente seguro), pero nunca omite ataques reales. Las sesiones de protocolo no acotadas pueden no terminar; ProVerif desenrolla los bucles heurísticamente.
Cuando ProVerif indica "Cannot Be Proved"
Si ProVerif no puede determinar el resultado dentro de su aproximación, muestra "CANNOT BE PROVED." Esto no constituye una demostración de inseguridad: significa que la herramienta agotó su capacidad heurística. Tamarin puede resolver estos casos.
Comprobación de conocimientos
¿Qué significa que ProVerif muestre "RESULT ... is false" para una consulta de confidencialidad?
Resumen de la lección
ProVerif automatiza la verificación de protocolos mediante resolución de cláusulas de Horn. Los protocolos se escriben en cálculo pi aplicado con ecuaciones criptográficas. Las consultas plantean preguntas sobre confidencialidad y autenticación. False significa que se ha demostrado la seguridad; true significa que el protocolo está comprometido (con una traza de ataque). Limitaciones: las aproximaciones pueden producir el resultado "cannot be proved."
Aprende Cryptology Academy con un tutor de IA — gratis
Escribe y ejecuta código real en tu navegador, obtén ayuda instantánea de un tutor de IA disponible 24/7 y continúa donde lo dejaste en la web o en la aplicación.
- Cursos
- 67
- Lecciones
- 261
Preguntas frecuentes
¿La lección «ProVerif: verificación automatizada de protocolos» es gratis?
Sí — el texto completo de «ProVerif: verificación automatizada de protocolos» es gratis para leer aquí en la web. Para practicarla de forma interactiva (editor de código integrado y tutor de IA 24/7) y desbloquear el resto del curso de Cryptology Academy, actualiza a CoddyKit PRO. El curso de Cryptology Academy incluye 4 lecciones en total.
¿Qué aprenderé en «ProVerif: verificación automatizada de protocolos»?
Especifique y verifique con ProVerif las propiedades del handshake de TLS. Practicas Cryptology Academy con código real que ejecutas directamente en el navegador, y un tutor de IA 24/7 responde tus preguntas mientras trabajas en la lección.
¿Necesito experiencia previa para empezar Cryptology Academy?
No se requiere experiencia previa. Cryptology Academy en CoddyKit está estructurado para principiantes hasta estudiantes avanzados, así que puedes empezar aquí o desde el inicio y avanzar a tu ritmo. Esta es la lección 3 de 4.
¿Cuánto tiempo toma la lección «ProVerif: verificación automatizada de protocolos»?
La mayoría de las lecciones de CoddyKit toman alrededor de 5–10 minutos. Cada una es compacta e interactiva, así que avanzas constantemente y retomas exactamente por donde dejaste en la web y la app.
¿Puedo escribir y ejecutar código en esta lección de Cryptology Academy?
Sí. Cada lección de Cryptology Academy incluye un editor de código integrado, así que escribes y ejecutas código real directamente en tu navegador y obtienes retroalimentación instantánea de IA — sin configuración local necesaria.
Todas las lecciones de este curso
- Por qué las demostraciones informales no bastan
- Modelo de atacante Dolev-Yao y criptografía simbólica
- ProVerif: verificación automatizada de protocolos
- Tamarin y demostraciones computacionales