CCIS Seminar - Thursday 11 April 2013 - salle A. Turing CE4
14:00:00 - Salle de salle A. Turing CE4

Maria Christofi, UVSQ

vérification formelle des implémentations cryptographiques.

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.


Home page CCIS Seminars
How to come to salle A. Turing CE4 - http://www-verimag.imag.fr/Plan-d-acces.html?lang=fr