Supervisor

Suitable for

Abstract

Prerequisites: Logic and Proof, Functional programming, Model Checking

 

Background

Security protocols are distributed programs designed to ensure security properties — such as confidentiality, authentication, and anonymity — using cryptographic primitives. These protocols are widely employed in a variety of applications, including online commerce, banking systems, mobile devices, and electronic voting. Formal methods have proven to be highly effective in the design and verification of security protocols. They offer rigorous frameworks and techniques that have helped uncover subtle flaws and vulnerabilities in protocol designs, e.g [1,2]

There exist several models for analyzing security protocols. One widely used approach is the symbolic model, where messages are abstractly represented as terms. When protocols involve operators such as exclusive OR (XOR), it becomes essential to reason modulo the equational theory of XOR, which is associative, commutative, and has additional properties such as nilpotency () and the existence of a neutral element (). Taking such properties into account significantly complicates protocol analysis, and many existing tools struggle to handle them effectively.

One of the most popular tools in the field of symbolic verification of security protocols, ProVerif [5] is based on a translation of the verification problem into Horn clauses, coupled with a resolution procedure that is proven correct. However, while correctness is guaranteed, termination is not: it is observed in practice but not ensured in theory. ProVerif has been the subject of initial research aimed at supporting AC operators (associative-commutative), such as XOR or Diffie-Hellman exponentiation, through preprocessing techniques [4]. However, this approach suffers from several limitations and has not been integrated into the main tool. An alternative direction, currently being explored by our team, involves reducing XOR to an AC operator using the so-called finite variant property. While promising, this approach raises concerns: the unification algorithm — a core component of ProVerif — is significantly more expensive modulo AC than it is modulo the theory of XOR, which enjoys better computational properties.

 

Objectives

The first objective of this internship will be to become familiar with the ProVerif tool and its underlying resolution-based procedure. Then, the main goal will be to adapt ProVerif's resolution procedure to natively handle the XOR operator, i.e., without relying on a reduction from XOR to a generic AC operator. This work will involve the following steps:

1.    Propose a new resolution procedure, by adapting the existing one to support XOR directly;

2.    Prove the correctness of the proposed procedure;

3.    Implement the procedure by modifying the current codebase, and evaluate its practical behavior, especially regarding termination. To this end, a set of case studies — such as those presented in [4,3] — will be considered.

Naturally, these three steps are interconnected. In case the procedure fails to terminate in practice, it will be necessary to return to step 1 and refine the method accordingly. The project can be adapted depending on the candidate’s academic level (Part B, C or MsC).

 

Expected skills

We are looking for candidates with a solid background in Foundation of Computer Science, particularly in areas such as logic and automated deduction. Some prior knowledge of security is an asset but is not mandatory. However, a strong interest in programming is essential. The ProVerif tool is implemented in OCaml. This internship may lead to a PhD thesis on similar topics with possible funding through ongoing research projects (e.g., the SVP project, ERC Synergy) within the team.

 

Collaboration

This project will be co supervise with Prof. Stéphanie Delaune from Rennes (France) in the IRISA laboratory. A visit to Rennes may be considered for an in-person meeting with Prof. Stéphanie Delaune.

 

References

[1] Bruno Blanchet. An efficient cryptographic protocol verifier based on prolog rules. In 14th IEEE Computer Security Foundations Workshop (CSFW-14 2001), 11-13 June 2001, Cape Breton, Nova Scotia, Canada, pages 82–96. IEEE Computer Society, 2001.

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

[3] Jannik Dreier, Lucca Hirschi, Sasa Radomirovic, and Ralf Sasse. Automated unbounded verification of stateful cryptographic protocols with exclusive OR. In 31st IEEE Computer Security Foundations Symposium, CSF 2018, Oxford, United Kingdom, July 9-12, 2018, pages 359–373. IEEE Computer Society, 2018.

[4] Ralf Küsters and Tomasz Truderung. Reducing protocol analysis with XOR to the xor-free case in the horn theory based approach. J. Autom. Reason., 46(3-4) :325–352, 2011.

[5] ProVerif. https://bblanche.gitlabpages.inria.fr/proverif/, 2001.