Kyber, Saber, and SK-MLWR Lattice-Based Key Encapsulation Mechanisms Model Checking with Maude
Authors: 
Duong Dinh Tran, Kazuhiro Ogata, Santiago Escobar, Sedat Akleylek, Ayoub Otmani Academic Editor: Thomas HainesAuthors Info & Claims
Abstract
Facing the potential threat raised by quantum computing, a great deal of research from many groups and industrial giants has gone into building public-key post-quantum cryptographic primitives that are resistant to the quantum attackers. Among them, there is a large number of post-quantum key encapsulation mechanisms (KEMs), whose purpose is to provide a secure key exchange, which is a very crucial component in public-key cryptography. This paper presents a formal security analysis of three lattice-based KEMs including Kyber, Saber, and SK-MLWR. We use Maude, a specification language supporting equational and rewriting logic and a high-performance tool equipped with many advanced features, such as a reachability analyzer that can be used as a model checker for invariant properties, to model the three KEMs as state machines. Because they all belong to the class of lattice-based KEMs, they share many common parts in their designs, such as polynomials, vectors, and message exchange patterns. We first model these common parts and combine them into a specification, called base specification. After that, for each of the three KEMs, by extending the base specification, we just need to model some additional parts and the mechanism execution. Once completing the three specifications, we conduct invariant model checkings with the Maude search command, pointing out a similar man-in-the-middle attack. The occurrence of this attack is due to the fact that authentication is not part of the KEMs, and therefore an active attacker can modify all communication between two honest parties.
References
[1]
P. W. Shor, “Algorithms for quantum computation: discrete logarithms and factoring,” in Proceedings 35th Annual Symposium on Foundations of Computer Science, pp. 124–134, IEEE, Santa Fe, NM, USA, November 1994.
[2]
L. K. Grover, “A fast quantum mechanical algorithm for database search,” in STOC ’96: Proceedings of the Twenty-Eighth Annual ACM Symposium on Theory of Computing, pp. 212–219, Association for Computing Machinery, New York, NY, USA, July 1996.
[3]
B. Blanchet, “Security protocol verification: symbolic and computational models,” in Principles of Security and Trust. POST 2012. Lecture Notes in Computer Science, vol. 7215, pp. 3–29, Springer, Berlin, Heidelberg, 2012.
[4]
J. Bos, L. Ducas, E. Kiltz, T. Lepoint, V. Lyubashevsky, J. M. Schanck, P. Schwabe, G. Seiler, and D. Stehle, “CRYSTALS - kyber: a CCA-secure module-lattice-based KEM,” in 2018 IEEE European Symposium on Security and Privacy (EuroS&P), pp. 353–367, IEEE, London, UK, April 2018.
[5]
J. P. D.’Anvers, A. Karmakar, S. Sinha Roy, and F. Vercauteren, “Saber: Module-LWR based key exchange, CPA-secure encryption and CCA-secure KEM,” in Progress in Cryptology - AFRICACRYPT. 2018 - International Conference on Cryptology in Africa, Marrakesh, vol. 10831 of Lecture Notes in Computer Science, A. Joux, A. Nitaj, and T. Rachidi, Eds., pp. 282–305, Springer, Cham, Morocco, May 2018.
[6]
S. Akleylek and K. Seyhan, “Module learning with rounding based key agreement scheme with modified reconciliation,” Computer Standards & Interfaces, vol. 79, 2022.
[7]
F. Durán, S. Eker, S. Escobar, N. Martí-Oliet, J. Meseguer, R. Rubio, and C. Talcott, “Programming and symbolic computation in maude,” Journal of Logical and Algebraic Methods in Programming, vol. 110, 2020.
[8]
D. Dolev and A. Yao, “On the security of public key protocols,” IEEE Transactions on Information Theory, vol. 29, no. 2, pp. 198–208, 1983.
[9]
D. D. Tran, K. Ogata, S. Escobar, S. Akleylek, and A. Otmani, “Formal specification and model checking of lattice-based key encapsulation mechanisms in maude,” in Proceedings of the International Workshop on Formal Analysis and Verification of Post-Quantum Cryptographic Protocols co-located with the 23rd International Conference on Formal Engineering Methods (ICFEM 2022), vol. 3280 of CEUR Workshop Proceedings, S. Akleylek, S. Escobar, K. Ogata, and A. Otmani, Eds., pp. 16–32, Madrid, Spain, October 2022.
[10]
D. D. Tran, K. Ogata, S. Escobar, S. Akleylek, and A. Otmani, “Formal specification and model checking of saber lattice-based key encapsulation mechanism in maude,” in The 34th International Conference on Software Engineering and Knowledge Engineering, SEKE 2022, KSIR Virtual Conference Center, USA, pp. 382–387, KSI Research Inc, July 2022.
[11]
R. Avanzi, J. Bos, L. Ducas, E. Kiltz, T. Lepoint, V. Lyubashevsky, J. M. Schanck, P. Schwabe, G. Seiler, and D. Stehlé, “CRYSTALS-Kyber: algorithm specifications and supporting documentation (version 3.02),” 2021, https://pq-crystals.org/kyber/data/kyber-specification-round3-20210804.pdf.
[12]
A. Basso, J. M. B. Mera, J.-P. D’Anvers, A. Karmakar, S. S. Roy, M. V. Beirendonck, and F. Vercauteren, “SABER: Mod-LWR based KEM (round 3 submission),” 2017, https://www.esat.kuleuven.be/cosic/pqcrypto/saber/files/saberspecround3.pdf.
[13]
M. Campagna and E. Crockett, “Hybrid post-quantum key encapsulation methods (PQ KEM) for transport layer security 1.2 (TLS),” 2021, RFC Editor https://datatracker.ietf.org/doc/html/draft-campagna-tls-bike-sike-hybrid.
[14]
B. LaMacchia, K. Lauter, and A. Mityagin, “Stronger security of authenticated key exchange,” in Provable Security, International Conference on Provable Security, ProvSec 2007, vol. 4784 of Lecture Notes in Computer Science, W. Susilo, J. K. Liu, and Y. Mu, Eds., pp. 1–16, Springer, Berlin, Heidelberg, Wollongong, Australia, 2007.
[15]
L. Zhou and F. Lv, “A simple provably secure AKE from the LWE problem,” Mathematical Problems in Engineering, vol. 2017, 16 pages, 2017.
[16]
J. Ding, P. Branco, and K. Schmitt, “Key exchange and authenticated key exchange with reusable keys based on RLWE assumption,” Cryptology ePrint Archive, 2019.
[17]
C. Jacomme, E. Klein, S. Kremer, and M. Racouchot, “A comprehensive, formal and automated analysis of the EDHOC protocol,” in 32nd USENIX Security Symposium (USENIX Security 23, pp. 5881–5898, USENIX Association, Anaheim, CA, 2023.
[18]
A. Hülsing, K.-C. Ning, P. Schwabe, F. Weber, and P. R. Zimmermann, “Post-quantum WireGuard,” in 2021 IEEE Symposium on Security and Privacy (SP), pp. 304–321, IEEE, San Francisco, CA, USA, May 2021.
[19]
G. Selander, J. P. Mattsson, and F. Palombini, “Ephemeral Diffie–Hellman over COSE (EDHOC),” 2022, Internet Engineering Task Force. draft-ietf-lake-edhoc-17. work in Progress, https://datatracker.ietf.org/doc/draft-ietf-lake-edhoc/17/.
[20]
V. Cheval, C. Jacomme, S. Kremer, and R. Künnemann, “SAPIC+: protocol verifiers of the world, unite!” in 31st USENIX Security Symposium (USENIX Security 22, pp. 3935–3952, USENIX Association, Boston, MA, USA, 2022.
[21]
B. Blanchet, V. Cheval, and V. Cortier, “ProVerif with lemmas, induction, fast subsumption, and much more,” in 2022 IEEE Symposium on Security and Privacy (SP), pp. 69–86, IEEE, San Francisco, CA, USA, May 2022.
[22]
D. Basin, C. Cremers, J. Dreier, and R. Sasse, “Symbolically analyzing security protocols using tamarin,” ACM SIGLOG News, vol. 4, no. 4, pp. 19–30, 2017.
[23]
J. A. Donenfeld, “WireGuard: next generation kernel network tunnel,” in Proceedings of the Network and Distributed System Security Symposium, NDSS 2017, San Diego, CA, USA, 2017.
[24]
S. Escobar, C. Meadows, and J. Meseguer, “Maude-NPA: cryptographic protocol analysis modulo equational properties,” in Foundations of Security Analysis and Design V, A. Aldini, G. Barthe, and R. Gorrieri, Eds., pp. 1–50, Springer, Berlin, Heidelberg, Berlin, Heidelberg, 2009.
[25]
C. J. F. Cremers, Scyther - semantics and verification of security protocols, Eindhoven University of Technology, 2006, Ph.D. thesis.
[26]
B. Blanchet, “Modeling and verifying security protocols with the applied pi calculus and ProVerif,” Foundations and Trends® in Privacy and Security, vol. 1, no. 1-2, pp. 1–135, 2016.
[27]
F. J. T. Thayer, J. C. Herzog, and J. D. Guttman, “Strand spaces: why is a security protocol correct?” in Proceedings. 1998 IEEE Symposium on Security and Privacy (Cat. No.98CB36186), pp. 160–171, IEEE, Oakland, CA, USA, May 1998.
[28]
S. Escobar, C. Meadows, J. Meseguer, and S. Santiago, “State space reduction in the Maude-NRL protocol analyzer,” Information and Computation, vol. 238, pp. 157–186, 2014.
[29]
J. C. Mitchell, “Multiset rewriting and security protocol analysis,” in Rewriting Techniques and Applications, vol. 2378, S. Tison, Ed., pp. 19–22, Springer, Berlin, Heidelberg, Copenhagen, Denmark, 2002.
[30]
V. K. Yadav, S. Venkatesan, and S. Verma, “Man in the middle attack on NTRU key exchange,” in Communication, Networks and Computing, S. Verma, R. S. Tomar, B. K. Chaurasia, V. Singh, and J. Abawajy, Eds., pp. 251–261, Springer Singapore, Singapore, 2019.
[31]
X. Lei and X. Liao, “NTRU-KE: a lattice-based public key exchange protocol,” Cryptology ePrint Archive, 2013, http://eprint.iacr.org/2013/718.
[32]
B. Blanchet, “Mechanizing game-based proofs of security protocols,” in Software Safety and Security - Tools for Analysis and Verification. vol. 33 of NATO Science for Peace and Security Series - D: Information and Communication Security, T. Nipkow, O. Grumberg, and B. Hauptmann, Eds., pp. 1–25, IOS Press, 2012.
[33]
G. Barthe, B. Grégoire, S. Heraud, and S. Z. Béguelin, “Computer-aided security proofs for the working cryptographer,” in Advances in Cryptology – CRYPTO 2011, vol. 6841, P. Rogaway, Ed., pp. 71–90, Springer, Berlin, Heidelberg, Santa Barbara, CA, USA, 2011.
[34]
G. Barthe, F. Dupressoir, B. Grégoire, C. Kunz, B. Schmidt, and P. Strub, “Easycrypt: a tutorial,” in Foundations of Security Analysis and Design VII, vol. 8604, A. Aldini, J. López, and F. Martinelli, Eds., pp. 146–166, Springer, Cham, 2013.
[35]
B. Blanchet, “Automatically verified mechanized proof of one-encryption key exchange,” in 2012 IEEE 25th Computer Security Foundations Symposium, pp. 325–339, IEEE, Cambridge, MA, USA, June 2012.
[36]
E. Bresson, O. Chevassut, and D. Pointcheval, “Security proofs for an efficient password-based key exchange,” in CCS ’03: Proceedings of the 10th ACM Conference on Computer and Communications Security, pp. 241–250, Association for Computing Machinery, New York, NY, USA, October 2003.
[37]
S. M. Bellovin and M. Merritt, “Encrypted key exchange: password-based protocols secure against dictionary attacks,” in Proceedings of the IEEE Symposium on Research in Security and Privacy, pp. 72–84, IEEE, Oakland, CA, USA, May 1992.
[38]
P. Kampanakis, D. Stebila, and T. Hansen, “Post-quantum hybrid key exchange in SSH,” 2023, Internet Engineering Task Force, draft-kampanakis-curdle-ssh-pq-ke-01. work in Progress, https://datatracker.ietf.org/doc/draft-kampanakis-curdle-ssh-pq-ke/01/.
Index Terms
- Kyber, Saber, and SK-MLWR Lattice-Based Key Encapsulation Mechanisms Model Checking with Maude
Index terms have been assigned to the content through auto-classification.
Recommendations
Key Recovery Attack on CRYSTALS-Kyber and Saber KEMs in Key Reuse Scenario
Computer Security – ESORICS 2024AbstractCrystals-Kyber, a key encapsulation mechanism (KEM) whose security is based on the Module-LWE problem, has recently been selected by NIST as part of its post-quantum cryptography initiative. At ASIACRYPT 2021, Qin et al. gave a method to evaluate ...
Efficient key encapsulation mechanisms with tight security reductions to standard assumptions in the two security models
In this paper, we propose two new practical constructions of chosen ciphertext attack secure CCA secure key encapsulation mechanisms KEM, which is the main building block for public key encryption in hybrid encryption, with remarkable security features: ...
Lattice-based certificateless public-key encryption in the standard model
The notion of certificateless public-key encryption (CL-PKE) was introduced by Al-Riyami and Paterson in 2003 that avoids the drawbacks of both traditional PKI-based public-key encryption (i.e., establishing public-key infrastructure) and identity-based ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
Copyright © 2023 Duong Dinh Tran et al.
This is an open access article distributed under the Creative Commons Attribution License, which permits unrestricted use, distribution, and reproduction in any medium, provided the original work is properly cited.
Publisher
John Wiley & Sons, Inc.
United States
Publication History
Published: 30 October 2023
Qualifiers
- Research-article
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 0Total Downloads
- Downloads (Last 12 months)0
- Downloads (Last 6 weeks)0
Reflects downloads up to 06 Jan 2025