Formal methods for the analysis of security protocols.
Tobarra Abad, María de los Llanos · Dialnet (Universidad de la Rioja) · 2012
Los sistemas informaticos 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 diseno de un sistema. La aparicion 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 criptografia debe, ademas de proporcionar confidencialidad, garantizar intergridad, no-repudio, autenticacion, autorizacion, . . . . Ademas es necesario el desarrollo de nuevos esquemas criptograficos 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 disenar, junco con que el anlisis de su correctitud es una tarea crucial. La mayoria de los metodos 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 ejecucion. Los aspectos temporales de un protocolo de seguridad se pueden dividir en dos categorias. Primero, las marcas temporales e informacion 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 comunicacion hostil en una red cableada. Debido al desarrollo de las redes inalmbricas y la aparicion de nuevas tecnologias, como los servicios web o las redes inalambricas de sensores, este modelo no es apropiado. Necesitamos representar diferentes medios de comunicacion con diferentes propiedades que pueden afectar a la seguridad del sistema. Otra razon para introducir nuestra extension para automatas temporizados. La verificacion de protocolos de seguridad es una tarea crucial en la mayoria de los procesos de desarrollo de sistemas de comunicacin. Pero el analisis 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 tambien es necesario una metodologa bien definida para aplicar el mecanismo de analisis. Despues de todo esto, en esta tesis doctoral, se presenta como contribucion principal una metodologia para el diseno y analisis de protocolos de seguridad mediante Uppaal asi como un nuevo tipo de automata temporizados de comportamiento extendido. La metodologia se encarga de definir un conjunto de pasos bien establecidos para permitir que disenadores desarrollen analicen un protocolo de seguridad siguiendo un estilo incremental. Ademas, introducimos los automatas de comportamiento extendido como herramienta para facilitar la tarea de modelado del sistema.