Vérification de protocoles cryptographiques avec listes de longueur non bornée

In this thesis, we propose two different techniques for verifying security protocols that manipulate lists ofunbounded length.In the first part of the thesis, we present a simple technique for proving secrecy properties for protocols thatmanipulate list elements in a uniform way, for an unbounded number of sessions. More specifically, thistechnique relies on the Horn clause approach used in the automatic verifier ProVerif: we show that if a protocolis proven secure by our technique with lists of length one, then it is secure for lists of unbounded length.Interestingly, this theorem relies on approximations made by our verification technique: in general, secrecy forlists of length one does not imply secrecy for lists of unbounded length.The second technique presented in this thesis automatically proves secrecy and authentication properties forsecurity protocols that manipulate different list elements in different ways. This result is achieved by extendingthe Horn clause approach of the automatic protocol verifier ProVerif. We extend the Horn clauses to be able torepresent lists of unbounded length. We adapt the resolution algorithm to handle the new class of Horn clauses,and prove the soundness of this new algorithm. We have implemented our algorithm and successfully testedit on several protocol examples, including XML protocols coming from web services. Finally, we present anextension of the input language of ProVerif, a variant of the applied pi calculus, to model protocols with lists ofunbounded length, give its formal semantics, and translate it automatically to Horn clauses.Dans cette thèse, nous proposons deux techniques différentes pour la vérification de protocoles de sécurité quiutilisent des listes de taille arbitraire.Dans la première partie de la thèse, nous présentons une technique simple pour vérifier le secret pour desprotocoles qui traitent tous les éléments des listes de façon uniforme, pour un nombre non borné de sessions.Plus précisément, cette technique est fondée sur l’approche à base de clauses de Horn utilisée par le vérificateurautomatique ProVerif. Nous montrons que si un protocole est prouvé sûr par notre technique avec des listes delongueur un, alors il est sûr pour des listes de longueur arbitraire. Curieusement, ce théorème repose sur desapproximations faites par notre technique de vérification : en général, le secret pour des listes de longueur unn’implique pas le secret pour des listes de taille arbitraire.La deuxième technique présentée dans cette thèse permet de prouver automatiquement des propriétés de secretet d’authentification pour des protocoles qui traitent des éléments différents de façon différente. Ce résultat estobtenu en étendant l’approche par clauses de Horn utilisée par ProVerif. Nous étendons la syntaxe des clausesde Horn pour représenter des listes de taille arbitraire. Nous adaptons l’algorithme de résolution pour qu’il traitela nouvelle classe de clauses de Horn et nous prouvons la correction de cet algorithme. Nous avons implémenténotre algorithme et nous l’avons testé avec succès sur plusieurs protocoles, en particulier sur des protocolespour les services web. Finalement, nous présentons une extension du langage d’entrée de ProVerif, une variantedu pi calcul appliqué, pour modéliser les protocoles avec des listes de longueur non bornée, nous en donnonsla sémantique et une traduction automatique en clauses de Horn