Research Information System
2022 International Workshop on Formal Analysis and Verification of Post-Quantum Cryptographic Protocols, FAVPQC 2022, Madrid, Spain, 24 October 2022, vol.3280, pp.16-31, (Full Text)
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.