El modelo Dolev-Yao , [1] llamado así por sus autores Danny Dolev y Andrew Yao , es un modelo formal utilizado para demostrar propiedades de protocolos criptográficos interactivos. [2] [3]
La red está representada por un conjunto de máquinas abstractas que pueden intercambiar mensajes. Estos mensajes están compuestos por términos formales. Estos términos revelan parte de la estructura interna de los mensajes, pero es de esperar que algunas partes permanezcan opacas para el adversario.
En este modelo, el adversario puede escuchar, interceptar y sintetizar cualquier mensaje y solo está limitado por las restricciones de los métodos criptográficos utilizados. En otras palabras: "el atacante lleva el mensaje".
Esta omnipotencia ha sido muy difícil de modelar, y muchos modelos de amenazas la simplifican, como se ha hecho para el atacante en la computación ubicua . [4]
Los primitivos criptográficos se modelan mediante operadores abstractos. Por ejemplo, el cifrado asimétrico para un usuario se representa mediante la función de cifrado y la función de descifrado . Sus principales propiedades son que su composición es la función de identidad ( ) y que un mensaje cifrado no revela nada sobre . A diferencia del mundo real, el adversario no puede manipular la representación de bits del cifrado ni adivinar la clave. Sin embargo, el atacante puede reutilizar cualquier mensaje que se haya enviado y, por lo tanto, se haya vuelto conocido. El atacante puede cifrarlos o descifrarlos con cualquier clave que conozca, para falsificar mensajes posteriores.
Un protocolo se modela como un conjunto de ejecuciones secuenciales, alternando entre consultas (envío de un mensaje a través de la red) y respuestas (obtención de un mensaje de la red).
La naturaleza simbólica del modelo Dolev-Yao lo hace más manejable que los modelos computacionales y accesible a los métodos algebraicos , pero potencialmente menos realista. Sin embargo, ambos tipos de modelos para protocolos criptográficos han sido relacionados. [5] Además, los modelos simbólicos son muy adecuados para mostrar que un protocolo está roto , en lugar de ser seguro, bajo los supuestos dados sobre las capacidades de los atacantes.
