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

Abstract

[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.