A Core Calculus for Equational Proofs of Cryptographic Protocols
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.
Wed 18 JanDisplayed time zone: Eastern Time (US & Canada) change
15:10 - 16:25
|MSWasm: Soundly Enforcing Memory-Safe Execution of Unsafe Code
Alexandra E. Michael University of California at San Diego; University of Washington, Anitha Gollamudi University of Massachusetts Lowell, Jay Bosamiya Carnegie Mellon University, Evan Johnson University of California at San Diego; Arm, Aidan Denlinger University of California at San Diego, Craig Disselkoen University of California at San Diego, Conrad Watt University of Cambridge, Bryan Parno Carnegie Mellon University, Marco Patrignani University of Trento, Marco Vassena Utrecht University, Deian Stefan University of California at San DiegoDOI
|Reconciling Shannon and Scott with a Lattice of Computable Information
Sebastian Hunt City University of London, Dave Sands Chalmers University of Technology, Sandro Stucki Amazon Prime VideoLink to publication DOI Pre-print
|A Core Calculus for Equational Proofs of Cryptographic Protocols
Joshua Gancher Carnegie Mellon University, Kristina Sojakova Inria, Xiong Fan Rutgers University, Elaine Shi Carnegie Mellon University, Greg Morrisett Cornell UniversityDOI