PhD on formal verification of electronic voting protocols (M/F)
New
- FTC PhD student / Offer for thesis
- 36 month
- BAC+5
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
FTC PhD student / Offer for thesis
Working hHours
Full Time
Workplace
54506 VANDOEUVRE LES NANCY
Contract Duration
36 month
Date of Hire
01/09/2026
Remuneration
2300 € gross monthly
Apply Application Deadline : 24 June 2026 23:59
Job Description
Thesis Subject
In recent years, electronic voting protocols have been increasingly used in sensitive contexts, such as union and political elections, and even national elections in some countries. Given these high-stakes situations, it is important to ensure the security of the underlying cryptographic protocols.
Two main families of models exist for proving protocol security: symbolic models, where messages are abstracted as terms, and computational models, which are more precise, treating messages as arbitrary bitstrings. The former have enabled the development of automated tools for security proofs, while the latter provide stronger security guarantees but are harder to automate.
One solution is to rely on interactive provers to perform security proofs in computational models, with a computer then confirming the validity of the proof. However, such strong-guarantee proofs remain rare in the context of electronic voting. The Squirrel interactive prover—a protocol prover we are developing in the team—offers the prospect of making such proofs feasible on a larger scale. This thesis will therefore focus on using the Squirrel prover to develop proofs for increasingly complex electronic voting protocols.
This research field is still young, with only a first security proof in Squirrel for an older electronic voting protocol. To advance further, this thesis may include developing innovative extensions to its underlying logic or to the tool itself.
Finally, faced with the threat quantum computers pose to classical cryptography in the coming decades, this thesis would aim to verify the everlasting privacy of votes, or even verifiability against quantum attackers. Note that Squirrel already provides guarantees against quantum attacks and is therefore suitable for this specific use case.
Your Work Environment
The thesis will take place within the PESTO team at LORIA. This team has extensive experience in electronic voting, having studied numerous systems in France and abroad (e.g., the Geneva canton system, Scytl, SwissPost), and worked on theoretical aspects such as selecting and designing appropriate security definitions and detecting vulnerabilities. More broadly, the PESTO team focuses on developing formal methods to prove protocol security and has contributed to the development of many tools for this purpose, including ProVerif, Tamarin, Jasmin, DeepSec, Sapic+, and, of course, the Squirrel Prover.
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
| Offer reference | UMR7503-VERCOR-006 |
|---|---|
| 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.