Verificación formal de protocolos de seguridad en HOL a partir del método inductivo

Abstract

Muchos protocolos de seguridad han presentado fallas sutiles que han sido descubiertos a través de los métodos formales. De ahí que la principal razón por formalizarlos es para eliminar errores humanos. Sin embargo, muchos modelos se han limitado en demostrar sólo propiedades de autentificación. Ahora por la enorme cantidad de transacciones electrónicas y por personas malignas en la red, necesitamos métodos más potentes que también permitan verificar propiedades como confidencialidad, frescura y posibilidad. Uno de ellos es el Método inductivo desarrollado por Lawrence C. Paulson [ 16]. Sin embargo, este método está orientado a una comunidad específica (usuarios de Isabelle). La principal motivación para desarrollar el presente trabajo es proporcionar el método inductivo de Paulson a otra gran comunidad de usuarios que utilizan la herramienta del Sistema HOL1 [20, 40]. Con esto lograremos popularizar el método para que mayor número de usuarios puedan utilizar la verificación formal de protocolos de seguridad en HOL a partir del método inductivo. El método inductivo se basa específicamente de cuatro teorías: la de mensajes, eventos, llaves compartidas y llaves públicas. La teoría de mensajes contiene la definición de los tipos de agentes, de los mensajes, tipos de operadores para modelar el tráfico existente en la red. La teoría de eventos, contiene la definición de los tipos de eventos que pueden suceder al enviar un mensaje por la red o al recibirlos. Se modela el conocimiento de cada uno de los tipos de agentes y la frescura de los mensajes. Las teorías de llaves compartidas y llaves públicas proporcionan propiedades del conocimiento inicial de los agentes, características propias de las llaves y garantías sobre el suministro de llaves. Cada una de las teorías contiene propiedades específicas y son representados en forma de teoremas matemáticos. Al finalizar cada una de las teorías desarrolladas en HOL, hemos verificado el protocolo OtwayRees, demostrando entre otras propiedades autenticación. Por último, se dan las conclusiones y los trabajos futuros propuestos para la continuidad de este trabajo.