Tools for automated, symbolic analysis of
real-world cryptographic protocols

Chaire IA
Sep. 2020 - Aug. 2024


The goal of this project is the development of efficient algorithms and tools for automated verification of cryptographic protocols, that are able to comprehensively analyse detailed models of real-world protocols building on techniques from automated reasoning. Automated reasoning is the subfield of AI whose goal is the design of algorithms that enable computers to reason automatically, and these techniques underlie almost all modern verification tools. Current analysis tools for cryptographic protocols do however not scale well, or require to (over)simplify models, when applied on real-world, deployed cryptographic protocols. We aim at overcoming these limitations: we therefore design new, dedicated algorithms, include these algorithms in verification tools, and use the resulting tools for the security analyses of real-world cryptographic protocols. These developments will be driven by and validated on three classes of protocols: e-voting protocols, protocols for mobile devices from the 5G standard, and protocols for modern messaging applications, in particular the NOISE protocol framework.


We are always looking for excellent students. You may contact the project PI and send him your academic CV.


Former members


Publications can be found here.