Resumen

El modelo de espacio de hebras ha sido propuesto como un método formal para verificar los objetivos de seguridad de los protocolos criptográficos. Sin embargo, actualmente solo se admiten operaciones de cifrado y descifrado y funciones hash para la semántica de los primitivos criptográficos. Por lo tanto, establecemos el marco del modelo de espacio de hebras extendido (ESSM) para describir operaciones algebraicas y modelos de amenazas avanzados. Basándonos en el ESSM, añadimos semántica algebraica, incluyendo el grupo Abeliano y la operación XOR, y un modelo de amenazas basado en ataques algebraicos, ataques de suplantación de compromiso de clave y ataques de adivinanza. Implementamos nuestro modelo utilizando la herramienta de análisis automático, Scyther. Demostramos la efectividad de nuestro marco analizando varios protocolos, en particular un protocolo de acuerdo de tres factores, con el cual podemos identificar nuevos ataques al tiempo que proporcionamos pruebas de traza.

• Materias:Cifrado de búsqueda Seguridad informática Reconstrucción virtual Detección de intrusos Sistema de programación
• Subjects:Search encryption Computer security Virtual reconstruction Intrusion detection Programming system
• Palabras claves:Propuesta; Método formal; Protocolos criptográficos; Cifrado; Operaciones de descifrado; Funciones hash
• Keywords:Proposed; Formal method; Cryptographic protocols; Encryption; Decryption operations; Hash functions