salle A. Turing CE4
11 avril 2013 - 14h00
vérification formelle des implémentations cryptographiques.
par Maria Christofi de UVSQ
Résumé : Dans une première partie, nous étudions la vérification du protocole mERA à l'aide de l'outil ProVerif. Nous vérifions que ce protocole assure certaines propriétés de sécurité, notamment l'authentification, le secret et la non-reliabilité, ainsi que des propriétés comme la vivacité du protocole.
Dans la deuxième partie, nous étudions la vérification formelle de la résistance des implémentations cryptographiques vis-à-vis d'un ensemble d'attaques spécifiques: les attaques par injection de fautes modifiant les données de l'implémentation. Nous présenterons une nouvelle méthode que nous avons développé vers cette voie en utilisant un outil basé sur l'analyse statique, nommé Frama-C. Afin de mécaniser la vérification, nous avons développé un nouveau plug-in de Frama-C, nommé TL-FACE. Nous avons appliqué cette méthode à une implémentation RSA-CRT munie de la contre-mesure de Vigilant (présentée à CHES 2008). Nous présenterons les résultats de cette vérification à l'aide de l'outil TL-FACE.
