Abstract FR:

Dans cette thèse nous étudions la vérification des protocoles cryptographiques. Dans la première partie nous montrons que le problème d'atteignabilité pour des protocoles cryptographiques temporisés bornés est decidable est NP-complet. Notre procédure se base sur un logique de Hoare complète pour des protocoles cryptographiques bornés et un langage de propriétés très expressif. Dans la deuxième partie, en utilisant des techniques d'interpretation abstraite, nous appliquons cette méthode pour vérifier des propriétés de secret pour le protocoles cryptographiques dans un modèle général. Nous traitons un nombre non borné de sessions, de participants et de nonces ain que des messages de taille arbitraire. Nous proposons un algorithme qui calcule un invariant inductif en utilisant des patterns comme représentation symbolique. Cette méthode a été implanté dans l'outil Hermes et validée sur plusieurs etudes de cas.