Modelo Dolev – Yao
El modelo Dolev-Yao , [1] llamado así por sus autores Danny Dolev y Andrew Yao , es un modelo formal utilizado para probar las propiedades de los protocolos criptográficos interactivos. [2] [3]
La red
La red está representada por un conjunto de máquinas abstractas que pueden intercambiar mensajes. Estos mensajes constan de términos formales. Estos términos revelan parte de la estructura interna de los mensajes, pero es de esperar que algunas partes sigan siendo opacas para el adversario.
El adversario
El adversario en este modelo 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 con el atacante en la informática ubicua . [4]
El modelo algebraico
Los operadores abstractos modelan las primitivas criptográficas . Por ejemplo, el cifrado asimétrico para un usuario está representado por 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 . 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, ser 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 (enviar un mensaje a través de la red) y respuestas (obtener un mensaje de la red).
Observación
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, se han relacionado ambos tipos de modelos para protocolos criptográficos. [5] Además, los modelos simbólicos son muy adecuados para mostrar que un protocolo está roto , en lugar de ser seguro, bajo las suposiciones dadas sobre las capacidades de los atacantes.
Ver también
Referencias
- ^ Dolev, D .; Yao, AC (1983), "Sobre la seguridad de los protocolos de clave pública" (PDF) , IEEE Transactions on Information Theory , IT-29 (2): 198-208, doi : 10.1109 / tit.1983.1056650
- ^ Backes, Michael; Pfitzmann, Birgit; Waidner, Michael (2006), Límites de solidez de los modelos Dolev-Yao (PDF) , Taller sobre criptografía formal y computacional (FCC'06), afiliado a ICALP'06
- ^ Chen, Quingfeng; Zhang, Chengqi; Zhang, Shichao (2008), Análisis de protocolo de transacciones seguras: modelos y aplicaciones , Notas de clase en Ciencias de la Computación / Programación e Ingeniería de Software, ISBN 9783540850731
- ^ Creese, Sadie; Goldsmith, Michael; Roscoe, Bill; Zakiuddin, Irfan (2003). El atacante en entornos informáticos ubicuos: formalización del modelo de amenazas (PDF) . Proc. del 1er Taller Internacional sobre Aspectos Formales en Seguridad y Confianza (Informe técnico). págs. 83–97.
- ^ Herzog, Jonathan (2005), Una interpretación computacional de los adversarios de Dolev-Yao , CiteSeerX 10.1.1.94.2941
