Supervisor

Suitable for

Abstract

Security protocols aim at securing communications. They are used in various applications (e.g. establishment of secure channels over the Internet, secure messaging, electronic voting, mobile communications, etc.) Their design is known to be error prone and flaws are difficult to fix once a protocol is largely deployed. Hence a common practice is to analyze the security of a protocol using formal techniques and in particular automatic tools. This approach has lead to the development of several verification tools such as ProVerif (https://proverif.inria.fr), Tamarin (https://tamarin-prover.github.io) and DeepSec (https://deepsec-prover.github.io) that rely on symbolic models to express protocols and their security properties. Symbolic, automated verification has been a very successful approach for revealing vulnerabilities or proving the absence of entire families of attacks. For instance, these tools were used to verify the security of several major protocols (e.g. TLS 1.3, 5G protocols, Belenios electronic voting protocol).

The problem of verifying security properties (even simple secrecy) is undecidable in general, especially when considering an unlimited number of sessions. For this reason, tools such as ProVerif and Tamarin may not terminate, as they allow users to model unbounded number of sessions. In the vein of [1], many recent features have been introduced in ProVerif to help the tool terminate. However, most of these features require some manual intervention on the part of users, and it can be quite challenging to understand which feature to use depending on the protocol under study. Internally, ProVerif’s core algorithm consists of saturating of a set of Horn clauses with free resolution. In practice, most, if not all, cases of non-termination occur due to the saturation procedure entering an infinite loop. In this project, we aim to develop a procedure that can automatically detect a large class of loops and appropriately apply some of the ProVerif’s features to exit the detected loops.

Objectives:

• get familiar with ProVerif’s saturation procedure (see [1]. The paper [2] is also interesting to have a broader view on ProVerif’s theory)       
• get familiar with the tool itself and the current benchmark for some non-terminating cases        
• design the new algorithm for loop detection and decision of appropriate countermeasures.         
• implement the algorithm and test them on provided benchmarks to evaluate their efficiency.

The library will be incorporated to the official release of ProVerif.

Bibliography: Reading the papers is not mandatory to complete the project but it will provide a good context for the project.

[1] Bruno Blanchet, Vincent Cheval, and Cortier Véronique. Proverif with lemmas, induction, fast subsumption, and much more. In Proceedings of the 43th IEEE Symposium on Security and Privacy (S&P’22). IEEE Computer Society Press, May 2022.

[2] Bruno Blanchet. Modeling and Verifying Security Protocols with the Applied Pi Calculus and ProVerif. Foundations and Trends in Privacy and Security, 1(1-2):1-135, October 2016.

Pre-requisites: Logic and Proof, Functional Programming