Doctorant en Vérification de protocoles avec opérateurs AC à l'aide de PROVERIF. (M/F)
The French National Centre for Scientific Research (CNRS)
France
Summary
Develop novel resolution techniques for associative-commutative equational theories to improve automated verification of security protocol reachability and equivalence, with formal soundness/completeness analysis and implementation focusing on scalability and termination.