Postdoc vérification formelle de protocoles de sécurité avec probabilités h/f

Informations générales Organisme de rattachement CNRS Référence UMR7503-VERCOR-005 Date de début de diffusion 05/03/2026 Date de parution 08/03/2026 Date de fin de diffusion 26/03/2026 Intitulé long de l'offre postdoc vérification formelle de protocoles de sécurité avec probabilités H/F Date limite de candidature 26/03/2026 Nature du contrat CDD d'1 an Versant Fonction Publique de l'Etat Catégorie Catégorie A (cadre) Nature de l'emploi Emploi ouvert uniquement aux contractuels Domaine / Métier Recherche - Chercheuse / Chercheur Statut du poste Vacant Intitulé du poste postdoc vérification formelle de protocoles de sécurité avec probabilités H/F Descriptif de l'employeur Le Centre national de la recherche scientifique est un organisme public de recherche pluridisciplinaire placé sous la tutelle du ministère de l’Enseignement supérieure et de la Recherche. Créé en 1939 et dirigé par des scientifiques, il a pour mission de faire progresser la connaissance et être utile à la société dans le respect des règles d’éthique, de déontologie et d’intégrité scientifique. Description du poste 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. Conditions particulières d'exercice Le Centre national de la recherche scientifique est l’une des plus importantes institutions publiques au monde : 34 000 femmes et hommes (plus de 1 000 laboratoires et 200 métiers), en partenariat avec les universités et les grandes écoles, y font progresser les connaissances en explorant le vivant, la matière, l’Univers et le fonctionnement des sociétés humaines. Depuis plus de 80 ans, y sont développées des recherches pluri et interdisciplinaires sur tout le territoire national, en Europe et à l’international. Le lien étroit que le CNRS tisse entre ses missions de recherche et le transfert vers la société fait de lui un acteur clé de l’innovation en France et dans le monde. Le partenariat qui le lie avec les entreprises est le socle de sa politique de valorisation et les start-ups issues de ses laboratoires (près de 100 chaque année) témoignent du potentiel économique de ses travaux de recherche. Descriptif du profil recherché Competences : 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. Contraintes et risques : Temps plein Oui Rémunération contractuels (en € brut/an) entre 3071,50 et 3501,51 euros bruts Localisation du poste Europe, France, Grand Est, Meurthe et Moselle (54) Géolocalisation du poste VANDOEUVRE LES NANCY Lieu d'affectation (sans géolocalisation) 54506 VANDOEUVRE LES NANCY (France) Critères candidat Niveau d'études / Diplôme Niveau 8 Doctorat/diplômes équivalents Spécialisation Formations générales Langues Français (Seuil)