- October 2020: Charlie Jacomme defended his PhD Thesis “Proofs of Security ProtocolsSymbolic 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