Goals

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.

Positions

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

Members

• Vincent Cheval (permanent researcher)
• Alexandre Debant (post-doc)
• Lucca Hirschi (permanent researcher)
• Elise Klein (PhD student)
• Steve Kremer (permanent researcher, PI of the project)
• Maïwenn Racouchot (PhD student)

Former members

• Raphaëlle Crubillé (post-doc 09/2019-12/2020, now CNRS researcher at LIS, Marseille)

Publications