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 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.
