Méthodes algorithmiques de vérification des protocoles cryptographiques

Gilles BARTHE, researcher INRIA Sophia-Antipolis (Reviewer) Michael RUSINOWITCH, researcher LORIA-INRIA-Lorraine (Reviewer) Yassine LAKHNECH, professor Joseph Fourier University (Advisor) Florian BOIAN, professor "Babes-Bolyai" University (Examiner) Francis KLAY, researcher R&D at France Telecom (Examiner)Cryptographic protocols play a major role in any application where data integrity, confidentiality, authenticity and other security related properties are crucial. Such applications include Smart-Cards, e-business, electronic vote or internet-based contract signing. In the first part of thesis, we show that the reachability problem for timed bounded cryptographic protocols and security properties, such as secret and authentication, is decidable and NP-complete. Our procedure is based on a complete and effective Hoare logic for timed bounded cryptographic protocols and an expressive assertion language. In the second part, using abstract interpretation techniques, we apply this method for verifying secrecy properties of cryptographic protocols in a general setting. We deal with unbounded number of sessions, unbounded number of principals, unbounded message depth and unbounded creation of fresh nonces. We provide an algorithm which computes an inductive invariant using patterns as symbolic representation. This algorithm has been implemented in the Hermes tool and has been validated on several case studies.Les protocoles cryptographiques jouent un rôle majeur dans les applications ou l'intégrité des données, la confidentialité, l'authenticité et autres propriétés sont essentielles. Ils sont utilisés par exemple dans le commerce électronique, la téléphonie mobile, le vote électronique. Dans la première partie de la thèse nous montrons que le problème d'atteignabilité pour des protocoles cryptographiques temporisés bornés est décidable est NP-complet. Notre procédure se base sur une 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'interprétation abstraite, nous appliquons cette méthode pour vérifier des propriétés de secret pour les protocoles cryptographiques dans un modèle général. Nous traitons un nombre non borné de sessions, de participants et de nonces ainsi 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 études de cas