Formal specification and model checking of Saber lattice-based key encapsulation mechanism in Maude

Creative Commons License

Tran D. D., Ogata K., Escobar S., Akleylek S., Otmani A.

34th International Conference on Software Engineering and Knowledge Engineering, SEKE 2022, Pennsylvania, United States Of America, 1 - 10 July 2022, pp.382-387 identifier

  • Publication Type: Conference Paper / Full Text
  • Doi Number: 10.18293/seke2022-097
  • City: Pennsylvania
  • Country: United States Of America
  • Page Numbers: pp.382-387
  • Keywords: KEM, lattice-based cryptography, Maude, model checking, post-quantum cryptography
  • Ondokuz Mayıs University Affiliated: Yes


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.