A Core Calculus for Equational Proofs of Cryptographic Protocols
| Autor: | Joshua Gancher, Kristina Sojakova, Xiong Fan, Elaine Shi, Greg Morrisett |
|---|---|
| Přispěvatelé: | Carnegie Mellon University [Pittsburgh] (CMU), Programming securely with cryptography (PROSECCO), Inria de Paris, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Algorand Foundation, Cornell University [New York], This work was also supported by a Packard Fellowship and an ONR YIP award. This project was partially funded through the NGI Assure Fund, a fund established by NLnet with financial support from the European Commission’s Next Generation Internet programme, under the aegis of DG Communications Networks, Content and Technology under grant agreement No 957073. |
| Rok vydání: | 2023 |
| Předmět: | |
| Zdroj: | POPL 2023-50th ACM SIGPLAN Symposium on Principles of Programming Languages POPL 2023-50th ACM SIGPLAN Symposium on Principles of Programming Languages, Jan 2023, Boston, United States. ⟨10.1145/3571223⟩ |
| ISSN: | 2475-1421 |
| DOI: | 10.1145/3571223 |
| Popis: | International audience; 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|