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, Amerika Birleşik Devletleri, 1 - 10 Temmuz 2022, ss.382-387 identifier

  • Yayın Türü: Bildiri / Tam Metin Bildiri
  • Doi Numarası: 10.18293/seke2022-097
  • Basıldığı Şehir: Pennsylvania
  • Basıldığı Ülke: Amerika Birleşik Devletleri
  • Sayfa Sayıları: ss.382-387
  • Anahtar Kelimeler: KEM, lattice-based cryptography, Maude, model checking, post-quantum cryptography
  • Ondokuz Mayıs Üniversitesi Adresli: Evet

Özet

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.