Many proofs of interactive cryptographic protocols (e.g., as in Universal Composability) operate by proving the protocol to be observationally equivalent to an idealized specification. Formal tool support for proving observational equivalence of cryptographic protocols is a nascent area of research. Current tools either support only certain forms of observational equivalence or require an amount of proof effort that makes large-scale verification infeasible.

To bridge this gap, we introduce equational techniques for cryptography in the computational model. Our core calculus, the Interactive Probabilistic Dependency Logic (IPDL), is simple, expressive, and addresses technical issues such as probabilistic behaviors, distributed message-passing, and resource-bounded adversaries and simulators. We demonstrate our techniques on a number of case studies, including a distributed coin toss protocol, Oblivious Transfer, and the GMW multi-party computation protocol. All proofs of our case studies are mechanized.