postdoc vérification formelle de protocoles de sécurité avec probabilités H/F

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.
Activités :
- 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

Contexte 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.