Por qué las demostraciones informales no bastan

Los diseñadores de protocolos producen habitualmente argumentos informales de seguridad: razonamientos en prosa sobre por qué un atacante no puede tener éxito. La historia demuestra que estos argumentos suelen ser erróneos, incluso cuando los diseñan expertos.

Needham-Schroeder (1978) se diseñó para la autenticación mutua. En 1995, Gavin Lowe descubrió un ataque de intermediario mediante verificación automatizada, 17 años después de su publicación. La prueba informal no detectó una sutil repetición.

El IEEE aprobó WEP en 1997 con afirmaciones informales de seguridad. En 2001, los investigadores descubrieron la reutilización del flujo de claves RC4, colisiones de IV y ausencia de integridad, lo que permitió romperlo en cuestión de minutos. El razonamiento informal no detectó nada de esto.

La seguridad de los protocolos depende de las interacciones entre muchas sesiones simultáneas, atacantes activos y supuestos criptográficos. El razonamiento humano tiene dificultades con la explosión del espacio de estados y las ejecuciones simultáneas entrelazadas.

Los métodos formales modelan matemáticamente el protocolo y demuestran o refutan propiedades de seguridad (secreto, autenticación y secreto directo) para todas las estrategias posibles del atacante, no solo para las que el diseñador tuvo en cuenta.

Simbólico (Dolev-Yao): la criptografía es una caja negra perfecta; el enfoque se centra en la lógica del protocolo. Computacional: juegos de seguridad probabilísticos reales, más cercanos a las garantías del mundo real. Ambos detectan errores reales.

POODLE (2014) explotó un oráculo de relleno en CBC de SSL 3.0. La vulnerabilidad era un fallo de diseño a nivel de protocolo, no un error de implementación. El análisis formal de la especificación de SSL 3.0 habría señalado el oráculo antes de su implementación.

TLS 1.3 (RFC 8446) se diseñó junto con análisis formales mediante ProVerif y miTLS. La especificación se iteró a partir de los resultados formales, un hito en la adopción de métodos formales por parte de los organismos de estandarización.

Las herramientas formales verifican el modelo del protocolo, no la implementación. Un protocolo verificado formalmente aún puede tener una implementación insegura. F* / HACL* amplía la verificación al propio código criptográfico.

La verificación formal es costosa: modelar un protocolo requiere semanas y conocimientos especializados. Sin embargo, para objetivos de gran valor (TLS, SSH y Signal), el coste está justificado: un solo fallo de protocolo puede afectar a miles de millones de usuarios.

¿Qué hizo significativa la revelación de Lowe en 1995 sobre el ataque a Needham-Schroeder?

Las pruebas informales fallan porque el razonamiento humano no detecta las interacciones entre sesiones simultáneas ni las estrategias de los atacantes. Needham-Schroeder, WEP y POODLE tenían argumentos informales de seguridad. TLS 1.3 incorporó análisis formal durante su diseño. Las herramientas formales detectan errores a nivel de protocolo antes de su implementación.