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).

Of the three aforementioned tools, ProVerif is generally considered to be the most efficient. It is also the only tool that does not rely on distributed or parallel computing. ProVerif’s internal procedure is based on the saturation of sets of Horn clauses which is inherently more suited to sequential computing. However, several time-consuming algorithms used in the saturation procedure can greatly benefit from parallel computing, such as Horn clauses subsumption checking, unification and matching of terms modulo an equational theory. This project aims to transform many algorithms used in ProVerif using the multicore programming framework that is provided in OCaml 5. We can expect significant speedup as, for instance, Horn clauses subsumption checking represents usually 80 to 90% of the total execution time of ProVerif. One of the difficulties however will be to appropriately combine parallel computing algorithm with other optimization features already implemented that are specifically tailored for sequential computing (such as hash consing techniques).

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)         
• identify the components in ProVerif’s saturation procedure that can benefit from concurrent programming        
• design the new algorithms for these components        
• evaluate the efficiency impact on the overall execution time (a benchmark is provided).

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. Modelling 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, Concurrent Programming