Formal Specification and Model Checking of Lattice-Based Key Encapsulation Mechanisms in Maude

Abstract

Advances in quantum computing have shown a serious challenge for widely used current cryptographic techniques because a sufficient large-scale quantum computer can efficiently solve hard mathematical problems on which the current public-key cryptography is relying. That is the reason why recently many researchers and industrial companies have spent lots of effort on constructing post-quantum cryptosystems, which are resistant to quantum attackers. Large numbers of post-quantum key encapsulation mechanisms (KEMs) have been proposed to provide secure key establishment - one of the most important building blocks in asymmetric cryptography. This paper presents a formal security analysis of three lattice-based KEMs: Kyber, Saber, and SK-MLWR. We first formally specify each of them in Maude, a rewriting logic-based specification and programming language equipped with many functionalities, such as a reachability analyzer (or the search command) that can be used as an invariant model checker, and then conduct invariant model checking with the Maude search command, finding an attack. © 2022 Copyright for this paper by its authors.