Modeling and verification of the post-quantum key encapsulation mechanism KYBER using Maude





Publicado en

Actas de las XXII Jornadas sobre Programación y Lenguajes (PROLE 2023)




Communication and information technologies shape the world’s systems of today, and those systems shape our society. The security of those systems relies on mathematical problems hard to solve for classical computers, that is, the available current computers. Recent advances in quantum computing threaten the security of our systems and the communications we use. In order to face this threat, multiple solutions and protocols have been proposed. Kyber is one of these protocols, and precisely it is a key encapsulation mechanism that bases its security in the learning with errors problem over module lattices. The presented work 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 of quantum adversaries and study how Kyber works. In the system-specification language Maude, we then construct a symbolic model to represent the behaviour of Kyber in a network. In this model, we conduct reachability analysis with the s e a r c h 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 by proving if liveness and security properties hold. Conference name: FAVPQC 2022: International Workshop on Formal Analysis and Verification of Post-Quantum Cryptographic Protocols. Year of publication: 2022


Acerca de García, Víctor

Palabras clave

Maude, Rewriting Logic, Formal Verification, Post-quantum Protocols, Key Encapsulation Mechanisms
Página completa del ítem
Notificar un error en este resumen
Mostrar cita
Mostrar cita en BibTeX
Descargar cita en BibTeX