Paper 2021/147

IPDL: A Simple Framework for Formally Verifying Distributed Cryptographic Protocols

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

Abstract

Although there have been many successes in verifying proofs of non-interactive cryptographic primitives such as encryption and signatures, formal verification of interactive cryptographic protocols is still a nascent area. While in principle, it seems possible to extend general frameworks such as Easycrypt to encode proofs for more complex, interactive protocols, a big challenge is whether the human effort would be scalable enough for proof mechanization to eventually acquire mainstream usage among the cryptography community. We work towards closing this gap by introducing a simple framework, Interactive Probabilistic Dependency Logic (IPDL), for reasoning about a certain well-behaved subset of cryptographic protocols. A primary design goal of IPDL is for formal cryptographic proofs to resemble their on-paper counterparts. To this end, IPDL includes an equational logic to reason about approximate observational equivalence (i.e., computational indistinguishability) properties between protocols. IPDL adopts a channel-centric core logic, which decomposes the behavior of the protocol into the behaviors along each communication channel. IPDL supports straight-line programs with statically bounded loops. This design allows us to capture a broad class of protocols encountered in the cryptography literature, including multi-party, reactive, and/or inductively-defined protocols; meanwhile, the logic can track the runtime of the computational reduction in security proofs, thus ensuring computational soundness. We demonstrate the use of IPDL by a number of case studies, including a multi-use, secure message communication protocol, a multi-party coin toss with abort protocol, several oblivious transfer constructions, as well as the two-party GMW protocol for securely evaluating general circuits. We provide a mechanization of the IPDL proof system and our case studies in Coq, and our code is open sourced at https://github.com/ipdl/ipdl.