Security protocols are widely used today to secure transactions that take place through public channels

like the Internet. Typical functionalities are the transfer of a credit card number or the authentication of a user on a system. Because of their increasing ubiquity in many important applications (e.g. electronic commerce, smartphone, government-issued ID . . . ), a very important research challenge consists of developing methods and verification tools to increase our trust in security protocols, and so on the applications that rely on them. 

 

Formal symbolic methods offer a way to carefully analyse security protocols through the development of 

proof techniques and specific tools, e.g. ProVerif, and Tamarin. These methods build on techniques from model-checking, automated reasoning, and concurrency theory.  We will explain how security protocols as well as the security properties they are supposed to achieve are formalised in those symbolic models. 

We will review existing results and also point out their main limitations.

Then, we will briefly present the Squirrel prover, a recent interactive tool partly developed by the Spicy team. This tool is based on the so-called computational model and offers stronger security guarantees than the one obtained in the symbolic setting.

Stéphanie Delaune completed her Ph.D. thesis at ENS Cachan in June 2006, and joined the CNRS in 2007. Stéphanie’s research focuses on the formal analysis and design of security protocols. She uses techniques issued from automated reasoning, rewriting, model-checking, and concurrency theory to model and analyse cryptographic protocols. In September 2016, Stéphanie joined the EMSEC team at IRISA 

(Rennes, France) and obtained an ERC Starting Grant: POPSTAR. The purpose of this project was to develop foundations and practical tools to analyse modern security protocols, especially those used in contactless devices. She is now in charge of the Spicy (Security & PrIvaCY) team, and also of the cybersecurity axis at IRISA, and the PI of the SVP project (PEPR Cybersecurity).