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

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

2022 International Workshop on Formal Analysis and Verification of Post-Quantum Cryptographic Protocols, FAVPQC 2022, Madrid, İspanya, 24 Ekim 2022, cilt.3280, ss.16-31 identifier

  • Yayın Türü: Bildiri / Tam Metin Bildiri
  • Cilt numarası: 3280
  • Basıldığı Şehir: Madrid
  • Basıldığı Ülke: İspanya
  • Sayfa Sayıları: ss.16-31
  • Anahtar Kelimeler: key encapsulation mechanism, Maude, model checking, post-quantum
  • Ondokuz Mayıs Üniversitesi Adresli: Evet

Özet

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.