Theme fund: NGI Zero Core
Start: 2023-10
- Seeall themes
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.
- The project's own website:https://github.com/kristinas/IPDL-Maude
This project was funded through theNGI0 Core Fund, a fund established byNLnet with financial support from the European Commission'sNext Generation Internet programme, under the aegis ofDG Communications Networks, Content and Technology under grant agreement No101092990.
