Calls: Send in your ideas. Deadline April 1, 2024
Grant
Theme fund: NGI Assure
Start: 2023-10

IPDL II

A new process logic aimed at formal proofs for cryptographic algorithm

Our project IPDL aims to increase the trustworthiness of large cryptographic systems by designing and implementing a natural and principled way of thinking about them. IPDL, short for Interactive Probabilistic Dependency Logic, is a process calculus and software implementation for formally verifying message-passing cryptographic protocols. Our goal is to use IPDL to develop cryptographic foundations that are both composable and concurrent. Concurrency means that our model of computation natively allows processes to run at the same time; composability allows us to prove the system secure by verifying the security of its subparts. In this setting, formal proofs closely resemble the thinking of a cryptographer.

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.