El protocolo Needham-Schroeder y sus ataques

El protocolo Needham-Schroeder (1978) fue uno de los primeros intentos formales de diseñar un protocolo de autenticación criptográfica utilizando un tercero de confianza (TTP). El objetivo era permitir que dos partes, Alice y Bob, se autenticaran mutuamente y establecieran una clave de sesión compartida mediante un servidor de autenticación (AS) de confianza que compartiera claves de larga duración con cada principal. El protocolo es anterior a la infraestructura de clave pública, pero introdujo conceptos —nonces para garantizar la frescura y distribución de claves mediante un servidor de confianza— que siguen siendo fundamentales en protocolos modernos como Kerberos. La comprensión de NS y de sus fallos dio forma a todo el campo del análisis de protocolos.

El protocolo de clave simétrica NS consta de cinco pasos. (1) Alice envía {A, B, Na} al AS para solicitar una clave de sesión con la que comunicarse con Bob. (2) El AS responde a Alice con {Na, B, Kab, {Kab, A}_Kb}_Ka: una clave de sesión Kab y un ticket para Bob, todo cifrado con la clave de larga duración de Alice, Ka. (3) Alice reenvía a Bob el ticket {Kab, A}_Kb. (4) Bob descifra el ticket, extrae Kab y envía {Nb}_Kab a Alice como desafío. (5) Alice responde {Nb-1}_Kab para demostrar que posee Kab. El nonce Nb evita la repetición del paso 4. Este protocolo presenta un ataque de replay conocido, explotado por Denning y Sacco (1981).

Denning y Sacco (1981) descubrieron un fallo: la respuesta del AS en el paso 2 no es fresca, ya que no contiene una marca de tiempo ni un nonce aportado por el servidor. Un atacante, Mallory, que hubiera interceptado anteriormente una clave de sesión Kab antigua (al comprometer una sesión pasada), puede repetir el ticket antiguo {Kab, A}_Kb ante Bob en cualquier momento futuro. Bob, al recibir lo que parece un ticket legítimo de Alice, utiliza la clave comprometida Kab para la sesión. La solución de Denning y Sacco consiste en añadir una marca de tiempo a la respuesta del AS y al ticket. Esta solución se adoptó en Kerberos: las marcas de tiempo se incluyen en los tickets para limitar su periodo de validez.

El protocolo de clave pública NS (también de 1978) se diseñó para la autenticación mutua entre dos partes mediante criptografía de clave pública. (1) Alice envía {Na, A}_PKb a Bob (el nonce Na cifrado con la clave pública de Bob). (2) Bob responde {Na, Nb}_PKa (ambos nonces cifrados con la clave pública de Alice). (3) Alice responde {Nb}_PKb (devuelve el nonce de Bob cifrado con su clave pública). Tras este intercambio, ambas partes poseen los dos nonces (Na, Nb) y pueden derivar una clave de sesión. El protocolo pareció seguro durante 17 años, hasta el ataque de Lowe de 1995.

Gavin Lowe (1995) descubrió un fallo crítico utilizando el model checker Failures in Compositional Reasoning (FDR). Mallory puede suplantar a Bob ante Alice mientras retransmite los mensajes a un Bob honesto. Paso 1: Alice envía {Na, A}_PKm a Mallory, creyendo que habla con Bob. Mallory reenvía {Na, A}_PKb a Bob. Paso 2: Bob responde {Na, Nb}_PKa, que Mallory descifra y vuelve a cifrar para Alice: {Na, Nb}_PKa. Alice lo descifra y extrae Nb. Paso 3: Alice envía {Nb}_PKm, creyendo que se lo envía a Bob. Mallory lo descifra y reenvía {Nb}_PKb a Bob. Bob cree que ha completado una autenticación mutua con Alice, pero Alice en realidad se está autenticando con Mallory. La solución consiste en que, en el paso 2, Bob incluya su propia identidad: {Na, Nb, B}_PKa.

La solución de Lowe para el protocolo NSPK es simple, pero profunda: la respuesta de Bob en el paso 2 debe incluir la identidad B de Bob, de modo que sea {Na, Nb, B}_PKa. Ahora, cuando Alice recibe la respuesta, comprueba que la identidad incluida B coincide con la parte con la que pretendía comunicarse. Mallory no puede sustituir su propia respuesta, ya que necesitaría la clave privada de Alice para construir un mensaje válido {Na, Nb, M}_PKa que supere la comprobación de Alice. Esta lección se generaliza como el principio de Needham-Abadi: los mensajes de autenticación deben vincular explícitamente la identidad del emisor, en lugar de depender únicamente del contexto para identificarlo.

