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

Due to the critical aspect of these security protocols, it is crucial to guarantee that possible bugs in these automatic tools do not affect the correctness of the security proofs. In addition, even though the efficiency of these tools have significantly improved over the years, the verification of real-life protocols may require an large amount time and memory to terminate. For instance, when the verification requires more than 200GB of memory, as it was the case for verifying privacy properties of an extension of TLS 1.3, the reproducibility of the verification results is severely affected.To tackle this problem, the approach taken in this project is to develop proof certificates that can be verified by a machine-checked verifier. One of the main difficulty is to ensure that certificates are sufficiently small in practice (in order that they can be easily exchanged) while guaranteeing a relatively small verification time. The certificate generation and verification will be based on ProVerif internal procedure.

Objectives:

• define the formal content of the certificate to be generated by ProVerif
• propose an algorithm to verify the certificate and prove its correctness (by hand) 
• implement the generation of certificate in ProVerif 
• implement the prover and its proof of correctness with F*[1]

We do not expect for the last objective to be fully completed as the implementation in F* may be extremely time consuming. However, a partial implementation will be elaborated.

[1] https://www.fstar-lang.org

[2] 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.

Pre-requisites: Logic and Proof, Functional Programming, (CAFV is a plus)