Modelo de atacante Dolev-Yao y criptografía simbólica

Propuesto por Danny Dolev y Andrew Yao en 1983, el modelo de Dolev-Yao es el modelo de adversario estándar para el análisis simbólico de protocolos. El atacante controla toda la red.

El atacante de Dolev-Yao puede: interceptar cualquier mensaje, almacenar mensajes, repetir mensajes antiguos y falsificar mensajes nuevos a partir de componentes conocidos, pero no puede romper las primitivas criptográficas subyacentes.

En los modelos simbólicos, el cifrado es una caja negra perfecta: el atacante no puede descifrar sin la clave, factorizar números grandes ni falsificar firmas. Esto simplifica el análisis, pero puede pasar por alto ataques en el nivel de implementación.

Los mensajes se modelan como términos: enc(k, m), sig(sk, m), hash(m), pair(a, b). El atacante conoce ciertos términos y deriva otros nuevos mediante reglas definidas (reglas de deducción).

El conocimiento del atacante es cerrado con respecto a la deducción: si conoce enc(k,m) y k, puede derivar m. Si conoce pair(a,b), puede derivar a y b. El cierre del conocimiento inicial = todo lo que el atacante puede aprender.

La seguridad del protocolo se expresa así: "el conocimiento del atacante nunca contiene el secreto s en ningún estado alcanzable". Confidencialidad = alcanzabilidad. Autenticación = ausencia de ciertos patrones de trazas problemáticos.

Protocolo entre dos partes: A→B: {Na, A}_{K_B}; B→A: {Na, Nb}_{K_A}; A→B: {Nb}_{K_B}. En álgebra de términos: Alice envía enc(pubkey_B, pair(Na, A)). Verificamos que, tras la ejecución, solo B conoce Na.

El cálculo pi aplicado (Abadi & Fournet 2001) es un álgebra de procesos para modelar protocolos. Los procesos se comunican a través de canales; el atacante controla los canales públicos. ProVerif y Tamarin utilizan este formalismo.

Un protocolo que es seguro en el modelo de Dolev-Yao aún puede ser inseguro desde el punto de vista computacional si la instanciación criptográfica es débil. El teorema de solidez computacional (Cortier et al.) cierra la brecha para clases específicas de primitivas.

Dolev-Yao no puede modelar: propiedades algebraicas (p. ej., la conmutatividad de XOR), ataques de canal lateral, errores de implementación ni fallos probabilísticos. Las extensiones, como el modelo de teoría ecuacional, permiten tratar algunas propiedades algebraicas.

¿Qué capacidad NO tiene el atacante de Dolev-Yao?

Dolev-Yao proporciona al atacante control total de la red, pero supone una criptografía perfecta. Los mensajes son términos de un álgebra; la seguridad es una propiedad de alcanzabilidad. El cálculo pi aplicado proporciona el lenguaje formal. Limitaciones: no puede modelar relaciones algebraicas, canales laterales ni errores de implementación.