El descubrimiento de la vulnerabilidad de NSPK por parte de Lowe se vio facilitado por el verificador de modelos FDR (Failures-Divergences Refinement), que explora exhaustivamente todas las ejecuciones posibles del protocolo, incluidas las intervenciones de adversarios. Esto impulsó el desarrollo de herramientas de análisis formal de protocolos: Proverif, basado en el cálculo pi aplicado, puede demostrar o refutar propiedades de autenticación y secreto en un número infinito de sesiones. Tamarin Prover utiliza reescritura de multiconjuntos y admite protocolos complejos como TLS 1.3 y Signal. AVISPA y Scyther son otras herramientas. Los diseños de protocolos modernos, como TLS 1.3, Signal y Noise, se someten a verificación formal antes de su implementación, un legado directo del episodio de NS/Lowe.

Los ataques contra NS aclararon la distinción entre los objetivos de autenticación. La autenticación de entidad consiste en demostrar que una parte está activa actualmente y participa en el protocolo; la frescura es importante. La autenticación del origen de los datos consiste en demostrar que un mensaje específico fue creado por una parte específica, pero no implica necesariamente que esta siga activa. El ataque de Lowe compromete la autenticación de entidad: Alice cree que se está autenticando con Bob, pero en realidad se está autenticando con Mallory, quien retransmite los mensajes a Bob. Las especificaciones modernas de protocolos expresan los objetivos con precisión: "Alice está autenticada ante Bob como la iniciadora de esta sesión". Los objetivos imprecisos producen especificaciones ambiguas que superan una revisión informal, pero fallan en el análisis formal.

Otra clase de ataques relacionados con NS son los ataques de reflexión: Mallory reenvía a Alice los mensajes que Alice le envió. Si el protocolo es simétrico, es decir, si ambas partes utilizan la misma clave y el mismo formato de mensaje, Alice puede aceptar su propio desafío como una respuesta válida de Bob. Para defenderse, se pueden utilizar direcciones de clave diferentes, con claves de cifrado y descifrado separadas para cada dirección, o incluir indicadores de rol en los mensajes; por ejemplo, el cifrador incluye "I am initiator" en el mensaje. Los protocolos modernos como TLS incluyen cadenas de etiquetas específicas del rol en las claves derivadas mediante HKDF, utilizando "c e traffic" para el cliente y "s hs traffic" para el servidor, con el fin de evitar la reflexión.

Los ataques de entrelazado combinan mensajes de varias sesiones de protocolo simultáneas para falsificar la autenticación. Si Alice ejecuta dos sesiones al mismo tiempo, Mallory puede mezclar mensajes de ambas para crear una sesión combinada coherente, pero no válida, que autentique a Mallory. La defensa es la vinculación de sesión: cada mensaje debe quedar vinculado criptográficamente al contexto de su sesión, por ejemplo, incluyendo un identificador de sesión o utilizando una clave única por sesión. TLS evita el entrelazado mediante el mensaje Finished, que contiene un MAC calculado sobre la transcripción completa de la sesión actual. Cualquier mensaje entrelazado modifica la transcripción e invalida el valor de Finished.

Los protocolos Needham-Schroeder influyeron directamente en el diseño de Kerberos, mediante las marcas de tiempo para evitar repeticiones, tomadas de la solución de Denning-Sacco; en TLS, cuyo MAC de transcripción del mensaje Finished evita el entrelazado y la reflexión; en Signal Protocol, mediante la vinculación de sesión a través del estado del ratchet; y en Noise Protocol Framework, mediante la vinculación de identidad en los patrones de handshake. Los ataques contra NS demostraron que los argumentos informales de seguridad son insuficientes: cada protocolo debe analizarse frente a un adversario activo que controla la red y puede repetir, reordenar y modificar mensajes. Este modelo de adversario, conocido como Dolev-Yao, es ahora estándar en la verificación formal de protocolos.

¿Qué cambio sencillo propuso Lowe para corregir la vulnerabilidad del protocolo de clave pública NS?

El protocolo simétrico Needham-Schroeder (1978) introdujo la distribución de claves de sesión basada en un TTP. El ataque de Denning-Sacco (1981) descubrió una vulnerabilidad de repetición, que se corrigió mediante marcas de tiempo en Kerberos. El protocolo de clave pública NSPK sufrió un ataque MITM descubierto por Lowe (1995) mediante la verificación de modelos, que se corrigió incluyendo la identidad del emisor en los mensajes. Estos ataques establecieron la verificación formal, con herramientas como Proverif y Tamarin, como un elemento esencial del diseño de protocolos. Lecciones clave: los mensajes deben vincular la identidad del emisor, las sesiones deben aislarse unas de otras, los ataques de reflexión se evitan mediante la derivación direccional de claves y los ataques de entrelazado se evitan mediante MAC de transcripción.