Formal methods for security protocol correctness
Liviu Pene · 2004
Ce memoire presente deux contributions de recherche dans l'utilisation de techniques formelles pour la verification de protocoles de securite. La premiere contribution traite de la verification des failles de confidentialite dans les protocoles cryptographiques par construction de modeles abstraits. La deuxieme contribution est un cadre pour l'elaboration de preuves de corrections pour une sous classe de protocoles par rapport a la propriete de confidentialite. [...] La structure de ce memoire est comme suit. Au chapitre 2, nous introduisons quelques definitions fondamentales relatives a la cryptographie et aux protocoles de securite. Au chapitre 3, nous presentons l'etat de l'art dans la verification de protocoles de securite. Au chapitre 4, nous presentons une nouvelle methode de verification de protocole de securite basee sur l'interpretation abstraite. Au chapitre 5, nous presentons un cadre de raisonnement formel permettant de verifier la correction des protocoles de securite par rapport a la propriete de confidentialite. Au chapitre 6, nous resumons le travail presente et soulignons nos contributions originales et de possibles developpements futurs de notre travail.