{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T02:17:11Z","timestamp":1775873831570,"version":"3.50.1"},"reference-count":98,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2023,7,20]],"date-time":"2023-07-20T00:00:00Z","timestamp":1689811200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"European Research Council under ERC Starting Grant SECOMP","award":["715753"],"award-info":[{"award-number":["715753"]}]},{"name":"AFOSR Grant","award":["12595060"],"award-info":[{"award-number":["12595060"]}]},{"name":"Concordium Blockchain Research Center at Aarhus University, by Nomadic Labs via a grant on the , by the German Federal Ministry of Education and Research BMBF","award":["16KISK038"],"award-info":[{"award-number":["16KISK038"]}]},{"name":"Deutsche Forschungsgemeinschaft (DFG, German Research Foundation) as part of the Excellence Strategy of the German Federal and State Governments","award":["EXC 2092 CASA-390781972"],"award-info":[{"award-number":["EXC 2092 CASA-390781972"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2023,9,30]]},"abstract":"<jats:p>State-separating proofs (SSP) is a recent methodology for structuring game-based cryptographic proofs in a modular way, by using algebraic laws to exploit the modular structure of composed protocols. While promising, this methodology was previously not fully formalized and came with little tool support. We address this by introducing SSProve, the first general verification framework for machine-checked state-separating proofs. SSProve combines high-level modular proofs about composed protocols, as proposed in SSP, with a probabilistic relational program logic for formalizing the lower-level details, which together enable constructing machine-checked cryptographic proofs in the Coq proof assistant. Moreover, SSProve is itself fully formalized in Coq, including the algebraic laws of SSP, the soundness of the program logic, and the connection between these two verification styles.<\/jats:p>\n          <jats:p>To illustrate SSProve, we use it to mechanize the simple security proofs of ElGamal and pseudo-random-function\u2013based encryption. We also validate the SSProve approach by conducting two more substantial case studies: First, we mechanize an SSP security proof of the key encapsulation mechanism\u2013data encryption mechanism (KEM-DEM) public key encryption scheme, which led to the discovery of an error in the original paper proof that has since been fixed. Second, we use SSProve to formally prove security of the sigma-protocol zero-knowledge construction, and we moreover construct a commitment scheme from a sigma-protocol to compare with a similar development in CryptHOL. We instantiate the security proof for sigma-protocols to give concrete security bounds for Schnorr\u2019s sigma-protocol.<\/jats:p>","DOI":"10.1145\/3594735","type":"journal-article","created":{"date-parts":[[2023,5,4]],"date-time":"2023-05-04T12:26:51Z","timestamp":1683203211000},"page":"1-61","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":13,"title":["SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq"],"prefix":"10.1145","volume":"45","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0198-7751","authenticated-orcid":false,"given":"Philipp G.","family":"Haselwarter","sequence":"first","affiliation":[{"name":"Aarhus University, Denmark"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2114-624X","authenticated-orcid":false,"given":"Exequiel","family":"Rivas","sequence":"additional","affiliation":[{"name":"Tallinn University of Technology, Estonia"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4144-9368","authenticated-orcid":false,"given":"Antoine","family":"Van Muylder","sequence":"additional","affiliation":[{"name":"KU Leuven, Belgium"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9881-3696","authenticated-orcid":false,"given":"Th\u00e9o","family":"Winterhalter","sequence":"additional","affiliation":[{"name":"MPI-SP, Germany"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8562-8750","authenticated-orcid":false,"given":"Carmine","family":"Abate","sequence":"additional","affiliation":[{"name":"MPI-SP, Germany"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5092-2172","authenticated-orcid":false,"given":"Nikolaj","family":"Sidorenco","sequence":"additional","affiliation":[{"name":"Aarhus University, Denmark"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8919-8081","authenticated-orcid":false,"given":"C\u0103t\u0103lin","family":"Hri\u0163cu","sequence":"additional","affiliation":[{"name":"MPI-SP, Germany"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5554-3203","authenticated-orcid":false,"given":"Kenji","family":"Maillard","sequence":"additional","affiliation":[{"name":"Inria Rennes, France"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2802-0973","authenticated-orcid":false,"given":"Bas","family":"Spitters","sequence":"additional","affiliation":[{"name":"Aarhus University, Denmark"}]}],"member":"320","published-online":{"date-parts":[[2023,7,20]]},"reference":[{"key":"e_1_3_4_2_2","doi-asserted-by":"publisher","DOI":"10.1109\/CSF51468.2021.00048"},{"key":"e_1_3_4_3_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796819000170"},{"key":"e_1_3_4_4_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-51054-1_1"},{"key":"e_1_3_4_5_2","article-title":"mathcomp-analysis","author":"Affeldt Reynald","year":"2021","unstructured":"Reynald Affeldt, Cyril Cohen, Marie Kerjean, Assia Mahboubi, Damien Rouhling, Kazuhiko Sakaguchi, and Pierre-Yves Strub. 2021. mathcomp-analysis. Analysis library compatible with Mathematical Components. Retrieved from https:\/\/github.com\/math-comp\/analysis.","journal-title":"Analysis library compatible with Mathematical Components"},{"key":"e_1_3_4_6_2","doi-asserted-by":"publisher","DOI":"10.1145\/3133956.3134078"},{"key":"e_1_3_4_7_2","doi-asserted-by":"publisher","DOI":"10.1145\/3319535.3354228"},{"key":"e_1_3_4_8_2","doi-asserted-by":"publisher","DOI":"10.1109\/SP40000.2020.00028"},{"key":"e_1_3_4_9_2","doi-asserted-by":"publisher","DOI":"10.1145\/3460120.3484771"},{"key":"e_1_3_4_10_2","doi-asserted-by":"publisher","DOI":"10.1145\/3319535.3363211"},{"key":"e_1_3_4_11_2","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-11(1:3)2015"},{"key":"e_1_3_4_12_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-19718-5_1"},{"key":"e_1_3_4_13_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-25379-9_12"},{"key":"e_1_3_4_14_2","doi-asserted-by":"crossref","first-page":"49","DOI":"10.1007\/11783596_6","volume-title":"Mathematics of Program Construction","author":"Audebaud Philippe","year":"2006","unstructured":"Philippe Audebaud and Christine Paulin-Mohring. 2006. Proofs of randomized algorithms in Coq. In Mathematics of Program Construction. Springer, 49\u201368."},{"key":"e_1_3_4_15_2","doi-asserted-by":"publisher","DOI":"10.1007\/11541868_4"},{"key":"e_1_3_4_16_2","doi-asserted-by":"publisher","DOI":"10.1109\/SP40001.2021.00008"},{"key":"e_1_3_4_17_2","doi-asserted-by":"publisher","DOI":"10.1145\/3460120.3484548"},{"key":"e_1_3_4_18_2","article-title":"The Messaging Layer Security (MLS) Protocol","author":"Barnes R.","year":"2022","unstructured":"R. Barnes, B. Beurdouche, R. Robert, J. Millican, E. Omara, and K. Cohn-Gordon. 2022. The Messaging Layer Security (MLS) Protocol. IETF Draft. Retrieved from https:\/\/datatracker.ietf.org\/doc\/html\/draft-ietf-mls-protocol-17.","journal-title":"IETF Draft"},{"key":"e_1_3_4_19_2","doi-asserted-by":"publisher","DOI":"10.1109\/SP40001.2021.00046"},{"key":"e_1_3_4_20_2","doi-asserted-by":"publisher","DOI":"10.1145\/2508859.2516663"},{"key":"e_1_3_4_21_2","doi-asserted-by":"publisher","DOI":"10.1145\/1866307.1866350"},{"key":"e_1_3_4_22_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10082-1_6"},{"key":"e_1_3_4_23_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-48899-7_27"},{"key":"e_1_3_4_24_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ICALP.2016.107"},{"key":"e_1_3_4_25_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22792-9_5"},{"key":"e_1_3_4_26_2","doi-asserted-by":"publisher","DOI":"10.1145\/2810103.2813697"},{"key":"e_1_3_4_27_2","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480894"},{"key":"e_1_3_4_28_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00145-019-09341-z"},{"key":"e_1_3_4_29_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2014.02.001"},{"key":"e_1_3_4_30_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00145-013-9167-4"},{"key":"e_1_3_4_31_2","doi-asserted-by":"publisher","DOI":"10.1007\/11761679_25"},{"key":"e_1_3_4_32_2","doi-asserted-by":"publisher","DOI":"10.5555\/2831143.2831157"},{"key":"e_1_3_4_33_2","unstructured":"Daniel J. Bernstein. 2009. Cryptography in NaCl. Retrieved from https:\/\/cr.yp.to\/highspeed\/naclcrypto-20090310.pdf."},{"key":"e_1_3_4_34_2","article-title":"Implementing and proving the TLS 1.3 record layer","author":"Bhargavan Karthikeyan","year":"2017","unstructured":"Karthikeyan Bhargavan, Antoine Delignat-Lavaud, C\u00e9dric Fournet, Markulf Kohlweiss, Jianyang Pan, Jonathan Protzenko, Aseem Rastogi, Nikhil Swamy, Santiago Zanella B\u00e9guelin, and Jean Karim Zinzindohoue. 2017. Implementing and proving the TLS 1.3 record layer. In Proceedings of the IEEE Symposium on Security and Privacy (S&P\u201917).","journal-title":"Proceedings of the IEEE Symposium on Security and Privacy (S&P\u201917)"},{"key":"e_1_3_4_35_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-44381-1_14"},{"key":"e_1_3_4_36_2","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2006.1"},{"key":"e_1_3_4_37_2","doi-asserted-by":"publisher","DOI":"10.1109\/CSF51468.2021.00049"},{"key":"e_1_3_4_38_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99253-8_9"},{"key":"e_1_3_4_39_2","doi-asserted-by":"publisher","DOI":"10.1109\/SP46214.2022.9833678"},{"key":"e_1_3_4_40_2","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. Retrieved from https:\/\/eprint.iacr.org\/2021\/467.","DOI":"10.1007\/978-3-031-22963-3_21"},{"key":"e_1_3_4_41_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-03332-3_9"},{"key":"e_1_3_4_42_2","unstructured":"Chris Brzuska and Sabine Oechsner. 2021. A State-Separating Proof for Yao\u2019s Garbling Scheme. Retrieved from https:\/\/eprint.iacr.org\/2021\/1453."},{"key":"e_1_3_4_43_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-020-09581-w"},{"key":"e_1_3_4_44_2","doi-asserted-by":"publisher","DOI":"10.1145\/3402457"},{"key":"e_1_3_4_45_2","article-title":"UC Domain Specific Language","author":"Canetti Ran","year":"2021","unstructured":"Ran Canetti, Assaf Kfoury, Alley Stoughton, Mayank Varia, Gollamudi Tarakaram, and Tomislav Petrovic. 2021. UC Domain Specific Language. unpublished. Retrieved from https:\/\/github.com\/easyuc\/EasyUC\/tree\/master\/uc-dsl.","journal-title":"unpublished"},{"key":"e_1_3_4_46_2","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2019.00019"},{"key":"e_1_3_4_47_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2016.02.008"},{"key":"e_1_3_4_48_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-25379-9_27"},{"key":"e_1_3_4_49_2","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539702403773"},{"key":"e_1_3_4_50_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-018-9458-4"},{"key":"e_1_3_4_51_2","article-title":"On Sigma-Protocols","author":"Damgaard Ivan","year":"2011","unstructured":"Ivan Damgaard. 2011. On Sigma-Protocols. lecture notes, Aarhus University. Retrieved from https:\/\/cs.au.dk\/ivan\/Sigma.pdf.","journal-title":"lecture notes, Aarhus University"},{"key":"e_1_3_4_52_2","doi-asserted-by":"publisher","DOI":"10.1109\/CSF54842.2022.9919663"},{"key":"e_1_3_4_53_2","doi-asserted-by":"crossref","unstructured":"Fran\u00e7ois Dupressoir Konrad Kohbrok and Sabine Oechsner. 2022. Bringing state-separating proofs to EasyCrypt\u2014A security proof for Cryptobox. Retrieved from https:\/\/eprint.iacr.org\/2021\/326.","DOI":"10.1109\/CSF54842.2022.9919671"},{"key":"e_1_3_4_54_2","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2019.00005"},{"key":"e_1_3_4_55_2","unstructured":"Denis Firsov and Dominique Unruh. 2022. Zero-Knowledge in EasyCrypt. Retrieved from https:\/\/eprint.iacr.org\/2022\/926."},{"key":"e_1_3_4_56_2","doi-asserted-by":"publisher","DOI":"10.1145\/2046707.2046746"},{"key":"e_1_3_4_57_2","doi-asserted-by":"crossref","unstructured":"Joshua Gancher Kristina Sojakova Xiong Fan Elaine Shi and Greg Morrisett. 2023. A Core Calculus for Equational Proofs of Cryptographic Protocols. Retrieved from https:\/\/github.com\/ipdl\/submission\/raw\/main\/main.pdf.","DOI":"10.1145\/3554342"},{"key":"e_1_3_4_58_2","doi-asserted-by":"publisher","DOI":"10.1145\/2034773.2034777"},{"key":"e_1_3_4_59_2","doi-asserted-by":"crossref","first-page":"68","DOI":"10.1007\/BFb0092872","volume-title":"Categorical Aspects of Topology and Analysis","author":"Giry Mich\u00e8le","year":"1982","unstructured":"Mich\u00e8le Giry. 1982. A categorical approach to probability theory. In Categorical Aspects of Topology and Analysis, B. Banaschewski (Ed.). Springer, 68\u201385. Retrieved from https:\/\/www.chrisstucchio.com\/blog_media\/2016\/probability_the_monad\/categorical_probability_giry.pdf."},{"key":"e_1_3_4_60_2","first-page":"181","article-title":"A plausible approach to computer-aided cryptographic proofs","author":"Halevi Shai","year":"2005","unstructured":"Shai Halevi. 2005. A plausible approach to computer-aided cryptographic proofs. IACR Cryptol. ePrint Arch.181. Retrieved from http:\/\/eprint.iacr.org\/2005\/181.","journal-title":"IACR Cryptol. ePrint Arch."},{"key":"e_1_3_4_61_2","article-title":"The Last Yard: Foundational End-to-End Verification of High-Speed Cryptography","author":"Haselwarter Philipp G.","year":"2023","unstructured":"Philipp G. Haselwarter, Benjamin Salling Hvass, Lasse Letager Hansen, Th\u00e9o Winterhalter, Catalin Hritcu, and Bas Spitters. 2023. The Last Yard: Foundational End-to-End Verification of High-Speed Cryptography. Cryptology ePrint Archive, Paper 2023\/185. Retrieved from https:\/\/eprint.iacr.org\/2023\/185. https:\/\/eprint.iacr.org\/2023\/185.","journal-title":"Cryptology ePrint Archive, Paper 2023\/185"},{"key":"e_1_3_4_62_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14303-8"},{"key":"e_1_3_4_63_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37075-5_10"},{"key":"e_1_3_4_64_2","volume-title":"Basic Concepts of Enriched Category Theory","author":"Kelly G M","year":"1982","unstructured":"G M Kelly. 1982. Basic Concepts of Enriched Category Theory. 143 pages. Reprint of the 1982 original, Cambridge University Press, Cambridge, UK."},{"key":"e_1_3_4_65_2","article-title":"Relational F* for State Separating Cryptographic Proofs","author":"Kohbrok Konrad","year":"2020","unstructured":"Konrad Kohbrok, Markulf Kohlweiss, Tahina Ramananandro, and Nikhil Swamy. 2020. Relational F* for State Separating Cryptographic Proofs. F* wiki article. Retrieved from https:\/\/github.com\/FStarLang\/FStar\/wiki\/Relational-F*-for-State-Separating-Cryptographic-Proofs.","journal-title":"F* wiki article"},{"key":"e_1_3_4_66_2","doi-asserted-by":"publisher","DOI":"10.1145\/199448.199528"},{"key":"e_1_3_4_67_2","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314607"},{"key":"e_1_3_4_68_2","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2019.00018"},{"key":"e_1_3_4_69_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-4721-8"},{"key":"e_1_3_4_70_2","article-title":"Mathematical components","author":"Mahboubi Assia","year":"2021","unstructured":"Assia Mahboubi and Enrico Tassi. 2021. Mathematical components. Online book. Retrieved from https:\/\/math-comp.github.io\/mcb\/.","journal-title":"Online book"},{"key":"e_1_3_4_71_2","doi-asserted-by":"publisher","DOI":"10.1145\/3371072"},{"key":"e_1_3_4_72_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-27375-9_3"},{"key":"e_1_3_4_73_2","first-page":"1","volume-title":"Proceedings of the Conference on Innovations in Computer Science (ICS\u201911)","author":"Maurer Ueli","year":"2011","unstructured":"Ueli Maurer and Renato Renner. 2011. Abstract cryptography. In Proceedings of the Conference on Innovations in Computer Science (ICS\u201911). Tsinghua University Press, 1\u201321. Retrieved from http:\/\/conference.iiis.tsinghua.edu.cn\/ICS2011\/content\/papers\/14.html."},{"key":"e_1_3_4_74_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-65127-9_22"},{"key":"e_1_3_4_75_2","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(92)90008-4"},{"key":"e_1_3_4_76_2","volume-title":"The Definition of Standard ML","author":"Milner Robin","year":"1990","unstructured":"Robin Milner, Mads Tofte, and Robert Harper. 1990. The Definition of Standard ML. MIT Press."},{"key":"e_1_3_4_77_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1989.39155"},{"key":"e_1_3_4_78_2","unstructured":"Christine Paulin-Mohring David Baelde and Pierre Courtieu. 2009. ALEA Coq Library. Retrieved from https:\/\/github.com\/coq-community\/alea."},{"key":"e_1_3_4_79_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46666-7_4"},{"key":"e_1_3_4_80_2","doi-asserted-by":"publisher","DOI":"10.1023\/A:1023064908962"},{"key":"e_1_3_4_81_2","doi-asserted-by":"publisher","DOI":"10.1023\/A:1023064908962"},{"key":"e_1_3_4_82_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00590-9_7"},{"key":"e_1_3_4_83_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-72044-9_14"},{"key":"e_1_3_4_84_2","article-title":"The Transport Layer Security (TLS) Protocol Version 1.3","author":"Rescorla Eric","year":"2018","unstructured":"Eric Rescorla. 2018. The Transport Layer Security (TLS) Protocol Version 1.3. IETF RFC 5246. Retrieved from https:\/\/tools.ietf.org\/html\/rfc8446.","journal-title":"IETF RFC 5246"},{"key":"e_1_3_4_85_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96881-0_1"},{"key":"e_1_3_4_86_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796814000264"},{"key":"e_1_3_4_87_2","article-title":"The Joy of Cryptography","author":"Rosulek Mike","year":"2021","unstructured":"Mike Rosulek. 2021. The Joy of Cryptography. Online textbook. Retrieved from http:\/\/web.engr.oregonstate.edu\/rosulekm\/crypto\/.","journal-title":"Online textbook"},{"key":"e_1_3_4_88_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF00196725"},{"key":"e_1_3_4_89_2","doi-asserted-by":"publisher","DOI":"10.1145\/3548606.3560689"},{"key":"e_1_3_4_90_2","first-page":"332","article-title":"Sequences of games: A tool for taming complexity in security proofs","author":"Shoup Victor","year":"2004","unstructured":"Victor Shoup. 2004. Sequences of games: A tool for taming complexity in security proofs. IACR Cryptol. ePrint Arch. (2004), 332. Retrieved from http:\/\/eprint.iacr.org\/2004\/332.","journal-title":"IACR Cryptol. ePrint Arch."},{"key":"e_1_3_4_91_2","doi-asserted-by":"publisher","DOI":"10.1109\/CSF51468.2021.00050"},{"key":"e_1_3_4_92_2","article-title":"A formal security analysis of Blockchain voting","author":"Sidorenco Nikolaj","year":"2022","unstructured":"Nikolaj Sidorenco and Bas Spitters. 2022. A formal security analysis of Blockchain voting. preprint. Retrieved from https:\/\/www.cs.au.dk\/spitters\/ovn.pdf.","journal-title":"preprint"},{"key":"e_1_3_4_93_2","doi-asserted-by":"publisher","DOI":"10.1145\/3474834"},{"key":"e_1_3_4_94_2","first-page":"206","volume-title":"EasyCrypt Reference Manual","author":"Stoughton Alley","year":"2018","unstructured":"Alley Stoughton, Fran\u00e7ois Dupressoir, Pierre-Yves Strub, C\u00e9sar Kunz, Juan Manuel Crespo, Benjamin Gr\u00e9goire, Gilles Barthe, and Benedikt Schmidt. 2018. EasyCrypt Reference Manual. Technical Report. 206 pages."},{"key":"e_1_3_4_95_2","unstructured":"Pierre-Yves Strub. 2020. XHL. Retrieved from https:\/\/github.com\/strub\/xhl."},{"key":"e_1_3_4_96_2","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837655"},{"key":"e_1_3_4_97_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-008-9097-2"},{"key":"e_1_3_4_98_2","doi-asserted-by":"publisher","DOI":"10.1145\/91556.91592"},{"key":"e_1_3_4_99_2","doi-asserted-by":"publisher","DOI":"10.1145\/3133956.3133974"}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3594735","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3594735","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:37:51Z","timestamp":1750178271000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3594735"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,7,20]]},"references-count":98,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2023,9,30]]}},"alternative-id":["10.1145\/3594735"],"URL":"https:\/\/doi.org\/10.1145\/3594735","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"value":"0164-0925","type":"print"},{"value":"1558-4593","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,7,20]]},"assertion":[{"value":"2021-10-29","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2023-03-24","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2023-07-20","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}