{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,12]],"date-time":"2026-06-12T04:36:12Z","timestamp":1781238972948,"version":"3.54.1"},"publisher-location":"New York, NY, USA","reference-count":64,"publisher":"ACM","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2025,11,19]]},"DOI":"10.1145\/3719027.3765213","type":"proceedings-article","created":{"date-parts":[[2025,11,22]],"date-time":"2025-11-22T23:32:38Z","timestamp":1763854358000},"page":"2729-2743","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["Formal Security and Functional Verification of Cryptographic Protocol Implementations in Rust"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3152-8997","authenticated-orcid":false,"given":"Karthikeyan","family":"Bhargavan","sequence":"first","affiliation":[{"name":"Cryspen, Paris, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3271-3593","authenticated-orcid":false,"given":"Lasse Letager","family":"Hansen","sequence":"additional","affiliation":[{"name":"Aarhus University, Aarhus, Denmark"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0003-3632-4613","authenticated-orcid":false,"given":"Franziskus","family":"Kiefer","sequence":"additional","affiliation":[{"name":"Cryspen, Paris, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0007-1000-7918","authenticated-orcid":false,"given":"Jonas","family":"Schneider-Bensch","sequence":"additional","affiliation":[{"name":"Cryspen, Paris, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2802-0973","authenticated-orcid":false,"given":"Bas","family":"Spitters","sequence":"additional","affiliation":[{"name":"Aarhus University, Aarhus, Denmark"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,11,22]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Th\u00e9o Winterhalter, Catalin Hritcu, Kenji Maillard, and Bas Spitters.","author":"Abate Carmine","year":"2021","unstructured":"Carmine Abate, Philipp G. Haselwarter, Exequiel Rivas, Antoine Van Muylder, Th\u00e9o Winterhalter, Catalin Hritcu, Kenji Maillard, and Bas Spitters. 2021. SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq. In CSF. IEEE, 1-15."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/2810103.2813707"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2013.42"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-68379-4_12"},{"key":"e_1_3_2_1_5_1","first-page":"1807","article-title":"Jasmin: High-Assurance and High-Speed Cryptography","author":"Almeida Jos\u00e9 Bacelar","year":"2017","unstructured":"Jos\u00e9 Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Arthur Blot, Benjamin Gr\u00e9goire, Vincent Laporte, Tiago Oliveira, Hugo Pacheco, Benedikt Schmidt, and Pierre-Yves Strub. 2017. Jasmin: High-Assurance and High-Speed Cryptography. In CCS. ACM, 1807-1823.","journal-title":"CCS. ACM"},{"key":"e_1_3_2_1_6_1","volume-title":"Proc. ACM Program. Lang.","volume":"3","author":"Astrauskas V.","unstructured":"V. Astrauskas, P. M\u00fcller, F. Poli, and A. J. Summers. 2019. Leveraging Rust Types for Modular Specification and Verification, In Object-Oriented Programming Systems, Languages, and Applications (OOPSLA). Proc. ACM Program. Lang., Vol. 3, 147:1-147:30."},{"key":"e_1_3_2_1_7_1","first-page":"689","volume-title":"25th USENIX Security Symposium, USENIX Security 16","author":"Aviram Nimrod","year":"2016","unstructured":"Nimrod Aviram, Sebastian Schinzel, Juraj Somorovsky, Nadia Heninger, Maik Dankel, Jens Steube, Luke Valenta, David Adrian, J. Alex Halderman, Viktor Dukhovni, Emilia K\u00e4sper, Shaanan Cohney, Susanne Engels, Christof Paar, and Yuval Shavitt. 2016. DROWN: Breaking TLS Using SSLv2. In 25th USENIX Security Symposium, USENIX Security 16, Austin, TX, USA, August 10-12, 2016, Thorsten Holz and Stefan Savage (Eds.). USENIX Association, 689-706. https:\/\/www.usenix.org\/conference\/usenixsecurity16\/technical-sessions\/presentation\/aviram"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP46215.2023.10179290"},{"key":"e_1_3_2_1_9_1","first-page":"777","article-title":"SoK: Computer-Aided Cryptography","author":"Barbosa Manuel","year":"2021","unstructured":"Manuel Barbosa, Gilles Barthe, Karthik Bhargavan, Bruno Blanchet, Cas Cremers, Kevin Liao, and Bryan Parno. 2021. SoK: Computer-Aided Cryptography. In SP. IEEE, 777-795.","journal-title":"SP. IEEE"},{"key":"e_1_3_2_1_10_1","first-page":"146","article-title":"EasyCrypt: A Tutorial. In FOSAD (Lecture Notes in Computer Science, Vol. 8604)","author":"Barthe Gilles","year":"2013","unstructured":"Gilles Barthe, Fran\u00e7ois Dupressoir, Benjamin Gr\u00e9goire, C\u00e9sar Kunz, Benedikt Schmidt, and Pierre-Yves Strub. 2013. EasyCrypt: A Tutorial. In FOSAD (Lecture Notes in Computer Science, Vol. 8604). Springer, 146-166.","journal-title":"Springer"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1890028.1890031"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3023357"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.SNAPL.2017.1"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-86695-1_7"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2014.14"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1452044.1452049"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2013.37"},{"key":"e_1_3_2_1_18_1","volume-title":"33rd USENIX Security Symposium, USENIX Security 2024","author":"Bhargavan Karthikeyan","year":"2024","unstructured":"Karthikeyan Bhargavan, Charlie Jacomme, Franziskus Kiefer, and Rolfe Schmidt. 2024. Formal verification of the PQXDH Post-Quantum key agreement protocol for end-to-end secure messaging. In 33rd USENIX Security Symposium, USENIX Security 2024, Philadelphia, PA, USA, August 14-16, 2024, Davide Balzarotti and Wenyuan Xu (Eds.). USENIX Association. https:\/\/www.usenix.org\/conference\/usenixsecurity24\/presentation\/bhargavan"},{"key":"e_1_3_2_1_19_1","volume-title":"IKE and SSH. In 23rd Annual Network and Distributed System Security Symposium, NDSS 2016","author":"Bhargavan Karthikeyan","year":"2016","unstructured":"Karthikeyan Bhargavan and Ga\u00ebtan Leurent. 2016. Transcript Collision Attacks: Breaking Authentication in TLS, IKE and SSH. In 23rd Annual Network and Distributed System Security Symposium, NDSS 2016, San Diego, California, USA, February 21-24, 2016. The Internet Society. http:\/\/wp.internetsociety.org\/ndss\/wp-content\/uploads\/sites\/25\/2017\/09\/transcript-collision-attacks-breaking-authentication-tls-ike-ssh.pdf"},{"key":"e_1_3_2_1_20_1","volume-title":"Dagstuhl seminar ''Formal Protocol Verification Applied","author":"Blanchet Bruno","unstructured":"Bruno Blanchet. 2007. CryptoVerif: Computationally sound mechanized prover for cryptographic protocols. In Dagstuhl seminar ''Formal Protocol Verification Applied, Vol. 117. 156."},{"key":"e_1_3_2_1_21_1","first-page":"54","article-title":"Automatic Verification of Security Protocols in the Symbolic Model: The Verifier ProVerif. In FOSAD (Lecture Notes in Computer Science, Vol. 8604)","author":"Blanchet Bruno","year":"2013","unstructured":"Bruno Blanchet. 2013. Automatic Verification of Security Protocols in the Symbolic Model: The Verifier ProVerif. In FOSAD (Lecture Notes in Computer Science, Vol. 8604). Springer, 54-87.","journal-title":"Springer"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"crossref","unstructured":"Chris Brzuska Antoine Delignat-Lavaud Christoph Egger C\u00e9dric Fournet Konrad Kohbrok and Markulf Kohlweiss. 2021. Key-schedule Security for the TLS 1.3 Standard. Cryptology ePrint Archive Paper 2021\/467. https:\/\/eprint.iacr.org\/2021\/467","DOI":"10.1007\/978-3-031-22963-3_21"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-03332-3_9"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133956.3134063"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP54263.2024.00220"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2017.58"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-17244-1_6"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/TIT.1983.1056650"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/S00145-021-09384-1"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3421473.3421477"},{"key":"e_1_3_2_1_31_1","unstructured":"Nima Rahimi Foroushaani and Bart Jacobs. 2022. Modular Formal Verification of Rust Programs with Unsafe Blocks. arXiv:2212.12976 [cs.LO] https:\/\/arxiv.org\/abs\/2212.12976"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2046707.2046746"},{"key":"e_1_3_2_1_33_1","unstructured":"Aymeric Fromherz and Jonathan Protzenko. 2024. Compiling C to safe Rust formalized. arXiv:2412.15042 [cs.PL] https:\/\/arxiv.org\/abs\/2412.15042"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3656422"},{"key":"e_1_3_2_1_35_1","first-page":"83","volume-title":"Constant-Time Callees with Variable-Time Callers. In 26th USENIX Security Symposium (USENIX Security 17)","author":"Garc\u00eda Cesar Pereida","year":"2017","unstructured":"Cesar Pereida Garc\u00eda and Billy Bob Brumley. 2017. Constant-Time Callees with Variable-Time Callers. In 26th USENIX Security Symposium (USENIX Security 17). USENIX Association, Vancouver, BC, 83-98. https:\/\/www.usenix.org\/conference\/usenixsecurity17\/technical-sessions\/presentation\/garcia"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/2382196.2382204"},{"key":"e_1_3_2_1_37_1","first-page":"30","article-title":"The Last Yard: Foundational End-to-End Verification of High-Speed Cryptography","author":"Haselwarter Philipp G.","year":"2024","unstructured":"Philipp G. Haselwarter, Benjamin Salling Hvass, Lasse Letager Hansen, Th\u00e9o Winterhalter, Catalin Hritcu, and Bas Spitters. 2024. The Last Yard: Foundational End-to-End Verification of High-Speed Cryptography. In CPP. ACM, 30-44.","journal-title":"CPP. ACM"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/3594735"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3547647"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP46214.2022.9833621"},{"key":"e_1_3_2_1_41_1","volume-title":"Bas Spitters, Manuel Barbosa, Antoine S\u00e9r\u00e9, and Pierre-Yves Strub.","author":"Kiefer Franziskus","year":"2023","unstructured":"Franziskus Kiefer, Karthikeyan Bhargavan, Lucas Franceschino, Denis Merigoux, Lasse Letager Hansen, Bas Spitters, Manuel Barbosa, Antoine S\u00e9r\u00e9, and Pierre-Yves Strub. 2023. HACSPEC: a gateway to high-assurance cryptography. RealWorldCrypto (2023)."},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1109\/EUROSP.2017.38"},{"key":"e_1_3_2_1_43_1","unstructured":"Kris Kwiatkowski Panos Kampanakis Bas Westerbaan and Douglas Stebila. 2024. Post-quantum hybrid ECDHE-MLKEM Key Agreement for TLSv1.3. Internet-Draft draft-kwiatkowski-tls-ecdhe-mlkem-03. Internet Engineering Task Force. https:\/\/datatracker.ietf.org\/doc\/draft-kwiatkowski-tls-ecdhe-mlkem\/03\/ Work in Progress."},{"key":"e_1_3_2_1_44_1","unstructured":"Markus Krabbe Larsen and Carsten Sch\u00fcrmann. 2025. Nominal State-Separating Proofs. Cryptology ePrint Archive Paper 2025\/598. https:\/\/eprint.iacr.org\/2025\/598"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/3586037"},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/3591283"},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/3658644.3670359"},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/2382196.2382206"},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/359657.359659"},{"key":"e_1_3_2_1_50_1","volume-title":"32nd USENIX Security Symposium, USENIX Security 2023","author":"Paterson Kenneth G.","year":"2023","unstructured":"Kenneth G. Paterson, Matteo Scarlata, and Kien Tuong Truong. 2023. Three Lessons From Threema: Analysis of a Secure Messenger. In 32nd USENIX Security Symposium, USENIX Security 2023, Anaheim, CA, USA, August 9-11, 2023, Joseph A. Calandrino and Carmela Troncoso (Eds.). USENIX Association, 1289-1306. https:\/\/www.usenix.org\/conference\/usenixsecurity23\/presentation\/paterson"},{"key":"e_1_3_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2019.00064"},{"key":"e_1_3_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP40000.2020.00114"},{"key":"e_1_3_2_1_53_1","first-page":"1465","volume-title":"EverParse: Verified Secure Zero-Copy Parsers for Authenticated Message Formats. In 28th USENIX Security Symposium, USENIX Security 2019","author":"Ramananandro Tahina","year":"2019","unstructured":"Tahina Ramananandro, Antoine Delignat-Lavaud, C\u00e9dric Fournet, Nikhil Swamy, Tej Chajed, Nadim Kobeissi, and Jonathan Protzenko. 2019. EverParse: Verified Secure Zero-Copy Parsers for Authenticated Message Formats. In 28th USENIX Security Symposium, USENIX Security 2019, Santa Clara, CA, USA, August 14-16, 2019. USENIX Association, 1465-1482."},{"key":"e_1_3_2_1_54_1","doi-asserted-by":"publisher","unstructured":"Eric Rescorla. 2018. The Transport Layer Security (TLS) Protocol Version 1.3. RFC 8446. doi:10.17487\/RFC8446","DOI":"10.17487\/RFC8446"},{"key":"e_1_3_2_1_55_1","unstructured":"Mike Rosulek. 2025. The Joy of Cryptography. https:\/\/joyofcryptography.com https:\/\/joyofcryptography.com."},{"key":"e_1_3_2_1_56_1","unstructured":"Douglas Stebila Scott Fluhrer and Shay Gueron. 2025. Hybrid key exchange in TLS 1.3. Internet-Draft draft-ietf-tls-hybrid-design-12. Internet Engineering Task Force. https:\/\/datatracker.ietf.org\/doc\/draft-ietf-tls-hybrid-design\/12\/ Work in Progress."},{"key":"e_1_3_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837655"},{"key":"e_1_3_2_1_58_1","doi-asserted-by":"publisher","unstructured":"The Coq Development Team. 2024. The Coq Proof Assistant. (2024). doi:10.5281\/zenodo.11551307","DOI":"10.5281\/zenodo.11551307"},{"key":"e_1_3_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/3510457.3513031"},{"key":"e_1_3_2_1_60_1","volume-title":"TreeSync: Authenticated Group Management for Messaging Layer Security. In 32nd USENIX Security Symposium, USENIX Security 2023","author":"Wallez Th\u00e9ophile","year":"2023","unstructured":"Th\u00e9ophile Wallez, Jonathan Protzenko, Benjamin Beurdouche, and Karthikeyan Bhargavan. 2023b. TreeSync: Authenticated Group Management for Messaging Layer Security. In 32nd USENIX Security Symposium, USENIX Security 2023, Anaheim, CA, USA, August 9-11, 2023, Joseph A. Calandrino and Carmela Troncoso (Eds.). USENIX Association, 1217-1233. https:\/\/www.usenix.org\/conference\/usenixsecurity23\/presentation\/wallez"},{"key":"e_1_3_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1145\/3576915.3623201"},{"key":"e_1_3_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133956.3134043"},{"key":"e_1_3_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133956.3134043"},{"key":"e_1_3_2_1_64_1","unstructured":"Sacha \u00c9lie Ayoun Xavier Denis Petar Maksimovic and Philippa Gardner. 2025. A Hybrid Approach to Semi-automated Rust Verification. arXiv:2403.15122 [cs.PL] https:\/\/arxiv.org\/abs\/2403.15122 gr"}],"event":{"name":"CCS '25: ACM SIGSAC Conference on Computer and Communications Security","location":"Taipei Taiwan","acronym":"CCS '25","sponsor":["SIGSAC ACM Special Interest Group on Security, Audit, and Control"]},"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.3765213","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,12,22]],"date-time":"2025-12-22T22:15:10Z","timestamp":1766441710000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3719027.3765213"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,11,19]]},"references-count":64,"alternative-id":["10.1145\/3719027.3765213","10.1145\/3719027"],"URL":"https:\/\/doi.org\/10.1145\/3719027.3765213","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"}}]}}