Abstract FR:

La vérification automatique des protocoles cryptographiques est un problème difficile et aux répercussions économiques importantes. On sait par ailleurs qu'il n'admet pas de solution générale car il est indécidable pour un nombre non borné de sessions. Nous nous intéressons dans cette thèse à l'étude des protocoles comportant un nombre borné de sessions en parallèle. Nous introduisons un système de réduction symbolique qui permet dans ce cadre d'effectuer une vérification exacte de ces protocoles. Afin de rendre cette méthode utilisable en pratique sur des protocoles comportant plusieurs sessions en parallèle, nous développons deux méthodes avancées de réduction de l'espace d'états adaptées à une recherche en profondeur. Enfin, nous présentons TRUST, un outil pour la vérification automatique de protocoles cryptographiques. TRUST intègre l'ensemble de ces résultats théoriques afin de fournir un outil de vérification qui soit à la fois simple à utiliser et efficace.