{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,19]],"date-time":"2026-01-19T01:04:49Z","timestamp":1768784689757,"version":"3.49.0"},"reference-count":38,"publisher":"Institution of Engineering and Technology (IET)","issue":"1","license":[{"start":{"date-parts":[[2023,10,30]],"date-time":"2023-10-30T00:00:00Z","timestamp":1698624000000},"content-version":"vor","delay-in-days":302,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100008530","name":"European Regional Development Fund","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100008530","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100003359","name":"Generalitat Valenciana","doi-asserted-by":"publisher","award":["CIPROM\/2022\/6"],"award-info":[{"award-number":["CIPROM\/2022\/6"]}],"id":[{"id":"10.13039\/501100003359","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100004410","name":"T\u00fcrkiye Bilimsel ve Teknolojik Ara\u015ft\u0131rma Kurumu","doi-asserted-by":"publisher","award":["121R006"],"award-info":[{"award-number":["121R006"]}],"id":[{"id":"10.13039\/501100004410","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100004794","name":"Centre National de la Recherche Scientifique","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100004794","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001665","name":"Agence Nationale de la Recherche","doi-asserted-by":"publisher","award":["ANR-22-PETQ-0008 PQ-TLS"],"award-info":[{"award-number":["ANR-22-PETQ-0008 PQ-TLS"]}],"id":[{"id":"10.13039\/501100001665","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["ietresearch.onlinelibrary.wiley.com"],"crossmark-restriction":true},"short-container-title":["IET Information Security"],"published-print":{"date-parts":[[2023,1]]},"abstract":"<jats:p>Facing the potential threat raised by quantum computing, a great deal of research from many groups and industrial giants has gone into building public\u2010key post\u2010quantum cryptographic primitives that are resistant to the quantum attackers. Among them, there is a large number of post\u2010quantum key encapsulation mechanisms (KEMs), whose purpose is to provide a secure key exchange, which is a very crucial component in public\u2010key cryptography. This paper presents a formal security analysis of three lattice\u2010based KEMs including Kyber, Saber, and SK\u2010MLWR. We use Maude, a specification language supporting equational and rewriting logic and a high\u2010performance 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\u2010based 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\u2010in\u2010the\u2010middle 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.<\/jats:p>","DOI":"10.1049\/2023\/9399887","type":"journal-article","created":{"date-parts":[[2023,10,30]],"date-time":"2023-10-30T20:20:06Z","timestamp":1698697206000},"update-policy":"https:\/\/doi.org\/10.1002\/crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Kyber, Saber, and SK\u2010MLWR Lattice\u2010Based Key Encapsulation Mechanisms Model Checking with Maude"],"prefix":"10.1049","volume":"2023","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7092-2084","authenticated-orcid":false,"given":"Duong Dinh","family":"Tran","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4441-3259","authenticated-orcid":false,"given":"Kazuhiro","family":"Ogata","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3550-4781","authenticated-orcid":false,"given":"Santiago","family":"Escobar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7005-6489","authenticated-orcid":false,"given":"Sedat","family":"Akleylek","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8176-8692","authenticated-orcid":false,"given":"Ayoub","family":"Otmani","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"265","published-online":{"date-parts":[[2023,10,30]]},"reference":[{"key":"e_1_2_14_1_2","doi-asserted-by":"crossref","unstructured":"ShorP. W. Algorithms for quantum computation: discrete logarithms and factoring Proceedings 35th Annual Symposium on Foundations of Computer Science November 1994 Santa Fe NM USA IEEE 124\u2013134 https:\/\/doi.org\/10.1109\/SFCS.1994.365700.","DOI":"10.1109\/SFCS.1994.365700"},{"key":"e_1_2_14_2_2","doi-asserted-by":"crossref","unstructured":"GroverL. K. A fast quantum mechanical algorithm for database search STOC \u201996: Proceedings of the Twenty-Eighth Annual ACM Symposium on Theory of Computing July 1996 New York NY USA Association for Computing Machinery 212\u2013219 https:\/\/doi.org\/10.1145\/237814.237866 2-s2.0-0029701737.","DOI":"10.1145\/237814.237866"},{"key":"e_1_2_14_3_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28641-4_2"},{"key":"e_1_2_14_4_2","doi-asserted-by":"crossref","unstructured":"BosJ. DucasL. KiltzE. LepointT. LyubashevskyV. SchanckJ. M. SchwabeP. SeilerG. andStehleD. CRYSTALS - kyber: a CCA-secure module-lattice-based KEM 2018 IEEE European Symposium on Security and Privacy (EuroS&P) April 2018 London UK IEEE 353\u2013367 https:\/\/doi.org\/10.1109\/EuroSP.2018.00032 2-s2.0-85050764372.","DOI":"10.1109\/EuroSP.2018.00032"},{"key":"e_1_2_14_5_2","doi-asserted-by":"crossref","unstructured":"D.\u2019AnversJ. P. KarmakarA. Sinha RoyS. andVercauterenF. JouxA. NitajA. andRachidiT. Saber: Module-LWR based key exchange CPA-secure encryption and CCA-secure KEM 10831 Progress in Cryptology - AFRICACRYPT. 2018 - International Conference on Cryptology in Africa Marrakesh May 2018 Morocco Springer Cham 282\u2013305 Lecture Notes in Computer Science https:\/\/doi.org\/10.1007\/978-3-319-89339-6_16 2-s2.0-85045905925.","DOI":"10.1007\/978-3-319-89339-6_16"},{"key":"e_1_2_14_6_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.csi.2021.103549"},{"key":"e_1_2_14_7_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2019.100497"},{"key":"e_1_2_14_8_2","doi-asserted-by":"publisher","DOI":"10.1109\/TIT.1983.1056650"},{"key":"e_1_2_14_9_2","unstructured":"TranD. D. OgataK. EscobarS. AkleylekS. andOtmaniA. AkleylekS. EscobarS. OgataK. andOtmaniA. Formal specification and model checking of lattice-based key encapsulation mechanisms in maude 3280 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) October 2022 Madrid Spain 16\u201332 CEUR Workshop Proceedings."},{"key":"e_1_2_14_10_2","doi-asserted-by":"crossref","unstructured":"TranD. D. OgataK. EscobarS. AkleylekS. andOtmaniA. Formal specification and model checking of saber lattice-based key encapsulation mechanism in maude The 34th International Conference on Software Engineering and Knowledge Engineering SEKE 2022 KSIR Virtual Conference Center USA July 2022 KSI Research Inc 382\u2013387 https:\/\/doi.org\/10.18293\/SEKE2022-097.","DOI":"10.18293\/SEKE2022-097"},{"key":"e_1_2_14_11_2","unstructured":"AvanziR. BosJ. DucasL. KiltzE. LepointT. LyubashevskyV. SchanckJ. M. SchwabeP. SeilerG. andStehl\u00e9D. CRYSTALS-Kyber: algorithm specifications and supporting documentation (version 3.02) 2021 https:\/\/pq-crystals.org\/kyber\/data\/kyber-specification-round3-20210804.pdf."},{"key":"e_1_2_14_12_2","unstructured":"BassoA. MeraJ. M. B. D\u2019AnversJ.-P. KarmakarA. RoyS. S. BeirendonckM. V. andVercauterenF. SABER: Mod-LWR based KEM (round 3 submission) 2017 https:\/\/www.esat.kuleuven.be\/cosic\/pqcrypto\/saber\/files\/saberspecround3.pdf."},{"key":"e_1_2_14_13_2","unstructured":"CampagnaM.andCrockettE. Hybrid post-quantum key encapsulation methods (PQ KEM) for transport layer security 1.2 (TLS) 2021 RFC Editorhttps:\/\/datatracker.ietf.org\/doc\/html\/draft-campagna-tls-bike-sike-hybrid."},{"key":"e_1_2_14_14_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-75670-5_1"},{"key":"e_1_2_14_15_2","doi-asserted-by":"publisher","DOI":"10.1155\/2017\/1740572"},{"key":"e_1_2_14_16_2","unstructured":"DingJ. BrancoP. andSchmittK. Key exchange and authenticated key exchange with reusable keys based on RLWE assumption Cryptology ePrint Archive 2019 665."},{"key":"e_1_2_14_17_2","first-page":"5881","volume-title":"32nd USENIX Security Symposium (USENIX Security 23","author":"Jacomme C.","year":"2023"},{"key":"e_1_2_14_18_2","doi-asserted-by":"crossref","unstructured":"H\u00fclsingA. NingK.-C. SchwabeP. WeberF. andZimmermannP. R. Post-quantum WireGuard 2021 IEEE Symposium on Security and Privacy (SP) May 2021 San Francisco CA USA IEEE 304\u2013321 https:\/\/doi.org\/10.1109\/SP40001.2021.00030.","DOI":"10.1109\/SP40001.2021.00030"},{"key":"e_1_2_14_19_2","unstructured":"SelanderG. MattssonJ. P. andPalombiniF. Ephemeral Diffie\u2013Hellman 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\/."},{"key":"e_1_2_14_20_2","first-page":"3935","volume-title":"31st USENIX Security Symposium (USENIX Security 22","author":"Cheval V.","year":"2022"},{"key":"e_1_2_14_21_2","doi-asserted-by":"crossref","unstructured":"BlanchetB. ChevalV. andCortierV. ProVerif with lemmas induction fast subsumption and much more 2022 IEEE Symposium on Security and Privacy (SP) May 2022 San Francisco CA USA IEEE 69\u201386 https:\/\/doi.org\/10.1109\/SP46214.2022.9833653.","DOI":"10.1109\/SP46214.2022.9833653"},{"key":"e_1_2_14_22_2","doi-asserted-by":"publisher","DOI":"10.1145\/3157831.3157835"},{"key":"e_1_2_14_23_2","doi-asserted-by":"crossref","unstructured":"DonenfeldJ. A. WireGuard: next generation kernel network tunnel Proceedings of the Network and Distributed System Security Symposium NDSS 2017 2017 San Diego CA USA https:\/\/doi.org\/10.14722\/ndss.2017.23160.","DOI":"10.14722\/ndss.2017.23160"},{"key":"e_1_2_14_24_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03829-7_1"},{"key":"e_1_2_14_25_2","volume-title":"Scyther - semantics and verification of security protocols","author":"Cremers C. J. F.","year":"2006"},{"key":"e_1_2_14_26_2","doi-asserted-by":"publisher","DOI":"10.1561\/3300000004"},{"key":"e_1_2_14_27_2","doi-asserted-by":"crossref","unstructured":"ThayerF. J. T. HerzogJ. C. andGuttmanJ. D. Strand spaces: why is a security protocol correct? Proceedings. 1998 IEEE Symposium on Security and Privacy (Cat. No.98CB36186) May 1998 Oakland CA USA IEEE 160\u2013171 https:\/\/doi.org\/10.1109\/SECPRI.1998.674832.","DOI":"10.1109\/SECPRI.1998.674832"},{"key":"e_1_2_14_28_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2014.07.007"},{"key":"e_1_2_14_29_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45610-4_2"},{"key":"e_1_2_14_30_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-981-13-2372-0_22"},{"key":"e_1_2_14_31_2","unstructured":"LeiX.andLiaoX. NTRU-KE: a lattice-based public key exchange protocol Cryptology ePrint Archive 2013 http:\/\/eprint.iacr.org\/2013\/718 718."},{"key":"e_1_2_14_32_2","first-page":"1","volume-title":"Software Safety and Security - Tools for Analysis and Verification. vol. 33 of NATO Science for Peace and Security Series - D: Information and Communication Security","author":"Blanchet B.","year":"2012"},{"key":"e_1_2_14_33_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22792-9_5"},{"key":"e_1_2_14_34_2","first-page":"146","volume-title":"Foundations of Security Analysis and Design VII","author":"Barthe G.","year":"2013"},{"key":"e_1_2_14_35_2","doi-asserted-by":"crossref","unstructured":"BlanchetB. Automatically verified mechanized proof of one-encryption key exchange 2012 IEEE 25th Computer Security Foundations Symposium June 2012 Cambridge MA USA IEEE 325\u2013339 https:\/\/doi.org\/10.1109\/CSF.2012.8 2-s2.0-84866904130.","DOI":"10.1109\/CSF.2012.8"},{"key":"e_1_2_14_36_2","doi-asserted-by":"crossref","unstructured":"BressonE. ChevassutO. andPointchevalD. Security proofs for an efficient password-based key exchange CCS \u201903: Proceedings of the 10th ACM Conference on Computer and Communications Security October 2003 New York NY USA Association for Computing Machinery 241\u2013250 https:\/\/doi.org\/10.1145\/948109.948142.","DOI":"10.1145\/948109.948142"},{"key":"e_1_2_14_37_2","doi-asserted-by":"crossref","unstructured":"BellovinS. M.andMerrittM. Encrypted key exchange: password-based protocols secure against dictionary attacks Proceedings of the IEEE Symposium on Research in Security and Privacy May 1992 Oakland CA USA IEEE 72\u201384 https:\/\/doi.org\/10.1109\/RISP.1992.213269.","DOI":"10.1109\/RISP.1992.213269"},{"key":"e_1_2_14_38_2","unstructured":"KampanakisP. StebilaD. andHansenT. 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\/."}],"container-title":["IET Information Security"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/downloads.hindawi.com\/journals\/ietis\/2023\/9399887.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/downloads.hindawi.com\/journals\/ietis\/2023\/9399887.xml","content-type":"application\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/ietresearch.onlinelibrary.wiley.com\/doi\/pdf\/10.1049\/2023\/9399887","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,11,5]],"date-time":"2025-11-05T16:50:09Z","timestamp":1762361409000},"score":1,"resource":{"primary":{"URL":"https:\/\/ietresearch.onlinelibrary.wiley.com\/doi\/10.1049\/2023\/9399887"}},"subtitle":[],"editor":[{"given":"Thomas","family":"Haines","sequence":"additional","affiliation":[],"role":[{"role":"editor","vocabulary":"crossref"}]}],"short-title":[],"issued":{"date-parts":[[2023,1]]},"references-count":38,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2023,1]]}},"alternative-id":["10.1049\/2023\/9399887"],"URL":"https:\/\/doi.org\/10.1049\/2023\/9399887","archive":["Portico"],"relation":{},"ISSN":["1751-8709","1751-8717"],"issn-type":[{"value":"1751-8709","type":"print"},{"value":"1751-8717","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,1]]},"assertion":[{"value":"2023-06-13","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2023-09-11","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2023-10-30","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}],"article-number":"9399887"}}