{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,4]],"date-time":"2026-04-04T18:21:04Z","timestamp":1775326864989,"version":"3.50.1"},"publisher-location":"Cham","reference-count":68,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031683787","type":"print"},{"value":"9783031683794","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"DOI":"10.1007\/978-3-031-68379-4_12","type":"book-chapter","created":{"date-parts":[[2024,8,15]],"date-time":"2024-08-15T20:17:23Z","timestamp":1723753043000},"page":"384-421","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":14,"title":["Formally Verifying Kyber"],"prefix":"10.1007","author":[{"given":"Jos\u00e9 Bacelar","family":"Almeida","sequence":"first","affiliation":[]},{"given":"Santiago","family":"Arranz Olmos","sequence":"additional","affiliation":[]},{"given":"Manuel","family":"Barbosa","sequence":"additional","affiliation":[]},{"given":"Gilles","family":"Barthe","sequence":"additional","affiliation":[]},{"given":"Fran\u00e7ois","family":"Dupressoir","sequence":"additional","affiliation":[]},{"given":"Benjamin","family":"Gr\u00e9goire","sequence":"additional","affiliation":[]},{"given":"Vincent","family":"Laporte","sequence":"additional","affiliation":[]},{"given":"Jean-Christophe","family":"L\u00e9chenet","sequence":"additional","affiliation":[]},{"given":"Cameron","family":"Low","sequence":"additional","affiliation":[]},{"given":"Tiago","family":"Oliveira","sequence":"additional","affiliation":[]},{"given":"Hugo","family":"Pacheco","sequence":"additional","affiliation":[]},{"given":"Miguel","family":"Quaresma","sequence":"additional","affiliation":[]},{"given":"Peter","family":"Schwabe","sequence":"additional","affiliation":[]},{"given":"Pierre-Yves","family":"Strub","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,8,16]]},"reference":[{"key":"12_CR1","doi-asserted-by":"crossref","unstructured":"Alagic, G., et al.: Status report on the third round of the NIST post-quantum cryptography standardization process. NISTIR 8413 (2022). https:\/\/csrc.nist.gov\/publications\/detail\/nistir\/8413\/final","DOI":"10.6028\/NIST.IR.8413"},{"key":"12_CR2","unstructured":"Albrecht, M., Ducas, L.: Lattice attacks on NTRU and LWE: a history of refinements. Cryptology ePrint Archive, Report 2021\/799 (2021). https:\/\/eprint.iacr.org\/2021\/799"},{"key":"12_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1007\/978-3-319-56614-6_4","volume-title":"Advances in Cryptology \u2013 EUROCRYPT 2017","author":"MR Albrecht","year":"2017","unstructured":"Albrecht, M.R.: On dual lattice attacks against small-secret LWE and parameter choices in HElib and SEAL. In: Coron, J.-S., Nielsen, J.B. (eds.) EUROCRYPT 2017, Part II. LNCS, vol. 10211, pp. 103\u2013129. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-56614-6_4"},{"key":"12_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"717","DOI":"10.1007\/978-3-030-17656-3_25","volume-title":"Advances in Cryptology \u2013 EUROCRYPT 2019","author":"MR Albrecht","year":"2019","unstructured":"Albrecht, M.R., Ducas, L., Herold, G., Kirshanova, E., Postlethwaite, E.W., Stevens, M.: The general sieve kernel and new records in lattice reduction. In: Ishai, Y., Rijmen, V. (eds.) EUROCRYPT 2019, Part II. LNCS, vol. 11477, pp. 717\u2013746. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-17656-3_25"},{"key":"12_CR5","doi-asserted-by":"publisher","unstructured":"Almeida, J.B., et al.: Jasmin: high-assurance and high-speed cryptography. In: Thuraisingham, B.M., Evans, D., Malkin, T., Xu, D. (eds.) ACM CCS 2017, pp. 1807\u20131823. ACM Press (2017). https:\/\/doi.org\/10.1145\/3133956.3134078","DOI":"10.1145\/3133956.3134078"},{"key":"12_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1007\/978-3-662-52993-5_9","volume-title":"Fast Software Encryption","author":"JB Almeida","year":"2016","unstructured":"Almeida, J.B., Barbosa, M., Barthe, G., Dupressoir, F.: Verifiable side-channel security of cryptographic implementations: constant-time MEE-CBC. In: Peyrin, T. (ed.) FSE 2016. LNCS, vol. 9783, pp. 163\u2013184. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-52993-5_9"},{"key":"12_CR7","doi-asserted-by":"publisher","unstructured":"Almeida, J.B., et al.: The last mile: high-assurance and high-speed cryptographic implementations. In: 2020 IEEE Symposium on Security and Privacy, pp. 965\u2013982. IEEE Computer Society Press (2020). https:\/\/doi.org\/10.1109\/SP40000.2020.00028","DOI":"10.1109\/SP40000.2020.00028"},{"issue":"3","key":"12_CR8","doi-asserted-by":"publisher","first-page":"164","DOI":"10.46586\/tches.v2023.i3.164-193","volume":"2023","author":"JB Almeida","year":"2023","unstructured":"Almeida, J.B., et al.: Formally verifying Kyber episode IV: implementation correctness. IACR TCHES 2023(3), 164\u2013193 (2023). https:\/\/doi.org\/10.46586\/tches.v2023.i3.164-193","journal-title":"IACR TCHES"},{"key":"12_CR9","doi-asserted-by":"publisher","unstructured":"Almeida, J.B., et al.: Machine-checked proofs for cryptographic standards: indifferentiability of sponge and secure high-assurance implementations of SHA-3. In: Cavallaro, L., Kinder, J., Wang, X., Katz, J. (eds.) ACM CCS 2019, pp. 1607\u20131622. ACM Press (2019). https:\/\/doi.org\/10.1145\/3319535.3363211","DOI":"10.1145\/3319535.3363211"},{"key":"12_CR10","unstructured":"Almeida, J.B., et al.: Formally verifying Kyber episode V: machine-checked IND-CCA security and correctness of ML-KEM in EasyCrypt. Cryptology ePrint Archive, Paper 2024\/843 (2024). https:\/\/eprint.iacr.org\/2024\/843"},{"key":"12_CR11","unstructured":"Avanzi, R., et al.: CRYSTALS-Kyber: algorithm specifications and supporting documentation (version 3.02). Round-3 submission to the NIST PQC standardization project (2021). https:\/\/pq-crystals.org\/kyber\/data\/kyber-specification-round3-20210804.pdf"},{"key":"12_CR12","doi-asserted-by":"publisher","unstructured":"Barbosa, M., et al.: SoK: computer-aided cryptography. In: 2021 IEEE Symposium on Security and Privacy, pp. 777\u2013795. IEEE Computer Society Press (2021). https:\/\/doi.org\/10.1109\/SP40001.2021.00008","DOI":"10.1109\/SP40001.2021.00008"},{"key":"12_CR13","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"358","DOI":"10.1007\/978-3-031-38554-4_12","volume-title":"CRYPTO 2023, Part V","author":"M Barbosa","year":"2023","unstructured":"Barbosa, M., et al.: Fixing and mechanizing the security proof of Fiat-Shamir with aborts and Dilithium. In: Handschuh, H., Lysyanskaya, A. (eds.) CRYPTO 2023, Part V. LNCS, vol. 14085, pp. 358\u2013389. Springer, Heidelberg (2023). https:\/\/doi.org\/10.1007\/978-3-031-38554-4_12"},{"key":"12_CR14","doi-asserted-by":"publisher","unstructured":"Barbosa, M., et al.: EasyPQC: verifying post-quantum cryptography. In: Vigna, G., Shi, E. (eds.) ACM CCS 2021, pp. 2564\u20132586. ACM Press (2021). https:\/\/doi.org\/10.1145\/3460120.3484567","DOI":"10.1145\/3460120.3484567"},{"key":"12_CR15","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"421","DOI":"10.1007\/978-3-031-38554-4_14","volume-title":"CRYPTO 2023, Part V","author":"M Barbosa","year":"2023","unstructured":"Barbosa, M., Dupressoir, F., Gr\u00e9goire, B., H\u00fclsing, A., Meijers, M., Strub, P.Y.: Machine-checked security for XMSS as in RFC 8391 and $${\\text{ SPHINCS }}^{+}$$. In: Handschuh, H., Lysyanskaya, A. (eds.) CRYPTO 2023, Part V. LNCS, vol. 14085, pp. 421\u2013454. Springer, Heidelberg (2023). https:\/\/doi.org\/10.1007\/978-3-031-38554-4_14"},{"key":"12_CR16","unstructured":"Barbosa, M., H\u00fclsing, A.: The security of Kyber\u2019s FO-transform. Cryptology ePrint Archive, Report 2023\/755 (2023). https:\/\/eprint.iacr.org\/2023\/755"},{"key":"12_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1007\/978-3-319-10082-1_6","volume-title":"Foundations of Security Analysis and Design VII","author":"G Barthe","year":"2014","unstructured":"Barthe, G., Dupressoir, F., Gr\u00e9goire, B., Kunz, C., Schmidt, B., Strub, P.-Y.: EasyCrypt: a tutorial. In: Aldini, A., Lopez, J., Martinelli, F. (eds.) FOSAD 2012-2013. LNCS, vol. 8604, pp. 146\u2013166. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-10082-1_6"},{"key":"12_CR18","doi-asserted-by":"publisher","unstructured":"Barthe, G., Fan, X., Gancher, J., Gr\u00e9goire, B., Jacomme, C., Shi, E.: Symbolic proofs for lattice-based cryptography. In: Lie, D., Mannan, M., Backes, M., Wang, X. (eds.) ACM CCS 2018, pp. 538\u2013555. ACM Press (2018). https:\/\/doi.org\/10.1145\/3243734.3243825","DOI":"10.1145\/3243734.3243825"},{"key":"12_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1007\/978-3-642-22792-9_5","volume-title":"Advances in Cryptology \u2013 CRYPTO 2011","author":"G Barthe","year":"2011","unstructured":"Barthe, G., Gr\u00e9goire, B., Heraud, S., B\u00e9guelin, S.Z.: Computer-aided security proofs for the working cryptographer. In: Rogaway, P. (ed.) CRYPTO 2011. LNCS, vol. 6841, pp. 71\u201390. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22792-9_5"},{"key":"12_CR20","doi-asserted-by":"crossref","unstructured":"Becker, A., Ducas, L., Gama, N., Laarhoven, T.: New directions in nearest neighbor searching with applications to lattice sieving. In: SODA 2016: Proceedings of the Twenty-Seventh Annual ACM-SIAM Symposium on Discrete Algorithms, pp. 10\u201324. Society for Industrial and Applied Mathematics (2016)","DOI":"10.1137\/1.9781611974331.ch2"},{"key":"12_CR21","unstructured":"Beringer, L., Petcher, A., Ye, K.Q., Appel, A.W.: Verified correctness and security of OpenSSL HMAC. In: Jung, J., Holz, T. (eds.) USENIX Security 2015, pp. 207\u2013221. USENIX Association (2015)"},{"key":"12_CR22","unstructured":"Bernstein, D.J., Persichetti, E.: Towards KEM unification. Cryptology ePrint Archive, Report 2018\/526 (2018). https:\/\/eprint.iacr.org\/2018\/526"},{"key":"12_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/978-3-030-36033-7_3","volume-title":"Theory of Cryptography","author":"N Bindel","year":"2019","unstructured":"Bindel, N., Hamburg, M., H\u00f6velmanns, K., H\u00fclsing, A., Persichetti, E.: Tighter proofs of CCA security in the quantum random oracle model. In: Hofheinz, D., Rosen, A. (eds.) TCC 2019, Part II. LNCS, vol. 11892, pp. 61\u201390. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-36033-7_3"},{"key":"12_CR24","unstructured":"Blanchette, J., Mahboubi, A. (eds.): Handbook of Proof Assistants. Springer (2025, to appear)"},{"key":"12_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/978-3-642-25385-0_3","volume-title":"Advances in Cryptology \u2013 ASIACRYPT 2011","author":"D Boneh","year":"2011","unstructured":"Boneh, D., Dagdelen, \u00d6., Fischlin, M., Lehmann, A., Schaffner, C., Zhandry, M.: Random oracles in a quantum world. In: Lee, D.H., Wang, X. (eds.) ASIACRYPT 2011. LNCS, vol. 7073, pp. 41\u201369. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-25385-0_3"},{"key":"12_CR26","doi-asserted-by":"crossref","unstructured":"Bos, J., et al.: CRYSTALS \u2013 Kyber: a CCA-secure module-lattice-based KEM. In: 2018 IEEE European Symposium on Security and Privacy, EuroS &P 2018, pp. 353\u2013367. IEEE (2018). https:\/\/eprint.iacr.org\/2017\/634","DOI":"10.1109\/EuroSP.2018.00032"},{"key":"12_CR27","doi-asserted-by":"publisher","unstructured":"Cremers, C., Fontaine, C., Jacomme, C.: A logic and an interactive prover for the computational post-quantum security of protocols. In: 2022 IEEE Symposium on Security and Privacy, pp. 125\u2013141. IEEE Computer Society Press (2022). https:\/\/doi.org\/10.1109\/SP46214.2022.9833800","DOI":"10.1109\/SP46214.2022.9833800"},{"key":"12_CR28","unstructured":"D\u2019Anvers, J.P., et al.: SABER. Technical report, National Institute of Standards and Technology (2020). https:\/\/csrc.nist.gov\/projects\/post-quantum-cryptography\/post-quantum-cryptography-standardization\/round-3-submissions"},{"key":"12_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/978-3-319-78381-9_5","volume-title":"Advances in Cryptology \u2013 EUROCRYPT 2018","author":"L Ducas","year":"2018","unstructured":"Ducas, L.: Shortest vector from lattice sieving: a few dimensions for free. In: Nielsen, J.B., Rijmen, V. (eds.) EUROCRYPT 2018, Part I. LNCS, vol. 10820, pp. 125\u2013145. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-78381-9_5"},{"key":"12_CR30","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1007\/978-3-031-38548-3_2","volume-title":"CRYPTO 2023, Part III","author":"L Ducas","year":"2023","unstructured":"Ducas, L., Pulles, L.N.: Does the dual-sieve attack on learning with errors even work? In: Handschuh, H., Lysyanskaya, A. (eds.) CRYPTO 2023, Part III. LNCS, vol. 14083, pp. 37\u201369. Springer, Heidelberg (2023). https:\/\/doi.org\/10.1007\/978-3-031-38548-3_2"},{"key":"12_CR31","doi-asserted-by":"publisher","unstructured":"Duman, J., H\u00f6velmanns, K., Kiltz, E., Lyubashevsky, V., Seiler, G.: Faster lattice-based KEMs via a generic Fujisaki-Okamoto transform using prefix hashing. In: Vigna, G., Shi, E. (eds.) ACM CCS 2021, pp. 2722\u20132737. ACM Press (2021). https:\/\/doi.org\/10.1145\/3460120.3484819","DOI":"10.1145\/3460120.3484819"},{"key":"12_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"537","DOI":"10.1007\/3-540-48405-1_34","volume-title":"Advances in Cryptology \u2014 CRYPTO\u2019 99","author":"E Fujisaki","year":"1999","unstructured":"Fujisaki, E., Okamoto, T.: Secure integration of asymmetric and symmetric encryption schemes. In: Wiener, M. (ed.) CRYPTO 1999. LNCS, vol. 1666, pp. 537\u2013554. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48405-1_34"},{"issue":"1","key":"12_CR33","doi-asserted-by":"publisher","first-page":"80","DOI":"10.1007\/s00145-011-9114-1","volume":"26","author":"E Fujisaki","year":"2013","unstructured":"Fujisaki, E., Okamoto, T.: Secure integration of asymmetric and symmetric encryption schemes. J. Cryptol. 26(1), 80\u2013101 (2013). https:\/\/doi.org\/10.1007\/s00145-011-9114-1","journal-title":"J. Cryptol."},{"key":"12_CR34","doi-asserted-by":"publisher","unstructured":"Gentry, C., Peikert, C., Vaikuntanathan, V.: Trapdoors for hard lattices and new cryptographic constructions. In: Ladner, R.E., Dwork, C. (eds.) 40th ACM STOC, pp. 197\u2013206. ACM Press (2008). https:\/\/doi.org\/10.1145\/1374376.1374407","DOI":"10.1145\/1374376.1374407"},{"key":"12_CR35","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"402","DOI":"10.1007\/978-3-031-07082-2_15","volume-title":"EUROCRYPT 2022, Part III","author":"P Grubbs","year":"2022","unstructured":"Grubbs, P., Maram, V., Paterson, K.G.: Anonymous, robust post-quantum public key encryption. In: Dunkelman, O., Dziembowski, S. (eds.) EUROCRYPT 2022, Part III. LNCS, vol. 13277, pp. 402\u2013432. Springer, Heidelberg (2022). https:\/\/doi.org\/10.1007\/978-3-031-07082-2_15"},{"key":"12_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/978-3-030-92068-5_2","volume-title":"Advances in Cryptology \u2013 ASIACRYPT 2021","author":"Q Guo","year":"2021","unstructured":"Guo, Q., Johansson, T.: Faster dual lattice attacks for\u00a0solving LWE with\u00a0applications to\u00a0CRYSTALS. In: Tibouchi, M., Wang, H. (eds.) ASIACRYPT 2021, Part IV. LNCS, vol. 13093, pp. 33\u201362. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-92068-5_2"},{"key":"12_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/978-3-030-56880-1_13","volume-title":"Advances in Cryptology \u2013 CRYPTO 2020","author":"Q Guo","year":"2020","unstructured":"Guo, Q., Johansson, T., Nilsson, A.: A key-recovery timing attack on post-quantum primitives using the Fujisaki-Okamoto transformation and its application on FrodoKEM. In: Micciancio, D., Ristenpart, T. (eds.) CRYPTO 2020, Part II. LNCS, vol. 12171, pp. 359\u2013386. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-56880-1_13"},{"key":"12_CR38","doi-asserted-by":"publisher","unstructured":"Hamburg, M., et al.: Chosen ciphertext k-trace attacks on masked CCA2 secure kyber. IACR TCHES 2021(4), 88\u2013113 (2021). https:\/\/doi.org\/10.46586\/tches.v2021.i4.88-113. https:\/\/tches.iacr.org\/index.php\/TCHES\/article\/view\/9061","DOI":"10.46586\/tches.v2021.i4.88-113"},{"key":"12_CR39","doi-asserted-by":"publisher","unstructured":"Hermelink, J., M\u00e5rtensson, E., Samardjiska, S., Pessl, P., Rodosek, G.D.: Belief propagation meets lattice reduction: security estimates for error-tolerant key recovery from decryption errors. IACR TCHES 2023(4), 287\u2013317 (2023). https:\/\/doi.org\/10.46586\/tches.v2023.i4.287-317","DOI":"10.46586\/tches.v2023.i4.287-317"},{"key":"12_CR40","doi-asserted-by":"publisher","unstructured":"Hermelink, J., Streit, S., Strieder, E., Thieme, K.: Adapting belief propagation to counter shuffling of NTTs. IACR TCHES 2023(1), 60\u201388 (2023). https:\/\/doi.org\/10.46586\/tches.v2023.i1.60-88","DOI":"10.46586\/tches.v2023.i1.60-88"},{"key":"12_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1007\/978-3-319-70500-2_12","volume-title":"Theory of Cryptography","author":"D Hofheinz","year":"2017","unstructured":"Hofheinz, D., H\u00f6velmanns, K., Kiltz, E.: A modular analysis of the Fujisaki-Okamoto transformation. In: Kalai, Y., Reyzin, L. (eds.) TCC 2017, Part I. LNCS, vol. 10677, pp. 341\u2013371. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-70500-2_12"},{"key":"12_CR42","unstructured":"Hofheinz, D., H\u00f6velmanns, K., Kiltz, E.: A modular analysis of the Fujisaki-Okamoto transformation. Cryptology ePrint Archive, Report 2017\/604 (2017). https:\/\/eprint.iacr.org\/2017\/604"},{"key":"12_CR43","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"414","DOI":"10.1007\/978-3-031-22972-5_15","volume-title":"ASIACRYPT 2022, Part IV","author":"K H\u00f6velmanns","year":"2022","unstructured":"H\u00f6velmanns, K., H\u00fclsing, A., Majenz, C.: Failing gracefully: Decryption failures and the Fujisaki-Okamoto transform. In: Agrawal, S., Lin, D. (eds.) ASIACRYPT 2022, Part IV. LNCS, vol. 13794, pp. 414\u2013443. Springer, Heidelberg (2022). https:\/\/doi.org\/10.1007\/978-3-031-22972-5_15"},{"key":"12_CR44","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"389","DOI":"10.1007\/978-3-030-45388-6_14","volume-title":"Public-Key Cryptography \u2013 PKC 2020","author":"K H\u00f6velmanns","year":"2020","unstructured":"H\u00f6velmanns, K., Kiltz, E., Sch\u00e4ge, S., Unruh, D.: Generic authenticated key exchange in\u00a0the quantum random oracle model. In: Kiayias, A., Kohlweiss, M., Wallden, P., Zikas, V. (eds.) PKC 2020. LNCS, vol. 12111, pp. 389\u2013422. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-45388-6_14"},{"key":"12_CR45","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"622","DOI":"10.1007\/978-3-031-15802-5_22","volume-title":"CRYPTO 2022, Part I","author":"A H\u00fclsing","year":"2022","unstructured":"H\u00fclsing, A., Meijers, M., Strub, P.Y.: Formal verification of Saber\u2019s public-key encryption scheme in EasyCrypt. In: Dodis, Y., Shrimpton, T. (eds.) CRYPTO 2022, Part I. LNCS, vol. 13507, pp. 622\u2013653. Springer, Heidelberg (2022). https:\/\/doi.org\/10.1007\/978-3-031-15802-5_22"},{"key":"12_CR46","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"96","DOI":"10.1007\/978-3-319-96878-0_4","volume-title":"Advances in Cryptology \u2013 CRYPTO 2018","author":"H Jiang","year":"2018","unstructured":"Jiang, H., Zhang, Z., Chen, L., Wang, H., Ma, Z.: IND-CCA-secure key encapsulation mechanism in the quantum random oracle model, revisited. In: Shacham, H., Boldyreva, A. (eds.) CRYPTO 2018, Part III. LNCS, vol. 10993, pp. 96\u2013125. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96878-0_4"},{"key":"12_CR47","unstructured":"Kreuzer, K.: Verification of correctness and security properties for CRYSTALS-KYBER. Cryptology ePrint Archive, Report 2023\/087 (2023). https:\/\/eprint.iacr.org\/2023\/087"},{"key":"12_CR48","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-13190-5_1","volume-title":"Advances in Cryptology \u2013 EUROCRYPT 2010","author":"V Lyubashevsky","year":"2010","unstructured":"Lyubashevsky, V., Peikert, C., Regev, O.: On ideal lattices and learning with errors over rings. In: Gilbert, H. (ed.) EUROCRYPT 2010. LNCS, vol. 6110, pp. 1\u201323. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-13190-5_1"},{"key":"12_CR49","doi-asserted-by":"crossref","unstructured":"Lyubashevsky, V., Peikert, C., Regev, O.: On ideal lattices and learning with errors over rings. Slides of the talk given by Chris Peikert at Eurocrypt 2010 (2010). https:\/\/iacr.org\/conferences\/eurocrypt2010\/talks\/slides-ideal-lwe.pdf","DOI":"10.1007\/978-3-642-13190-5_1"},{"key":"12_CR50","unstructured":"Lyubashevsky, V., Peikert, C., Regev, O.: On ideal lattices and learning with errors over rings. Cryptology ePrint Archive, Report 2012\/230 (2012). https:\/\/eprint.iacr.org\/2012\/230"},{"key":"12_CR51","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-031-31368-4_1","volume-title":"PKC 2023, Part I","author":"V Maram","year":"2023","unstructured":"Maram, V., Xagawa, K.: Post-quantum anonymity of Kyber. In: Boldyreva, A., Kolesnikov, V. (eds.) PKC 2023, Part I. LNCS, vol. 13940, pp. 3\u201335. Springer, Heidelberg (2023). https:\/\/doi.org\/10.1007\/978-3-031-31368-4_1"},{"key":"12_CR52","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"700","DOI":"10.1007\/978-3-642-29011-4_41","volume-title":"Advances in Cryptology \u2013 EUROCRYPT 2012","author":"D Micciancio","year":"2012","unstructured":"Micciancio, D., Peikert, C.: Trapdoors for lattices: simpler, tighter, faster, smaller. In: Pointcheval, D., Johansson, T. (eds.) EUROCRYPT 2012. LNCS, vol. 7237, pp. 700\u2013718. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-29011-4_41"},{"key":"12_CR53","doi-asserted-by":"crossref","unstructured":"Micciancio, D., Voulgaris, P.: Faster exponential time algorithms for the shortest vector problem. In: SODA 2010: Proceedings of the Twenty-First Annual ACM-SIAM Symposium on Discrete Algorithms, pp. 1468\u20131480. Society for Industrial and Applied Mathematics (2010)","DOI":"10.1137\/1.9781611973075.119"},{"key":"12_CR54","unstructured":"National Institute of Standards and Technology: FIPS PUB 202 \u2013 SHA-3 standard: Permutation-based hash and extendable-output functions (2015). http:\/\/nvlpubs.nist.gov\/nistpubs\/FIPS\/NIST.FIPS.202.pdf"},{"key":"12_CR55","unstructured":"National Institute of Standards and Technology: FIPS PUB 203 (Initial Public Draft) \u2013 module-lattice-based key-encapsulation mechanism standard (2023). https:\/\/csrc.nist.gov\/pubs\/fips\/203\/ipd"},{"key":"12_CR56","doi-asserted-by":"publisher","unstructured":"Ngo, K., Dubrova, E., Guo, Q., Johansson, T.: A side-channel attack on a masked IND-CCA secure saber KEM implementation. IACR TCHES 2021(4), 676\u2013707 (2021). https:\/\/doi.org\/10.46586\/tches.v2021.i4.676-707. https:\/\/tches.iacr.org\/index.php\/TCHES\/article\/view\/9079","DOI":"10.46586\/tches.v2021.i4.676-707"},{"key":"12_CR57","doi-asserted-by":"publisher","unstructured":"Nguyen, P.Q., Vidick, T.: Sieve algorithms for the shortest vector problem are practical. J. Math. Crypt. 181\u2013207 (2008). https:\/\/doi.org\/10.1515\/JMC.2008.009","DOI":"10.1515\/JMC.2008.009"},{"key":"12_CR58","doi-asserted-by":"publisher","unstructured":"Pessl, P., Prokop, L.: Fault attacks on CCA-secure lattice KEMs. IACR TCHES 2021(2), 37\u201360 (2021). https:\/\/doi.org\/10.46586\/tches.v2021.i2.37-60. https:\/\/tches.iacr.org\/index.php\/TCHES\/article\/view\/8787","DOI":"10.46586\/tches.v2021.i2.37-60"},{"key":"12_CR59","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"513","DOI":"10.1007\/978-3-319-66787-4_25","volume-title":"Cryptographic Hardware and Embedded Systems \u2013 CHES 2017","author":"R Primas","year":"2017","unstructured":"Primas, R., Pessl, P., Mangard, S.: Single-trace side-channel attacks on masked lattice-based encryption. In: Fischer, W., Homma, N. (eds.) CHES 2017. LNCS, vol. 10529, pp. 513\u2013533. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66787-4_25"},{"key":"12_CR60","unstructured":"Saito, T., Xagawa, K., Yamakawa, T.: Tightly-secure key-encapsulation mechanism in the quantum random oracle model. Cryptology ePrint Archive, Report 2017\/1005 (2017). https:\/\/eprint.iacr.org\/2017\/1005"},{"key":"12_CR61","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"520","DOI":"10.1007\/978-3-319-78372-7_17","volume-title":"Advances in Cryptology \u2013 EUROCRYPT 2018","author":"T Saito","year":"2018","unstructured":"Saito, T., Xagawa, K., Yamakawa, T.: Tightly-secure key-encapsulation mechanism in the quantum random oracle model. In: Nielsen, J.B., Rijmen, V. (eds.) EUROCRYPT 2018, Part III. LNCS, vol. 10822, pp. 520\u2013551. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-78372-7_17"},{"key":"12_CR62","unstructured":"Schwabe, P., et al.: CRYSTALS-KYBER. Technical report, National Institute of Standards and Technology (2017). https:\/\/csrc.nist.gov\/projects\/post-quantum-cryptography\/post-quantum-cryptography-standardization\/round-1-submissions"},{"key":"12_CR63","unstructured":"Schwabe, P., et al.: CRYSTALS-KYBER. Technical report, National Institute of Standards and Technology (2022). https:\/\/csrc.nist.gov\/Projects\/post-quantum-cryptography\/selected-algorithms-2022"},{"key":"12_CR64","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"192","DOI":"10.1007\/978-3-662-53644-5_8","volume-title":"Theory of Cryptography","author":"EE Targhi","year":"2016","unstructured":"Targhi, E.E., Unruh, D.: Post-quantum security of the fujisaki-okamoto and OAEP transforms. In: Hirt, M., Smith, A. (eds.) TCC 2016, Part II. LNCS, vol. 9986, pp. 192\u2013216. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-53644-5_8"},{"key":"12_CR65","doi-asserted-by":"publisher","unstructured":"Unruh, D.: Quantum relational Hoare logic. Proc. ACM Program. Lang. 3(POPL), 33:1\u201333:31 (2019). https:\/\/doi.org\/10.1145\/3290346","DOI":"10.1145\/3290346"},{"key":"12_CR66","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1007\/978-3-030-64837-4_11","volume-title":"Advances in Cryptology \u2013 ASIACRYPT 2020","author":"D Unruh","year":"2020","unstructured":"Unruh, D.: Post-quantum verification of Fujisaki-Okamoto. In: Moriai, S., Wang, H. (eds.) ASIACRYPT 2020. LNCS, vol. 12491, pp. 321\u2013352. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-64837-4_11"},{"key":"12_CR67","doi-asserted-by":"publisher","unstructured":"Ye, K.Q., Green, M., Sanguansin, N., Beringer, L., Petcher, A., Appel, A.W.: Verified correctness and security of mbedTLS HMAC-DRBG. In: Thuraisingham, B.M., Evans, D., Malkin, T., Xu, D. (eds.) ACM CCS 2017, pp. 2007\u20132020. ACM Press (2017). https:\/\/doi.org\/10.1145\/3133956.3133974","DOI":"10.1145\/3133956.3133974"},{"key":"12_CR68","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1007\/978-3-030-26951-7_9","volume-title":"Advances in Cryptology \u2013 CRYPTO 2019","author":"M Zhandry","year":"2019","unstructured":"Zhandry, M.: How to record quantum queries, and applications to quantum indifferentiability. In: Boldyreva, A., Micciancio, D. (eds.) CRYPTO 2019, Part II. LNCS, vol. 11693, pp. 239\u2013268. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-26951-7_9"}],"container-title":["Lecture Notes in Computer Science","Advances in Cryptology \u2013 CRYPTO 2024"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-68379-4_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,8,15]],"date-time":"2024-08-15T20:19:34Z","timestamp":1723753174000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-68379-4_12"}},"subtitle":["Episode V: Machine-Checked IND-CCA Security and Correctness of ML-KEM in EasyCrypt"],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031683787","9783031683794"],"references-count":68,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-68379-4_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"16 August 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CRYPTO","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Annual International Cryptology Conference","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Santa Barbara, CA","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18 August 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 August 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"44","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"crypto2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/crypto.iacr.org\/2024\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}