IMDEA Software

IMDEA initiative

Home > Events > Invited Talks > 2023 > A Core Calculus for Equational Proofs of Cryptographic Protocols

Kristina Sojakova

Thursday, May 4, 2023

10:00am Meeting room 302 & Zoom3 (pass: @s3)

Kristina Sojakova, Research Engineer, INRIA

A Core Calculus for Equational Proofs of Cryptographic Protocols


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.