Calls: Send in your ideas. Deadline August 1st, 2023.
Source code :
More info available :
More projects like this
Software engineering


Equational Proofs for Distributed Cryptographic Protocols

In cryptography, interactive, distributed cryptographic protocols are most often proved secure using the simulation paradigm, wherein the protocol of interest is proved (approximately) equivalent to an idealization. The simulation paradigm is extremely powerful, as it allows a wide range of security properties to be captured under one definition. On the other hand, while expressive, the simulation paradigm presents extra complications for formally verifying security proofs. Proving equivalences between distributed protocols in general requires heavyweight techniques based on manually constructing so-called bisimulations (suitable relational invariants), which creates a barrier to entry for formal methods. We lower this barrier to entry with IPDL, or Interactive Probabilistic Dependency Logic, a new process calculus for cryptographic protocols. IPDL includes an approximate equational logic that allows computationally sound reasoning about protocols in a manner both close to the simulation paradigm and amenable for formal verification. Using IPDL, we deliver short, simulation-based proofs of variety of cryptographic protocols. Our most complex and very general case study verifies the n-party GMW protocol for secure function evaluation.

Logo NLnet: abstract logo of four people seen from above Logo NGI Assure: letterlogo shaped like a tag

This project was funded through the NGI Assure Fund, a fund established by NLnet with financial support from the European Commission's Next Generation Internet programme, under the aegis of DG Communications Networks, Content and Technology under grant agreement No 957073.

Navigate projects

Please check out NLnet's theme funds, such as NGI Assure and NGI Zero Entrust.

Want to help but no money to spend? Help us by protecting open source and its users.