Modelado y verificación del mecanismo de encapsulación de claves post-cuánticas KYBER usando Maude

Abstract

[ES] Las tecnologías de la información y la comunicación dan forma a los sistemas del mundo de hoy, y esos sistemas dan forma a la sociedad en la que vivimos. La seguridad de esos sistemas se basa en problemas matemáticos difíciles de resolver para las computadoras clásicas, es decir, las computadoras disponibles en la actualidad. Los avances recientes en computación cuántica amenazan la seguridad de nuestros sistemas y las comunicaciones que utilizamos con ellos. Para hacer frente a la amenaza se han propuesto múltiples soluciones y protocolos. Kyber es uno de ellos, en concreto se trata de un mecanismo de encapsulación de claves que basa su seguridad en el problema de aprendizaje con errores sobre retículos modulares. Este trabajo de fin de máster se centra en el análisis de Kyber para comprobar su seguridad bajo las asunciones del adversario del modelo de Dolev-Yao. Para conseguir este objetivo, primero aprendemos sobre el estado actual de las soluciones propuestas contra la amenaza que suponen los adversarios cuánticos y estudiamos cómo funciona Kyber. Luego construimos en el lenguaje de especificación del sistema Maude, un modelo simbólico para representar el comportamiento de Kyber en una red. En este modelo, llevamos a cabo un análisis de alcanzabilidad con el comando search y encontramos que hay un ataque Man-In-The-Middle presente. Luego, usamos la herramienta Maude LTL logical model checker para ampliar el análisis del sistema y probar si se mantienen unas propiedades de viveza y seguridad.

[EN] Communication and information technologies shape the world's systems of today, and those systems shape the society we live in. The security of those systems relay on mathematical problems hard to solve for classical computers, that is, the available current computers. Recent advances in quantum computing threat the security of our systems and the communications we use. In order to face the threat, multiple solutions and protocols have been proposed. Kyber is one of them, specifically it is a key encapsulation mechanism that bases its security in the learning with errors problem over module lattices. This master's thesis focuses on the analysis of Kyber to check its security under Dolev-Yao adversary assumptions. For that matter, we first learn about the current state of the solutions proposed against the threat quantum adversaries suppose and study how Kyber works. We then construct in the system-specification language Maude, a symbolic model to represent the behaviour of Kyber in a network. On this model we conduct reachability analysis with the search command and find that a Man-In-The-Middle attack is present. Then we use the Maude LTL logical model checker to extend the analysis of the system with proving if a liveness and a security property hold.