postdoc on formal verifiication of security protocols with probabilities (M/F)
New
- Researcher in FTC
- 12 mounth
- Doctorate
This offer is available in English version
This offer is open to people with a document recognizing their status as a disabled worker.
Offer at a glance
The Unit
Laboratoire lorrain de recherche en informatique et ses applications
Contract Type
Researcher in FTC
Working hHours
Full Time
Workplace
54506 VANDOEUVRE LES NANCY
Contract Duration
12 mounth
Date of Hire
01/04/2026
Remuneration
between 3071,50 and 3501,51 euros (gross salary)
Apply Application Deadline : 26 March 2026 23:59
Job Description
Missions
The overall objective of this postdoctoral position is to enable the formal verification of security protocols involving non-negligible probabilities.
Formal methods have proven their value in the design and analysis of security protocols. They provide rigorous frameworks and techniques that have uncovered new vulnerabilities. In particular, ProVerif is a state-of-the-art tool dedicated to the security analysis of protocols. It has been successfully applied to numerous protocols in the literature, providing security proofs or revealing new attacks.
However, these formal (or symbolic) models do not allow for the modeling of probabilistic behaviors, such as when a protocol agent makes a random choice. This is particularly relevant in electronic voting, where some protocols assume that voters randomly select one of two received ballots. It also applies to protocols using "short" codes, where these codes have a non-negligible probability of being guessed by an attacker.
The goal of this postdoctoral research is to develop new methods for automatically analyzing properties of probabilistic security protocols. One approach will be to identify sufficient conditions that can be proven using existing tools such as ProVerif.
Activity
Research meetings
Drafting papers as progress is made
Design of definitions and proofs
Writing research articles
Participating in team seminars and conferences
Your Profil
Skills
The candidate must hold a PhD and have training in security protocol verification in symbolic models, or possess strong expertise in formal verification and logic.
Your Work Environment
The work will be carried out within the Pesto team at LORIA.
The Pesto team focuses on the formal analysis of security protocols and studies numerous protocols, including electronic voting. The team has developed several algorithms to prove protocol security and regularly contributes to tools such as ProVerif and Tamarin.
Compensation and benefits
Compensation
between 3071,50 and 3501,51 euros (gross salary)
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
| Offer reference | UMR7503-VERCOR-005 |
|---|---|
| CN Section(s) / Research Area | Information sciences: bases of information technology, calculations, algorithms, representations, uses |
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.
Create your alert
Don't miss any opportunity to find the job that's right for you. Register for free and receive new vacancies directly in your mailbox.