Contexte et atouts du poste

ProVerif est un vérificateur de protocoles cryptographiques dans lequel de nombreux protocols ont été vérifiés (et corrigés), entre autre TLS, le protocol de messagerie instantanée Signal, des protocoles d'avionique et de vote électronique.

Dans le cadre du projet PIQ VIP et d'une collaboration entre les équipes VeriDis et Pesto d'Inria, l'objectif du postdoc est d'augmenter la confiance dans ProVerif, et de faciliter l'exploration théorique d'extensions à cet outil.

Pour cela, le ou la postdoc utilisera l'assistant à la preuve Isabelle/HOL, qui permet d'exprimer des énoncés mathématiques et leurs preuves, qui sont automatiquement vérifiés par l'outil. Isabelle/HOL inclue une grande librairie de résultats en mathématique, logique et informatique, et est utilisé pour la vérification de projets de grande ampleur comme le microkernel Sel4.

Mission confiée

Missions :
Avec l'aide d...