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

Abstract

The security of most public-key cryptosystems currently in use today is threatened by advances in quantum computing. 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. A large number 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 Saber lattice-based KEM. We first formally specify the mechanism in Maude, a rewriting logic-based specification/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 Knowledge Systems Institute Graduate School. All rights reserved.