Kyber, Saber, and SK-MLWR Lattice-Based Key Encapsulation Mechanisms Model Checking with Maude

Facing the potential threat raised by quantum computing, a great deal of research from many groups and industrial giants has gone into building public-key post-quantum cryptographic primitives that are resistant to the quantum attackers. Among them, there is a large number of post-quantum key encapsulation mechanisms (KEMs), whose purpose is to provide a secure key exchange, which is a very crucial component in public-key cryptography. This paper presents a formal security analysis of three lattice-based KEMs including Kyber, Saber, and SK-MLWR. We use Maude, a specification language supporting equational and rewriting logic and a high-performance tool equipped with many advanced features, such as a reachability analyzer that can be used as a model checker for invariant properties, to model the three KEMs as state machines. Because they all belong to the class of lattice-based KEMs, they share many common parts in their designs, such as polynomials, vectors, and message exchange patterns. We first model these common parts and combine them into a specification, called base specification. After that, for each of the three KEMs, by extending the base specification, we just need to model some additional parts and the mechanism execution. Once completing the three specifications, we conduct invariant model checkings with the Maude search command, pointing out a similar man-in-the-middle attack. The occurrence of this attack is due to the fact that authentication is not part of the KEMs, and therefore an active attacker can modify all communication between two honest parties.