{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T06:28:05Z","timestamp":1770272885237,"version":"3.49.0"},"reference-count":36,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2023,1,9]],"date-time":"2023-01-09T00:00:00Z","timestamp":1673222400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2023,1,9]]},"abstract":"<jats:p>Many proofs of interactive cryptographic protocols (e.g., as in Universal Composability) operate by proving the protocol at hand to be observationally equivalent to an idealized specification. While pervasive, formal tool support for observational equivalence of cryptographic protocols is still a nascent area of research. Current mechanization efforts tend to either focus on diff-equivalence, which establishes observational equivalence between protocols with identical control structures, or require an explicit witness for the observational equivalence in the form of a bisimulation relation. Our goal is to simplify proofs for cryptographic protocols by introducing a core calculus, IPDL, for cryptographic observational equivalences. Via IPDL, we aim to address a number of theoretical issues for cryptographic proofs in a simple manner, including probabilistic behaviors, distributed message-passing, and resource-bounded adversaries and simulators. We demonstrate IPDL on a number of case studies, including a distributed coin toss protocol, Oblivious Transfer, and the GMW multi-party computation protocol. All proofs of case studies are mechanized via an embedding of IPDL into the Coq proof assistant.<\/jats:p>","DOI":"10.1145\/3571223","type":"journal-article","created":{"date-parts":[[2023,1,11]],"date-time":"2023-01-11T21:58:14Z","timestamp":1673474294000},"page":"866-892","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":8,"title":["A Core Calculus for Equational Proofs of Cryptographic Protocols"],"prefix":"10.1145","volume":"7","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2257-7073","authenticated-orcid":false,"given":"Joshua","family":"Gancher","sequence":"first","affiliation":[{"name":"Carnegie Mellon University, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4880-1416","authenticated-orcid":false,"given":"Kristina","family":"Sojakova","sequence":"additional","affiliation":[{"name":"Inria, France"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0166-0794","authenticated-orcid":false,"given":"Xiong","family":"Fan","sequence":"additional","affiliation":[{"name":"Rutgers University, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5605-1048","authenticated-orcid":false,"given":"Elaine","family":"Shi","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2619-5614","authenticated-orcid":false,"given":"Greg","family":"Morrisett","sequence":"additional","affiliation":[{"name":"Cornell University, USA"}]}],"member":"320","published-online":{"date-parts":[[2023,1,11]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00145-001-0014-7"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/2382196.2382270"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2007.05.002"},{"key":"e_1_2_1_4_1","volume-title":"SP 2021 - 42nd IEEE Symposium on Security and Privacy. San Fransisco \/ Virtual, United States. https:\/\/hal.archives-ouvertes.fr\/hal-03172119","author":"Baelde David","unstructured":"David Baelde , St\u00e9phanie Delaune , Charlie Jacomme , Adrien Koutsos , and Sol\u00e8ne Moreau . 2021. An Interactive Prover for Protocol Verification in the Computational Model . In SP 2021 - 42nd IEEE Symposium on Security and Privacy. San Fransisco \/ Virtual, United States. https:\/\/hal.archives-ouvertes.fr\/hal-03172119 David Baelde, St\u00e9phanie Delaune, Charlie Jacomme, Adrien Koutsos, and Sol\u00e8ne Moreau. 2021. An Interactive Prover for Protocol Verification in the Computational Model. In SP 2021 - 42nd IEEE Symposium on Security and Privacy. San Fransisco \/ Virtual, United States. https:\/\/hal.archives-ouvertes.fr\/hal-03172119"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2660267.2660276"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP40001.2021.00008"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3460120.3484548"},{"key":"e_1_2_1_8_1","doi-asserted-by":"crossref","unstructured":"G. Barthe B. Gr\u00e9goire S. Heraud and Santiago Zanella B\u00e9guelin. 2011. Computer-Aided Security Proofs for the Working Cryptographer. In CRYPTO. G. Barthe B. Gr\u00e9goire S. Heraud and Santiago Zanella B\u00e9guelin. 2011. Computer-Aided Security Proofs for the Working Cryptographer. In CRYPTO.","DOI":"10.1007\/978-3-642-22792-9_5"},{"key":"e_1_2_1_9_1","volume-title":"Proceedings of the 22nd ACM SIGSAC Conference on Computer and Communications Security. 1156\u20131168","author":"Barthe Gilles","year":"2015","unstructured":"Gilles Barthe , Benjamin Gr\u00e9goire , and Benedikt Schmidt . 2015 . Automated proofs of pairing-based cryptography . In Proceedings of the 22nd ACM SIGSAC Conference on Computer and Communications Security. 1156\u20131168 . Gilles Barthe, Benjamin Gr\u00e9goire, and Benedikt Schmidt. 2015. Automated proofs of pairing-based cryptography. In Proceedings of the 22nd ACM SIGSAC Conference on Computer and Communications Security. 1156\u20131168."},{"key":"e_1_2_1_10_1","volume-title":"Annual International Cryptology Conference. 97\u2013109","author":"Beaver Donald","year":"1995","unstructured":"Donald Beaver . 1995 . Precomputing oblivious transfer . In Annual International Cryptology Conference. 97\u2013109 . Donald Beaver. 1995. Precomputing oblivious transfer. In Annual International Cryptology Conference. 97\u2013109."},{"key":"e_1_2_1_11_1","volume-title":"Pedram Hosseyni, Ralf K\u00fcsters, Guido Schmitz, and Tim W\u00fcrtele.","author":"Bhargavan Karthikeyan","year":"2021","unstructured":"Karthikeyan Bhargavan , Abhishek Bichhawat , Quoc Huy Do , Pedram Hosseyni, Ralf K\u00fcsters, Guido Schmitz, and Tim W\u00fcrtele. 2021 . DY* : A Modular Symbolic Verification Framework for Executable Cryptographic Protocol Code. In EuroS&P 2021 - 6th IEEE European Symposium on Security and Privacy. Virtual, Austria . https:\/\/hal.inria.fr\/hal-03178425 Karthikeyan Bhargavan, Abhishek Bichhawat, Quoc Huy Do, Pedram Hosseyni, Ralf K\u00fcsters, Guido Schmitz, and Tim W\u00fcrtele. 2021. DY* : A Modular Symbolic Verification Framework for Executable Cryptographic Protocol Code. In EuroS&P 2021 - 6th IEEE European Symposium on Security and Privacy. Virtual, Austria. https:\/\/hal.inria.fr\/hal-03178425"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2006.1"},{"key":"e_1_2_1_13_1","volume-title":"Foundations of security analysis and design","author":"Blanchet Bruno","unstructured":"Bruno Blanchet . 2013. Automatic verification of security protocols in the symbolic model: The verifier proverif . In Foundations of security analysis and design VII. Springer , 54\u201387. Bruno Blanchet. 2013. Automatic verification of security protocols in the symbolic model: The verifier proverif. In Foundations of security analysis and design VII. Springer, 54\u201387."},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1008908.1008911"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3372885.3373815"},{"key":"e_1_2_1_17_1","volume-title":"32nd IEEE Computer Security Foundations Symposium. https:\/\/eprint.iacr.org\/2019\/582","author":"Canetti Ran","year":"2019","unstructured":"Ran Canetti , Alley Stoughton , and Mayank Varia . 2019 . EasyUC: Using EasyCrypt to Mechanize Proofs of Universally Composable Security . In 32nd IEEE Computer Security Foundations Symposium. https:\/\/eprint.iacr.org\/2019\/582 Ran Canetti, Alley Stoughton, and Mayank Varia. 2019. EasyUC: Using EasyCrypt to Mechanize Proofs of Universally Composable Security. In 32nd IEEE Computer Security Foundations Symposium. https:\/\/eprint.iacr.org\/2019\/582"},{"key":"e_1_2_1_18_1","first-page":"173","article-title":"Practical byzantine fault tolerance","volume":"99","author":"Castro Miguel","year":"1999","unstructured":"Miguel Castro and Barbara Liskov . 1999 . Practical byzantine fault tolerance . In OsDI. 99 , 173 \u2013 186 . Miguel Castro and Barbara Liskov. 1999. Practical byzantine fault tolerance. In OsDI. 99, 173\u2013186.","journal-title":"OsDI."},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2046707.2046717"},{"key":"e_1_2_1_20_1","volume-title":"The Scyther Tool: Verification, Falsification, and Analysis of Security Protocols","author":"Cremers Cas J. F.","unstructured":"Cas J. F. Cremers . 2008. The Scyther Tool: Verification, Falsification, and Analysis of Security Protocols . In Computer Aided Verification, Aarti Gupta and Sharad Malik (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg . 414\u2013418. Cas J. F. Cremers. 2008. The Scyther Tool: Verification, Falsification, and Analysis of Security Protocols. In Computer Aided Verification, Aarti Gupta and Sharad Malik (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 414\u2013418."},{"key":"e_1_2_1_21_1","volume-title":"Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security.","author":"Karim","unstructured":"Karim M. El Defrawy and Vitor Pereira. 2019. A High-Assurance Evaluator for Machine-Checked Secure Multiparty Computation . Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security. Karim M. El Defrawy and Vitor Pereira. 2019. A High-Assurance Evaluator for Machine-Checked Secure Multiparty Computation. Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security."},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/TIT.1983.1056650"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3497775.3503693"},{"key":"e_1_2_1_24_1","doi-asserted-by":"crossref","unstructured":"Joshua Gancher Kristina Sojakova Xiong Fan Elaine Shi and Greg Morrisett. 2022. A Core Calculus for Equational Proofs of Distributed Cryptographic Protocols: Supplemental Material. https:\/\/github.com\/ipdl\/ipdl Joshua Gancher Kristina Sojakova Xiong Fan Elaine Shi and Greg Morrisett. 2022. A Core Calculus for Equational Proofs of Distributed Cryptographic Protocols: Supplemental Material. https:\/\/github.com\/ipdl\/ipdl","DOI":"10.1145\/3554342"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/28395.28420"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498684"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314607"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3387108"},{"key":"e_1_2_1_30_1","volume-title":"32nd IEEE Computer Security Foundations Symposium. http:\/\/www.andreas-lochbihler.de\/pub\/lochbihler2019csf.pdf","author":"Lochbihler Andreas","year":"2019","unstructured":"Andreas Lochbihler , S. Reza Sefidgar , David Basin , and Ueli Maurer . 2019 . Formalizing Constructive Cryptography using CryptHOL . In 32nd IEEE Computer Security Foundations Symposium. http:\/\/www.andreas-lochbihler.de\/pub\/lochbihler2019csf.pdf Andreas Lochbihler, S. Reza Sefidgar, David Basin, and Ueli Maurer. 2019. Formalizing Constructive Cryptography using CryptHOL. In 32nd IEEE Computer Security Foundations Symposium. http:\/\/www.andreas-lochbihler.de\/pub\/lochbihler2019csf.pdf"},{"key":"e_1_2_1_31_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Lowe Gavin","unstructured":"Gavin Lowe . 1996. Breaking and fixing the Needham-Schroeder Public-Key Protocol using FDR . In Tools and Algorithms for the Construction and Analysis of Systems , Tiziana Margaria and Bernhard Steffen (Eds.). Springer Berlin Heidelberg, Berlin , Heidelberg . 147\u2013166. isbn:978-3-540-49874-2 Gavin Lowe. 1996. Breaking and fixing the Needham-Schroeder Public-Key Protocol using FDR. In Tools and Algorithms for the Construction and Analysis of Systems, Tiziana Margaria and Bernhard Steffen (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 147\u2013166. isbn:978-3-540-49874-2"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.4457887"},{"key":"e_1_2_1_33_1","volume-title":"Theory of Security and Applications, Sebastian M\u00f6dersheim and Catuscia Palamidessi (Eds.)","author":"Maurer Ueli","unstructured":"Ueli Maurer . 2012. Constructive Cryptography \u2013 A New Paradigm for Security Definitions and Proofs . In Theory of Security and Applications, Sebastian M\u00f6dersheim and Catuscia Palamidessi (Eds.) . Springer Berlin Heidelberg, Berlin , Heidelberg . 33\u201356. isbn:978-3-642-27375-9 Ueli Maurer. 2012. Constructive Cryptography \u2013 A New Paradigm for Security Definitions and Proofs. In Theory of Security and Applications, Sebastian M\u00f6dersheim and Catuscia Palamidessi (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 33\u201356. isbn:978-3-642-27375-9"},{"key":"e_1_2_1_34_1","volume-title":"The TAMARIN Prover for the Symbolic Analysis of Security Protocols","author":"Meier Simon","unstructured":"Simon Meier , Benedikt Schmidt , Cas Cremers , and David Basin . 2013. The TAMARIN Prover for the Symbolic Analysis of Security Protocols . In Computer Aided Verification, Natasha Sharygina and Helmut Veith (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg . 696\u2013701. isbn:978-3-642-39799-8 Simon Meier, Benedikt Schmidt, Cas Cremers, and David Basin. 2013. The TAMARIN Prover for the Symbolic Analysis of Security Protocols. In Computer Aided Verification, Natasha Sharygina and Helmut Veith (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 696\u2013701. isbn:978-3-642-39799-8"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(92)90008-4"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/301250.301312"},{"key":"e_1_2_1_37_1","volume-title":"Principles of Security and Trust","author":"Petcher Adam","unstructured":"Adam Petcher and Greg Morrisett . 2015. The Foundational Cryptography Framework . In Principles of Security and Trust , Riccardo Focardi and Andrew Myers (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg . 53\u201372. isbn:978-3-662-46666-7 Adam Petcher and Greg Morrisett. 2015. The Foundational Cryptography Framework. In Principles of Security and Trust, Riccardo Focardi and Andrew Myers (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 53\u201372. isbn:978-3-662-46666-7"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1109\/SECPRI.1996.502680"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3571223","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3571223","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T18:08:21Z","timestamp":1750183701000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3571223"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,1,9]]},"references-count":36,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2023,1,9]]}},"alternative-id":["10.1145\/3571223"],"URL":"https:\/\/doi.org\/10.1145\/3571223","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,1,9]]},"assertion":[{"value":"2023-01-11","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}