- August 2023: Distinguished paper award at Usenix’23 for the paper “Hash Gone Bad: Automated discovery of protocol attacks that exploit hash function weaknesses” by Vincent Cheval, Cas Cremers, Alexander Dax, Lucca Hirschi, Charlie Jacomme, and Steve Kremer
- May 2023: Distinguished paper award at S&P’23 for the paper “Typing High-Speed Cryptography against Spectre v1” by Basavesh Ammanaghatta Shivakumar, Gilles Barthe, Benjamin Grégoire, Vincent Laporte, Tiago Oliviera, Swarn Priya, Peter Schwabe, Lucas Tabary-Maujean.
- May 2023: Michaël Rusinowitch and Mathieu Turuani have been awarded the LICS Test-of-Time award for their paper “An NP Decision Procedure for Protocol Insecurity with XOR” by Yannick Chevalier, Ralf Küsters, Michaël Rusinowitch, Mathieu Turuani.
- April 2022: Véronique Cortier is awarded the CNRS Silver medal 2022!
- April 2021: Charlie Jacomme receives the GDR Sécurité PhD award 2021. Congrats Charlie!
- February 2021: Itsaka Rakotonirina’s PhD defence on 01/02/20201.
- October 2020: Charlie Jacomme defended his PhD Thesis “Proofs of Security Protocols Symbolic Methods and Powerful Attackers”.
- September 2020: Best paper award at ESORICS for the paper “Automatic generation of sources lemmas in Tamarin: towards automatic proofs of security protocols” by Véronique Cortier, Stéphanie Delaune, and Jannik Dreier.
The aim of the Pesto project is to build formal models and techniques, for computer-aided analysis and design of security protocols (in a broad sense). While historically the main goals of protocols were condentiality and authentication the situation has changed. E-voting protocols need to guarantee privacy of votes, while ensuring transparency of the election; electronic devices communicate data by the means of web services; RFID and mobile phone protocols have to guarantee that people cannot be traced. Due to malware, security protocols need to rely on additional mechanisms, such as trusted hardware components or multi-factor authentication, to guarantee security even if the computing platform is a priori untrusted. Current existing techniques and tools are however unable to analyse the properties required by these new protocols and take into account the newly deployed mechanisms and associated attacker models.
- Formal methods for Cryptographic protocols
- Automated reasoning
- Electronic voting
- Privacy in social networks