A Core Calculus for Equational Proofs of Cryptographic Protocols
summary
Introduces a tiny process calculus and an equation-of-logic that proves observational equivalence for distributed crypto by rewriting networks of probabilistic programs rather than by bespoke bisimulations. Claims: IPDL supports exact and approximate (crypto) rewrites, is congruent for modular proofs, and is sound against arbitrary polynomial-time adversaries. Implements the calculus embedded in Coq and mechanizes case studies (coin toss, OT, GMW MPC), with proofs under 2,300 LOC (largest ≈2,200; one OTP proof ≈700 LOC versus prior 18,000/2,000).
AI-written summary · about
chapters (12)
- 0:00Start
- 0:28Observational Equivalence: Universal Composability
- 2:38Real Hybrid
- 2:51Barriers to Equational Reasoning
- 5:16Computational Model
- 6:19Protocols in IPDL
- 9:24Equational Logic
- 10:26Exact Equivalences
- 12:23Approximate Reasoning
- 15:23Coq Embedding
- 16:31Case Studies
- 23:01Soundness
related talks
01h 09mProofs - Practice 1
22mComputational-Bounded Robust Compilation and Universally Composable Security
01h 08mTutorial on Proof Systems
01h 07mIndistinguishability Obfuscation via Mathematical Proofs
01h 09mCrypto + ML 1
52mIndistinguishability Obfuscation via Mathematical Proofs of Equivalence
01h 01mLocal Proofs Approaching the Witness Length
01h 03mLinear-Time Zero-Knowledge Arguments with Logarithmic Proof-Size