Post-Doctoral Research Visit F/M Verification of messaging protocols and verification of protocols in the presence of key compromise

Funding project

This post-doc position is in the framework of the PEPR Cybersecurity SVP project, a collaborative project on the verification of security protocols, funded by the France 2030 programme. It groups the teams Spicy (IRISA), Pesto (LORIA), Splits (Inria Center of University Cote d'Azur), Inspire (ENS Paris-Saclay) and Prosecco (Inria Paris).

Team

The post-doc will take place in the Prosecco team of Inria Paris. In this team, we develop some of the leading security protocol verification tools (CryptoVerif, Squirrel, formerly ProVerif) and Rust program verification tools (Aeneas), targeting in particular verification of implementations of cryptographic primitives and protocols.

Travel

The post-doc will travel to security conferences, in order to present his research work. Travel expenses are covered within the limits of the scale in force.

The recruited person will do research on the verification of messaging protocols (like Signal, Whatsapp, MLS) and the verification of protocols in case of key compromise. Messaging protocols are widely used and aim at guaranteeing complex security properties in the presence of compromise, such as post-compromise security: the protocols recovers security after a compromise. Hence, they are an interesting target for study. Other protocols are also interesting to study in complex compromise scenarios, for instance the VPN WireGuard, and are also targets for this post-doc.

The research will include theoretical results, case studies using protocol verification tools, and possibly extensions of verification tools.

The considered research directions include:

• proving (parts of) MLS using Squirrel (MLS is a very complex protocol, so we will start with partial proofs);
• proving security protocols using CryptoVerif with complex compromise scenarios;
• designing protocols with as strong as possible post-compromise security properties;
• proving privacy properties (such as anonymity) for messaging protocols;
• detecting the compromise of keys.

The objective will be to publish the research results in major computer security conferences such as IEEE Symposium of Security and Privacy, ACM CCS, Usenix Security, IEEE Computer Security Foundations Symposium.

For more information on our research and our security protocol verification tools, the applicants may consult the web pages of Squirrel https://squirrel-prover.github.io/ and CryptoVerif https://cryptoverif.inria.fr .

This work will be done in collaboration with Adrien Koutsos, who develops in particular Squirrel, and Bruno Blanchet, who develops in particular CryptoVerif.

Main activities :

• Write research papers
• Design new security protocols
• Use protocol verification tools developed in the team Prosecco (Squirrel, CryptoVerif)

Additional activities :

• Extend protocol verification tools developed in the team Prosecco (Squirrel, CryptoVerif)

Technical skills and level required : A successful PhD thesis on the verification of security protocols is required, with publications in some of the major computer security conferences (IEEE Symposium of Security and Privacy, ACM CCS, Usenix Security, IEEE Computer Security Foundations Symposium).

Languages : Fluency in English

Relational skills :

• Reliability.
• Integrity.
• Ability to collaborate with the other members of the team as well as to work autonomously.
• Willingness to learn.

• Subsidized meals
• Partial reimbursement of public transport costs
• Leave: 7 weeks of annual leave + 10 extra days off due to RTT (statutory reduction in working hours) + possibility of exceptional leave (sick children, moving home, etc.)
• Possibility of teleworking and flexible organization of working hours
• Professional equipment available (videoconferencing, loan of computer equipment, etc.)
• Social, cultural and sports events and activities
• Access to vocational training
• Social security coverage