Doctorant (H/F) sur la vérification formelle de protocoles de vote électronique
Nouveau
- CDD Doctorant
- 36 mois
- BAC+5
L'offre en un coup d'oeil
L'unité
Laboratoire lorrain de recherche en informatique et ses applications
Type de Contrat
CDD Doctorant
Temps de Travail
Complet
Lieu de Travail
54506 VANDOEUVRE LES NANCY
Durée du contrat
36 mois
Date d'Embauche
01/09/2026
Rémuneration
La rémunération est d'un minimum de 2300,00 € mensuel
Postuler Date limite de candidature : mercredi 24 juin 2026 23:59
Description du Poste
Sujet De Thèse
Ces dernières années, les protocoles de vote électronique sont de plus en plus utilisés dans des contextes sensibles, tels que les élections syndicales et politiques, voire les élections nationales dans certains pays. Face à ces situations à haut risque, il est impératif de garantir la sécurité des protocoles cryptographiques sous-jacents.
Deux grandes familles de modèles existent pour prouver la sécurité des protocoles : les modèles dits symboliques où les messages sont abstraits par des termes et les modèles dits computationnels, plus précis où les messages sont des suites de bits arbitraires. Les premiers modèles ont permis le développements d'outils automatiques pour la preuve de sécurité. Les deuxièmes apportent des meilleures garanties de sécurité mais les preuves sont plus difficiles à automatiser.
Une solution consiste à s'appuyer sur des prouveurs interactifs pour effectuer les preuves de sécurité dans des modèles computationnels, un ordinateur confirmant alors la validité de la preuve. Cependant, de telles preuves fournissant des garanties fortes restent rares dans le contexte du vote électronique. Le prouveur interactif Squirrel, un prouveur de protocole que nous développons par ailleurs, offre la perspective de rendre possible de telles preuves à plus grande échelle. Cette thèse se concentrera donc sur l'utilisation du démonstrateur Squirrel pour développer des preuves de protocoles de vote électronique de plus en plus complexes.
Ce domaine de recherche est encore jeune, avec uniquement une première preuve de sécurité en Squirrel d'un protocol de vote électronique ancien. Pour permettre d'aller plus loin, cette thèse pourra notamment inclure le développement d'extensions novatrices de sa logique sous-jacente ou de l'outil lui-même.
Enfin, face à la menace que représentent les ordinateurs quantiques pour la cryptographie classique dans les décennies à venir, cette thèse s'attacherait à vérifier la confidentialité permanente des votes (everlasting privacy) voire à la vérifiabilité face à un attaquant quantique. Notons que Squirrel offre déjà des garanties contre les attaques quantiques et convient donc à ce cas d'utilisation spécifique.
Votre Environnement de Travail
La thèse se déroulera au sein de l'équipe PESTO au LORIA. Cette équipe possède une solide expérience du vote électronique, ayant étudié de nombreux systèmes en France et à l'étranger (système du canton de Genève, Scytl), et travaillé sur les aspects théoriques (choix et conception des définitions de sécurité appropriées, détection des failles). Plus généralement, l'équipe PESTO se concentre sur le développement de méthodes formelles pour prouver la sécurité des protocoles et a participé au développement de nombreux outils à cet effet, tels que ProVerif, Tamarin, Jasmin, DeepSec, Sapic+ et, bien sûr, le Squirrel Prover.
Rémunération et avantages
Rémunération
La rémunération est d'un minimum de 2300,00 € mensuel
Congés et RTT annuels
44 jours
Pratique et Indemnisation du TT
Pratique et indemnisation du TT
Transport
Prise en charge à 75% du coût et forfait mobilité durable jusqu’à 300€
À propos de l’offre
| Référence de l’offre | UMR7503-VERCOR-006 |
|---|---|
| Section(s) CN / Domaine de recherche | Sciences informatiques : fondements de l'informatique, calculs, algorithmes, représentations, exploitations |
À propos du CNRS
Le CNRS est un acteur majeur de la recherche fondamentale à une échelle mondiale. Le CNRS est le seul organisme français actif dans tous les domaines scientifiques. Sa position unique de multi-spécialiste lui permet d’associer les différentes disciplines pour affronter les défis les plus importants du monde contemporain, en lien avec les acteurs du changement.
Créer une alerte
Ne manquez aucune opportunité de trouver le poste qui vous correspond. Inscrivez-vous gratuitement et recevez les nouvelles offres directement dans votre boite mail.