La verificación formal de protocolos criptográficos es la verificación de protocolos criptográficos para garantizar las propiedades de seguridad requeridas. Uno de los componentes de dicha verificación es determinar la resistencia del protocolo a los ataques, asumiendo la confiabilidad de las primitivas criptográficas en las que se basa. Para resolver este problema, se han desarrollado una serie de enfoques basados en varios métodos de verificación formal . Una característica común de los métodos formales es el uso de un enfoque sistemático del problema, lo que le permite realizar una verificación más razonable, precisa y eficiente de las propiedades de seguridad del protocolo.
El término verificación formal de protocolos criptográficos fue introducido por primera vez por Catherine Meadows [ 1] , investigadora principal de los ingleses. Centro de Sistemas Informáticos de Alta Garantía (CHACS) [2] y Laboratorio de Investigación Naval (NRL).
A la hora de verificar los protocolos criptográficos, además de comprobar las propiedades tradicionales que garantizan el correcto funcionamiento de los sistemas distribuidos, también se presta mayor atención a la justificación de las propiedades especiales de seguridad de la información . Las más importantes de estas propiedades son las siguientes propiedades:
La definición matemática rigurosa de estas propiedades depende esencialmente del modelo formal en términos del cual se describe el protocolo criptográfico. Por lo general, al verificar los protocolos criptográficos, se hacen las siguientes suposiciones sobre las habilidades del adversario:
Por lo tanto, para garantizar la confidencialidad e integridad de la información, el protocolo debe diseñarse de modo que ningún adversario pueda extraer suficiente información de los mensajes interceptados para llevar a cabo la amenaza prevista.
Las máquinas de estado se pueden utilizar para analizar protocolos criptográficos. En este caso, se aplica una técnica conocida como técnica de análisis de accesibilidad. Esta técnica asume la descripción del sistema de la siguiente forma. Para cada transición se construye un estado global del sistema, que se expresa a través de los estados de las entidades del sistema y los estados de los canales de comunicación entre ellas. A continuación, se analiza cada estado global y se determinan sus propiedades, como interbloqueo y corrección. Si la entidad no puede recibir el mensaje y se suponía que debía recibirse en este estado, entonces hay un problema en el protocolo.
La técnica de análisis de accesibilidad es eficaz para determinar la corrección de un protocolo frente a sus especificaciones, pero no garantiza la seguridad frente a un atacante activo.
Existe un método automático completo para verificar las propiedades de confidencialidad de los protocolos criptográficos. El método se basa en una interpretación abstracta robusta de los protocolos criptográficos que utiliza una extensión de los autómatas de árbol , a saber, los autómatas de árbol con parámetros V, que mezcla técnicas autoteóricas con las características de las técnicas deductivas. Contrariamente a la mayoría de los enfoques de verificación de modelos , este método ofrece garantías de seguridad de facto. Se describe la posibilidad de analizar protocolos en presencia de principales multisesión paralelos.
Un protocolo criptográfico expuesto a un adversario se denomina sistema de salto etiquetado (LTS). Cada estado LTS está representado por un par (S,K) , donde S es el estado de cálculo del protocolo y K es el conocimiento disponible para el adversario. Las transiciones a LTS se realizan en función de la especificación del protocolo y las suposiciones sobre las capacidades adversarias (modelo adversario). Como resultado de las transiciones, tanto los estados de cálculo del protocolo como el conocimiento del enemigo pueden cambiar. Algunas de las transiciones se pueden etiquetar con acciones que se realizan en la transición. La propiedad del protocolo a comprobar se especifica mediante una fórmula lógica. Para este propósito, pueden ser adecuadas las lógicas temporales , las lógicas del conocimiento , etc .. Así, la verificación de protocolos criptográficos se reduce a la tarea clásica de la lógica matemática: verificar la factibilidad de una fórmula en un modelo. Verificar muchas propiedades se reduce a verificar la accesibilidad de ciertos estados en el LTS; Se han desarrollado numerosos algoritmos para resolver este problema. La ventaja de este enfoque es la simplicidad y versatilidad, así como la posibilidad de utilizar numerosas herramientas para resolver el problema de la verificación del modelo. La mayor dificultad encontrada al probar protocolos reales es que los LTS pueden tener un número ilimitado de estados. Para superar esta dificultad, se utilizan métodos simbólicos para representar modelos, métodos para construir un modelo sobre la marcha (on-the-fly), varios tipos de abstracción de datos.
La descripción (especificación) del protocolo se representa como una fórmula Spec de algún lenguaje lógico formal. La descripción de las capacidades del adversario y la propiedad del protocolo probado también están representadas por las fórmulas Φ y Ψ . El problema de verificación se reduce a comprobar la derivabilidad de la fórmula Ψ a partir de las fórmulas Spec y Φ . La principal ventaja de este enfoque es que le permite verificar las propiedades necesarias para los protocolos iterativos , independientemente del número de rondas de su ejecución. La desventaja es que la construcción de la demostración suele ser muy laboriosa y no puede automatizarse por completo. Por lo general, la construcción de una prueba de este tipo se reduce a la formación de un sistema especial de restricciones, en el que, junto con el dispositivo de protocolo, se tienen en cuenta los conocimientos y capacidades del adversario, y se verifica la solución de este sistema de restricciones. .
En el caso de que el lenguaje de especificación de los protocolos criptográficos esté dotado de semántica operacional formal (como es el caso del spi-calculus ), se puede introducir una relación de equivalencia de traza o bisimulación ≈ sobre un conjunto de protocolos . Entonces, para comprobar algunas propiedades del protocolo parametrizado P(M) dado , es suficiente comprobar que para cualquier proceso A actuando como adversario, se cumple la equivalencia A|P(M)≈A|P(M) . En este caso, se dice que los procesos P(M) y P(M′) están en una relación de equivalencia de prueba. Se encontró que las tareas de verificar las propiedades de confidencialidad e integridad de los protocolos se reducen a la tarea de verificar la equivalencia de prueba de los procesos spi . Se propuso un algoritmo para verificar la equivalencia de prueba de procesos spi libres de replicación . La característica principal de este problema es que la equivalencia A|P(M) ≈ A|P(M ) debe verificarse para un proceso arbitrario A (adversario), y esto lleva a la necesidad de analizar un conjunto infinitamente grande de cálculos de longitud finita. Se señaló que para verificar de manera efectiva la equivalencia de las pruebas, es necesario desarrollar métodos para la representación simbólica y el análisis del conocimiento del enemigo. En esta nota, proponemos un método alternativo para representar y analizar el conocimiento del enemigo, que se puede utilizar para probar la equivalencia de prueba de los procesos de cálculo de spi .
El enfoque más reciente para el análisis de protocolo formal es utilizar el método de verificación de tipo introducido por Abadi . Abadi introdujo el tipo no confiable (Un) para los mensajes abiertos que se originan en un oponente (todos, excepto los principales que autentican, actúan como oponentes). En el método de verificación de tipos, a los mensajes y canales se les asignan tipos (por ejemplo, un elemento de datos de tipo privado aparece en un canal público). El método de verificación de tipos tiene la gran ventaja de que, al igual que el método de verificación de modelos, es completamente automático, pero a diferencia de este último, es capaz de operar con varias clases de sistemas infinitos. Sin embargo, tiene la desventaja potencial de que, dado que las violaciones de seguridad se definen en términos de inconsistencias de tipo, los requisitos de seguridad que se probarán deben establecerse en la especificación tal como está escrita. Esto distingue un método de verificación de tipo de un método de verificación de modelo, para el cual cualquier propiedad de seguridad que pueda expresarse en términos de lógica temporal puede especificarse independientemente, después de que se haya especificado el protocolo en sí.
Existe una técnica para la verificación automática de protocolos criptográficos basada en una representación intermedia del protocolo utilizando un conjunto de frases de Horn (un programa lógico). Esta técnica permite verificar las propiedades de seguridad de los protocolos, como la confidencialidad y la autenticación , de forma totalmente automática. Además, las pruebas obtenidas con su ayuda son correctas para un número ilimitado de sesiones de protocolo.
El método de justificación basado en la condición previa más débil (razonamiento de la condición previa más débil) está destinado a la verificación del programa. Esta técnica considera tres componentes: el estado anterior a la ejecución de la instrucción del programa, la instrucción del programa en sí y el objetivo, que debe ser verdadero después de ejecutar la instrucción. La desventaja de esta técnica radica en la dificultad de la prueba para predicados complejos . Para programas largos con muchos objetivos, las pruebas pueden no ser posibles. En el trabajo dedicado al entorno integrado CPAL-ES (Cryptographic Protocol Analysis Language Evaluation System), se utiliza el método de “precondición más débil” para la verificación. Dado que los protocolos criptográficos tienden a ser cortos, este método se ha aplicado con éxito a estos protocolos.
El verificador automático de protocolo criptográfico AVISPA, que incluye la herramienta TA4SL, puede analizar un número limitado e ilimitado de sesiones de protocolo utilizando OFMC , CL-ATSE y SATMC . AVISPA es muy adecuado para analizar las propiedades de seguridad en el caso de un número limitado de sesiones. Para sesiones ilimitadas, AVISPA solo brinda soporte limitado. Por ejemplo, el uso de AVISPA es especialmente problemático si no hay rastros de un ataque.
La herramienta de verificación automática de protocolos criptográficos ProVerif, que implementa el método de inferencia lógica, permite analizar un número ilimitado de sesiones de protocolo utilizando la aproximación superior y la representación de protocolo mediante expresiones Horn .
ProVerif le permite verificar automáticamente la propiedad de privacidad , la propiedad de autenticación , manejar muchas primitivas criptográficas diferentes, incluida la criptografía de clave pública y compartida (cifrado y firma ), funciones hash y acuerdo de clave Diffie-Hellman , especificado tanto en las reglas de reescritura como en el forma de ecuaciones.
ProVerif puede procesar un número ilimitado de sesiones de protocolo (incluso en paralelo) y un espacio de mensajes ilimitado, le permite especificar el modelo de protocolo en términos cercanos al área temática modelada y, en la mayoría de los casos, brinda la oportunidad de obtener una u otra respuesta sobre las propiedades del protocolo. Las desventajas de ProVerif incluyen el hecho de que esta herramienta puede indicar ataques falsos y también requiere una estrecha interacción con el usuario y una comprensión profunda de la esencia del problema al verificar los protocolos.
El verificador de protocolo criptográfico automático de Scyther utiliza análisis simbólico combinado con búsqueda bidireccional basada en patrones parcialmente ordenados y verifica un número limitado e ilimitado de sesiones de protocolo.
En el enfoque de Scyther, un protocolo se define como una secuencia de eventos, donde los eventos incluyen tanto la transmisión de mensajes intercambiados por los participantes de la sesión como los mensajes que un atacante puede insertar. Se utiliza una notación para distinguir entre "hilos" (ejecuciones separadas de un evento).
Scyther no requiere que se especifique un script de ataque. Solo es necesario establecer parámetros que limiten el número máximo de ejecuciones o el espacio de trayectorias a iterar.
La herramienta FDR2, que se basa en el método de verificación de modelos, utiliza la notación CSP (Comunicación de procesos secuenciales) para describir el comportamiento de los participantes del protocolo. Cada participante del protocolo se modela como un proceso CSP que está esperando un mensaje o enviando un mensaje. Los canales se utilizan para comunicarse entre procesos y simular adversarios. El adversario se describe como una composición paralela de varios procesos, uno para cada hecho o mensaje, de los que puede obtener alguna información sobre la ejecución del protocolo. FDR2 utiliza un enfoque llamado verificación del modelo de refinamiento . Consiste en confirmar que el modelo que describe el comportamiento del sistema que implementa el protocolo bajo prueba es equivalente al modelo que especifica los requisitos de seguridad para este protocolo.