Doctorant en Vérification de protocoles avec opérateurs AC à l'aide de PROVERIF. (M/F)

Job Description

Thesis Subject

Verifying protocols with AC operators using PROVERIF

Formal verification relies on mathematical reasoning techniques to establish properties of complex distributed systems. In symbolic verification frameworks, system behaviours and data manipulations are represented as algebraic terms and analysed using automated deduction procedures. A central difficulty in this setting lies in the treatment of algebraic structures that satisfy non-trivial equational properties, in particular associativity and commutativity. Supporting such theories significantly increases the complexity of automated reasoning procedures and raises fundamental questions regarding soundness, completeness,
and termination.
PROVERIF is a widely used automated reasoning tool based on a translation of verification problems into Horn clauses [5], together with a resolution procedure that is proven sound [1, 2]. While soundness is guaranteed, termination is not ensured in general, although it is often observed in practice.
Several extensions have been investigated in order to integrate associative-commutative (AC) theories into this framework, including theories related to XOR, Abelian Groups, and Diffie–Hellman exponentiation, mainly through preprocessing techniques [4]. However, these approaches suffer from important limitations and have not been integrated into the main tool. Recently, we extended PROVERIF to support XOR for the analysis of reachability properties [3]. Building upon this work, the objective of this PhD project is to develop new resolution techniques capable of handling richer classes of associative-commutative equational theories within the same automated reasoning framework.
Objectives of the PhD project. The first objective of the PhD project will be to acquire a thorough understanding of the PROVERIF resolution engine and its underlying theoretical foundations.
The main scientific goal will then be to extend this resolution procedure to support additional associative-commutative equational theories, such as Abelian Groups (AG), Diffie-Hellman exponentiation, or bilinear pairings. The initial focus will be on reachability properties.
1
More precisely, the PhD project will consist of the following tasks :
1. Design a new resolution procedure by adapting the existing framework to support richer associative-commutative theories ;
2. Establish the soundness and, whenever possible, completeness properties of the proposed procedure ;
3. Implement the new procedure within the PROVERIF codebase and evaluate its practical behaviour, with particular attention to scalability and termination issues.

These three research directions are strongly interconnected. In particular, should the proposed procedure exhibit poor termination behaviour in practice, the theoretical framework will need to be refined accordingly.

Once a first extension has been successfully developed, several research directions may be explored, including the analysis of equivalence properties and the support of user-defined associative-commutative operators.

Références
[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] Vincent Cheval and Stéphanie Delaune. Symbolic protocol verification modulo xor in proverif. In Proceedings of the 33rd ACM Conference on Computer and Communications Security (CCS'26). ACM Press, November 2026.
[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.

Keywords. protocols, formal verification, symbolic model, AC opertors, PROVERIF

Laboratory, institution and university. The thesis will take place at IRISA (Rennes).
Team or project of the Lab. Team SPICY at IRISA.
Name and email address of the advisor.
Stéphanie Delaune, Stephanie.Delaune@irisa.fr
Grant. The PhD thesis is supported by the SVP Project (PEPR Cybersécurité).
https://pepr-cyber-svp.cnrs.fr/

Your Work Environment

About the Laboratory
www.irisa.fr
IRISA is currently one of France's largest research laboratories (with over 850 people) in the fields of computer science and information technology. Organized into seven scientific departments, IRISA is a laboratory of excellence whose scientific priorities include bioinformatics, system security, new software architectures, virtual reality, big data analysis, and artificial intelligence. Focused on the future of computing and inherently international in scope, IRISA is at the very heart of society's digital transformation and innovation, serving fields such as cybersecurity, health, environment and ecology, transportation, robotics, energy, culture, and artificial intelligence.
Presentation of CNRS as an employer: https://www.cnrs.fr/en/cnrs
Presentation of IRISA as the host laboratory: https://www.irisa.fr/umr-6074
The position is in a sector subject to the protection of scientific and technical potential (PPST), and therefore, in accordance with regulations, your appointment must be authorized by the competent authority of the MESR (Ministry of Higher Education and Research).

Compensation and benefits

Compensation

2300 € gross monthly

Annual leave and RTT

44 jours

Remote Working practice and compensation

Pratique et indemnisation du TT

Transport

Prise en charge à 75% du coût et forfait mobilité durable jusqu’à 300€

About the offer

About the CNRS

The CNRS is a major player in fundamental research on a global scale. The CNRS is the only French organization active in all scientific fields. Its unique position as a multi-specialist allows it to bring together different disciplines to address the most important challenges of the contemporary world, in connection with the actors of change.

CNRS

The research professions