{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,22]],"date-time":"2025-12-22T22:17:46Z","timestamp":1766441866238,"version":"3.48.0"},"publisher-location":"New York, NY, USA","reference-count":36,"publisher":"ACM","funder":[{"name":"Deutsche Forschungsgemeinschaft (DFG, German research Foundation)","award":["EXC 2092 CASA - 390781972"],"award-info":[{"award-number":["EXC 2092 CASA - 390781972"]}]},{"name":"German Federal Ministry of Education and Research (BMBF)","award":["16KISK038"],"award-info":[{"award-number":["16KISK038"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2025,11,19]]},"DOI":"10.1145\/3719027.3765218","type":"proceedings-article","created":{"date-parts":[[2025,11,22]],"date-time":"2025-11-22T23:33:16Z","timestamp":1763854396000},"page":"156-169","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Formally Verified Correctness Bounds for Lattice-Based Cryptography"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6848-5564","authenticated-orcid":false,"given":"Manuel","family":"Barbosa","sequence":"first","affiliation":[{"name":"University of Porto (FCUP), Porto, Portugal and INESC TEC, Porto, Portugal"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8215-4729","authenticated-orcid":false,"given":"Matthias J.","family":"Kannwischer","sequence":"additional","affiliation":[{"name":"Chelpis Quantum Tech, Taipei, Taiwan"}]},{"ORCID":"https:\/\/orcid.org\/0009-0002-5457-0685","authenticated-orcid":false,"given":"Thing-han","family":"Lim","sequence":"additional","affiliation":[{"name":"Academia Sinica, Taipei, Taiwan"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1310-0997","authenticated-orcid":false,"given":"Peter","family":"Schwabe","sequence":"additional","affiliation":[{"name":"MPI-SP, Bochum, Germany and Radboud University, Nijmegen, Netherlands"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8196-7875","authenticated-orcid":false,"given":"Pierre-Yves","family":"Strub","sequence":"additional","affiliation":[{"name":"PQShield, Paris, France"}]}],"member":"320","published-online":{"date-parts":[[2025,11,22]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"Agence nationale de la s\u00e9curit\u00e9 des syst\u00e8mes d'information (ANSSI). 2023. ANSSI Views on the Post-Quantum Cryptography Transition: Follow-up Position Paper. Technical Report. Agence nationale de la s\u00e9curit\u00e9 des syst\u00e8mes d'information (ANSSI). https:\/\/cyber.gouv.fr\/sites\/default\/files\/document\/follow_up_position_ paper_on_post_quantum_cryptography.pdf Accessed: 2025-02--11."},{"key":"e_1_3_2_1_2_1","unstructured":"Erdem Alkim Joppe Bos L\u00e9o Ducas Patrick Longa Ilya Mironov Michael Naehrig Valeria Nikolaenko Chris Peikert Ananth Raghunathan and Douglas Stebila. 2021. FrodoKEM Learning With Errors Key Encapsulation Algo- rithm Specifications And Supporting Documentation. https:\/\/frodokem.org\/ files\/FrodoKEM-specification-20210604.pdf Accessed: 2024--12--27."},{"key":"e_1_3_2_1_3_1","unstructured":"Erdem Alkim L\u00e9o Ducas Thomas P\u00f6ppelmann and Peter Schwabe. 2016. Post-quantum Key Exchange - A New Hope. 327--343."},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","unstructured":"Jos\u00e9 Bacelar Almeida Santiago Arranz Olmos Manuel Barbosa Gilles Barthe Fran\u00e7ois Dupressoir Benjamin Gr\u00e9goire Vincent Laporte Jean-Christophe L\u00e9ch- enet Cameron Low Tiago Oliveira Hugo Pacheco Miguel Quaresma Peter Schwabe and Pierre-Yves Strub. 2024. Formally Verifying Kyber - Episode V: Machine-Checked IND-CCA Security and Correctness of ML-KEM in EasyCrypt. 384--421. doi:10.1007\/978--3-031--68379--4_12","DOI":"10.1007\/978--3-031--68379--4_12"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.62056\/ahee0iuc"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","unstructured":"Gilles Barthe Benjamin Gr\u00e9goire Sylvain Heraud and Santiago Zanella B\u00e9guelin. 2011. Computer-Aided Security Proofs for the Working Cryptographer. 71--90. doi:10.1007\/978--3--642--22792--9_5","DOI":"10.1007\/978--3--642--22792--9_5"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978--3--319--89339--6_12"},{"key":"e_1_3_2_1_8_1","volume-title":"Ming-Shing Chen, Chitchanok Chuengsa- tiansup, Tanja Lange, Adrian Marotzke, Bo-Yuan Peng, Nicola Tuveri, Chris- tine van Vredendaal, and Bo-Yin Yang.","author":"Bernstein Daniel J.","year":"2020","unstructured":"Daniel J. Bernstein, Billy Bob Brumley, Ming-Shing Chen, Chitchanok Chuengsa- tiansup, Tanja Lange, Adrian Marotzke, Bo-Yuan Peng, Nicola Tuveri, Chris- tine van Vredendaal, and Bo-Yin Yang. 2020. NTRU Prime. Techni- cal Report. National Institute of Standards and Technology. avail- able at https:\/\/csrc.nist.gov\/projects\/post-quantum-cryptography\/post-quantum- cryptography-standardization\/round-3-submissions."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978--3-030--44223--1_12"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/EuroSP.2018.00032"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"crossref","unstructured":"Joppe W. Bos L\u00e9o Ducas Eike Kiltz Tancr\u00e8de Lepoint Vadim Lyubashevsky John M. Schanck Peter Schwabe Gregor Seiler and Damien Stehl\u00e9. 2018. CRYS- TALS - Kyber: A CCA-Secure Module-Lattice-Based KEM. 353--367. doi:10.1109\/ EuroSP.2018.00032","DOI":"10.1109\/EuroSP.2018.00032"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978--3-030--88238--9_5"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","unstructured":"Jan-Pieter D'Anvers and Senne Batsleer. 2022. Multitarget Decryption Failure Attacks and Their Application to Saber and Kyber. 3--33. doi:10.1007\/978--3-030-97121--2_1","DOI":"10.1007\/978--3-030-97121--2_1"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","unstructured":"Jan-Pieter D'Anvers Qian Guo Thomas Johansson Alexander Nilsson Frederik Vercauteren and Ingrid Verbauwhede. 2019. Decryption Failure Attacks on IND- CCA Secure Lattice-Based Schemes. 565--598. doi:10.1007\/978--3-030--17259--6_19","DOI":"10.1007\/978--3-030--17259--6_19"},{"key":"e_1_3_2_1_15_1","volume-title":"Frederik Ver- cauteren, Jose Maria Bermudo Mera, Michiel Van Beirendonck, and Andrea Basso.","author":"D'Anvers Jan-Pieter","year":"2020","unstructured":"Jan-Pieter D'Anvers, Angshuman Karmakar, Sujoy Sinha Roy, Frederik Ver- cauteren, Jose Maria Bermudo Mera, Michiel Van Beirendonck, and Andrea Basso. 2020. SABER. Technical Report. National Institute of Standards and Technology. available at https:\/\/csrc.nist.gov\/projects\/post-quantum-cryptography\/post- quantum-cryptography-standardization\/round-3-submissions."},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","unstructured":"Jan-Pieter D'Anvers M\u00e9lissa Rossi and Fernando Virdia. 2020. (One) Failure Is Not an Option: Bootstrapping the Search for Failures in Lattice-Based Encryption Schemes. 3--33. doi:10.1007\/978--3-030--45727--3_1","DOI":"10.1007\/978--3-030--45727--3_1"},{"key":"e_1_3_2_1_17_1","volume-title":"Angshuman Karmakar Sujoy Sinha Roy, and Frederik Vercauteren","author":"D'Anvers Jan-Pieter","year":"2018","unstructured":"Jan-Pieter D'Anvers, Angshuman Karmakar Sujoy Sinha Roy, and Frederik Vercauteren. 2018. Saber: Module-LWR based key exchange, CPA-secure en- cryption and CCA-secure KEM. Cryptology ePrint Archive, Report 2018\/230. https:\/\/eprint.iacr.org\/2018\/230"},{"key":"e_1_3_2_1_18_1","unstructured":"Jan-Pieter D'Anvers Frederik Vercauteren and Ingrid Verbauwhede. 2018. The impact of error dependencies on Ring\/Mod-LWE\/LWR based schemes. Cryptol- ogy ePrint Archive Report 2018\/1172. https:\/\/eprint.iacr.org\/2018\/1172"},{"key":"e_1_3_2_1_19_1","unstructured":"Jan-Pieter D'Anvers Frederik Vercauteren and Ingrid Verbauwhede. 2018. On the impact of decryption failures on the security of LWE\/LWR based schemes. Cryptology ePrint Archive Report 2018\/1089. https:\/\/eprint.iacr.org\/2018\/1089"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICC.2017.7996806"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"crossref","unstructured":"Jintai Ding Scott R. Fluhrer and Saraswathy RV. 2018. Complete Attack on RLWE Key Exchange with Reused Keys Without Signal Leakage. 467--486. doi:10.1007\/ 978--3--319--93638--3_27","DOI":"10.1007\/978-3-319-93638-3_27"},{"key":"e_1_3_2_1_22_1","unstructured":"Scott Fluhrer. 2016. Cryptanalysis of ring-LWE based key exchange with key share reuse. Cryptology ePrint Archive Report 2016\/085. https:\/\/eprint.iacr.org\/ 2016\/085"},{"key":"e_1_3_2_1_23_1","volume-title":"Cryptographic Mechanisms: Recommendations and Key Lengths. Technical Guide- line. https:\/\/www.bsi.bund.de\/SharedDocs\/Downloads\/EN\/BSI\/Publications\/TechGuidelines\/TG02102\/BSI-TR-02102--1.pdf.","author":"Information Federal Office","year":"2024","unstructured":"Federal Office for Information Security (BSI). 2024. Cryptographic Mechanisms: Recommendations and Key Lengths. Technical Guide- line. https:\/\/www.bsi.bund.de\/SharedDocs\/Downloads\/EN\/BSI\/Publications\/TechGuidelines\/TG02102\/BSI-TR-02102--1.pdf."},{"key":"e_1_3_2_1_24_1","unstructured":"FrodoKEM Team. 2024. FrodoKEM: Practical Quantum-Secure Key Encapsulation from Generic Lattices. https:\/\/frodokem.org\/ Accessed: 2024--12--27 see the ''News'' section.."},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","unstructured":"Eiichiro Fujisaki and Tatsuaki Okamoto. 1999. Secure Integration of Asymmetric and Symmetric Encryption Schemes. 537--554. doi:10.1007\/3--540--48405--1_34","DOI":"10.1007\/3--540--48405--1_34"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978--3-031--22972--5_15"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","unstructured":"Andreas H\u00fclsing Matthias Meijers and Pierre-Yves Strub. 2022. Formal Ver- ification of Saber's Public-Key Encryption Scheme in EasyCrypt. 622--653. doi:10.1007\/978--3-031--15802--5_22","DOI":"10.1007\/978--3-031--15802--5_22"},{"key":"e_1_3_2_1_28_1","unstructured":"Zhengzhong Jin and Yunlei Zhao. 2017. Optimal Key Consensus in Presence of Noise. Cryptology ePrint Archive Report 2017\/1058. https:\/\/eprint.iacr.org\/ 2017\/1058"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF61375.2024.00016"},{"key":"e_1_3_2_1_30_1","volume-title":"Ananth Raghunathan, and Douglas Stebila.","author":"Naehrig Michael","year":"2020","unstructured":"Michael Naehrig, Erdem Alkim, Joppe Bos, L\u00e9o Ducas, Karen Easterbrook, Brian LaMacchia, Patrick Longa, Ilya Mironov, Valeria Nikolaenko, Christo- pher Peikert, Ananth Raghunathan, and Douglas Stebila. 2020. FrodoKEM. Technical Report. National Institute of Standards and Technology. avail- able at https:\/\/csrc.nist.gov\/projects\/post-quantum-cryptography\/post-quantum- cryptography-standardization\/round-3-submissions."},{"key":"e_1_3_2_1_31_1","unstructured":"National Institute of Standards and Technology. 2024. FIPS PUB 203 -- ML- KEM: Module-Lattice-Based Key-Encapsulation Mechanism Standard. https: \/\/nvlpubs.nist.gov\/nistpubs\/FIPS\/NIST.FIPS.203.pdf."},{"key":"e_1_3_2_1_32_1","unstructured":"National Institute of Standards and Technology. 2024. FIPS PUB 204 -- ML- DSA: Module-Lattice-Based Digital Signature Standard. https:\/\/nvlpubs.nist.gov\/ nistpubs\/FIPS\/NIST.FIPS.204.pdf."},{"key":"e_1_3_2_1_33_1","unstructured":"National Institute of Standards and Technology. 2024. FIPS PUB 205 -- SLH- DSA: Stateless Hash-Based Digital Signature Standard. https:\/\/nvlpubs.nist.gov\/ nistpubs\/FIPS\/NIST.FIPS.205.pdf."},{"key":"e_1_3_2_1_34_1","unstructured":"NIST 2015. FIPS PUB 202 -- SHA-3 Standard: Permutation-Based Hash and Extendable-Output Functions. https:\/\/nvlpubs.nist.gov\/nistpubs\/FIPS\/NIST.FIPS. 202.pdf."},{"volume-title":"Technical Report","author":"Schwabe Peter","key":"e_1_3_2_1_35_1","unstructured":"Peter Schwabe, Roberto Avanzi, Joppe Bos, L\u00e9o Ducas, Eike Kiltz, Tancr\u00e8de Lepoint, Vadim Lyubashevsky, John M. Schanck, Gregor Seiler, and Damien Stehl\u00e9. 2020. CRYSTALS-KYBER. Technical Report. National Institute of Standards and Technology. available at https:\/\/csrc.nist.gov\/projects\/post-quantum-cryptography\/post-quantum- cryptography-standardization\/round-3-submissions."},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","unstructured":"Tianrui Wang Anyu Wang and Xiaoyun Wang. 2023. Exploring Decryption Failures of BIKE: New Class of Weak Keys and Key Recovery Attacks. 70--100. doi:10.1007\/978--3-031--38548--3_3","DOI":"10.1007\/978--3-031--38548--3_3"}],"event":{"name":"CCS '25: ACM SIGSAC Conference on Computer and Communications Security","sponsor":["SIGSAC ACM Special Interest Group on Security, Audit, and Control"],"location":"Taipei Taiwan","acronym":"CCS '25"},"container-title":["Proceedings of the 2025 ACM SIGSAC Conference on Computer and Communications Security"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3719027.3765218","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,12,22]],"date-time":"2025-12-22T22:15:56Z","timestamp":1766441756000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3719027.3765218"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,11,19]]},"references-count":36,"alternative-id":["10.1145\/3719027.3765218","10.1145\/3719027"],"URL":"https:\/\/doi.org\/10.1145\/3719027.3765218","relation":{},"subject":[],"published":{"date-parts":[[2025,11,19]]},"assertion":[{"value":"2025-11-22","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}