Paper 2019/1422

IPDL: A Probabilistic Dataflow Logic for Cryptography

Xiong Fan, Joshua Gancher, Greg Morrisett, Elaine Shi, and Kristina Sojakova

Abstract

While there have been many successes in verifying cryptographic security proofs of noninter- active primitives such as encryption and signatures, less attention has been paid to interactive cryptographic protocols. Interactive protocols introduce the additional verification challenge of concurrency, which is notoriously hard to reason about in a cryptographically sound manner. When proving the (approximate) observational equivalance of protocols, as is required by simulation based security in the style of Universal Composability (UC), a bisimulation is typically performed in order to reason about the nontrivial control flows induced by concurrency. Unfortunately, bisimulations are typically very tedious to carry out manually and do not capture the high-level intuitions which guide informal proofs of UC security on paper. Because of this, there is currently a large gap of formality between proofs of cryptographic protocols on paper and in mechanized theorem provers. We work towards closing this gap through a new methodology for iteratively constructing bisimulations in a manner close to on-paper intuition. We present this methodology through Interactive Probabilistic Dependency Logic (IPDL), a simple calculus and proof system for specifying and reasoning about (a certain subclass of) distributed probabilistic computations. The IPDL framework exposes an equational logic on protocols; proofs in our logic consist of a number of rewriting rules, each of which induce a single low-level bisimulation between protocols. We show how to encode simulation-based security in the style of UC in our logic, and evaluate our logic on a number of case studies; most notably, a semi-honest secure Oblivious Transfer protocol, and a simple multiparty computation protocol robust to Byzantine faults. Due to the novel design of our logic, we are able to deliver mechanized proofs of protocols which we believe are comprehensible to cryptographers without verification expertise. We provide a mechanization in Coq of IPDL and all case studies presented in this work.

Note: This work is superseded by report: https://eprint.iacr.org/2021/147