Title: IPDL: A Probabilistic Dataflow Logic for Cryptography

Abstract:

While there have been many successes in verifying cryptographic security proofs of noninteractive 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 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. We deliver mechanized proofs of IPDL and all case studies presented in this work.

About the Speaker:Kristina Sojakova is a Postdoctoral Researcher at the Computer Science Department, Cornell University. Find further details about Kristina here: http://www.cs.cornell.edu/~ks858/

About the Seminar: The COBRA Seminars are weekly seminars hosted by COBRA. The seminars are open to everyone with an interest in blockchain