postdoc vérification formelle de protocoles de sécurité avec probabilités H/F
Nouveau
- Chercheur en contrat CDD
- 12 mois
- Doctorat
L'offre en un coup d'oeil
L'unité
Laboratoire lorrain de recherche en informatique et ses applications
Type de Contrat
Chercheur en contrat CDD
Temps de Travail
Complet
Lieu de Travail
54506 VANDOEUVRE LES NANCY
Durée du contrat
12 mois
Date d'Embauche
01/04/2026
Rémuneration
entre 3071,50 et 3501,51 euros bruts
Postuler Date limite de candidature : jeudi 26 mars 2026 23:59
Description du Poste
Les Missions
L'objectif général de postdoc est de permettre la vérification formelle de protocoles de sécurité, avec des probabilités non négligeables
Les méthodes formelles ont démontré leur utilité dans la conception et l’analyse des protocoles de sécurité. Elles offrent en effet des cadres et des techniques rigoureux qui ont permis de découvrir de nouvelles failles. En particulier, ProVerif est un outil de pointe dédié à l’analyse de sécurité des protocoles. Il a été appliqué avec succès à de nombreux protocoles de la littérature, fournissant des preuves de sécurité ou révélant de nouvelles attaques.
Cependant, ces modèles formels (ou symboliques) ne permettent pas de modéliser des comportements probabilistes, par exemple quand un agent du protocole fait un choix aléatoire. C'est notamment le cas das le vote électronique où certains protocoles supposent que les électeurs font choisir au hasard de voter avec l'une des deux feuilles de vote reçues. C'est également le cas des protocoles avec codes "courts" où ces codes ont une probabilité non négligeable d'être devinés par l'attaquant.
L'objectif de ce postdoc est de développer de nouvelles méthodes pour analyser automatiquement des propriétés sur des protocoles de sécurité probabilistes. Une piste sera d'identifier des conditions suffisantes, prouvables dans des outils existants comme ProVerif.
L'Activité
- réunions de recherche
- rédaction de draft au fur et à mesure de l'avancement
- mise au point de définitions et de preuves
- rédactions d'article
- participation aux séminaires d'équipe et à des conférences
Votre Profil
Compétences
Le candidat ou la candidate devra avoir une thèse et être formé.e à la preuve de sécurité des protocoles, dans des modèles symboliques ou bien avoir une forte compétence en vérification formelle et logique.
Votre Environnement de Travail
Le travail sera effectué au sein de l'équipe Pesto du LORIA.
L'équipe Pesto s'intéresse à l'analyse formelle de protocoles de sécurité et étudie de nombreux protocoles dont le vote électronique. Ainsi l'équipe a développé de nombreux algorithmes pour prouver la sécurité des protocoles et contribue régulièrement à des outils comme ProVerif ou Tamarin.
Rémunération et avantages
Rémunération
entre 3071,50 et 3501,51 euros bruts
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-005 |
|---|---|
| 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.