Formal methods for the analysis of security protocols

Resumen

Los sistemas informáticos que aparecen en la actualidad se encuentran orientados al desarrollo de entornos colaborativos y distribuidos, Estas tendencias han convertido a las redes, y especialmente a Internet, en elementos clave en el proceso del diseño de un sistema. La aparición de nuevos tipos de aplicaciones sobre Internet que implican el intercambio de datos privados han otorgado suma importacia al estudio de los protocolos de seguridad. Las soluciones tradicionales en este campo no son adecuadas para los nuevos requisitos en seguridad. Actualmente, la criptografía debe, ademas de proporcionar confidencialidad, garantizar intergridad, no-repudio, autenticación, autorización, . . . . Además es necesario el desarrollo de nuevos esquemas criptográficos que den cobertura a las nuevas necesidades. Los protocolos de seguridad son programas distribuidos que se ejecutan bajo un entorno inseguro. Debido a su naturaleza distribuida son complejos de diseñar, junco con que el anlisis de su correctitud es una tarea crucial. La mayoria de los métodos formales omiten el tiempo para incrementar su rendimiento. Sin embargo, en sistemas de seguridad, como programas distribuidos que son, el tiempo tiene gran influencia en su ejecución. Los aspectos temporales de un protocolo de seguridad se pueden dividir en dos categorias. Primero, las marcas temporales e información temporal (tiempo de vida para los tokens, las sesiones, las claves, . . . ) que son incluidos en los mensajes. Segundo, el flujo temporal de los protocolos (tiempos de caducidad, retransmisiones,. . . ) que pueden ser explotados por un intruso para llevar a cabo un ataque. De forma que no solo estamos interesados en modelar elementos temporales pero tambien en representar el flujo temporal en nuestro modelos. Los automatas temporizados extendidos que presentamos en esta tesis doctoral nos ayudan en ambos casos. Los modelos basados en la propuesta de Dolev-Yao consideran un medio de comunicación hostil en una red cableada. Debido al desarrollo de las redes inalmbricas y la aparición de nuevas tecnologías, como los servicios web o las redes inalámbricas de sensores, este modelo no es apropiado. Necesitamos representar diferentes medios de comunicación con diferentes propiedades que pueden afectar a la seguridad del sistema. Otra razón para introducir nuestra extensión para automatas temporizados. La verificación de protocolos de seguridad es una tarea crucial en la mayoria de los procesos de desarrollo de sistemas de comunicacin. Pero el análisis de los protocolos de seguridad no se puede realizar de forma aislada. Debe integrarse en los procesos de desarrollo de software. Como consequencia, no solo necesitamos un mecanismo para analizar protocolos de seguridad, sino que también es necesario una metodologa bien definida para aplicar el mecanismo de análisis. Después de todo esto, en esta tesis doctoral, se presenta como contribución principal una metodología para el diseño y análisis de protocolos de seguridad mediante Uppaal asi como un nuevo tipo de automata temporizados de comportamiento extendido. La metodología se encarga de definir un conjunto de pasos bien establecidos para permitir que diseñadores desarrollen analicen un protocolo de seguridad siguiendo un estilo incremental. Además, introducimos los automatas de comportamiento extendido como herramienta para facilitar la tarea de modelado del sistema.