Modélisation et vérification de protocoles dans le modèle calculatoire avec Squirrel

L'assistant de preuve Squirrel est dédié à la vérification de protocoles cryptographiques. Le modèle utilisé par ce prouveur est appelé modèle calculatoire. Il assure un haut niveau de garanties de sécurité, mais souffre d'un manque d'automatisation. Cette thèse propose d'utiliser des méthodes symboliques et de les adapter pour le modèle calculatoire de Squirrel. Tout d'abord, les protocoles dans Squirrel sont déclarés par des processus écrits dans une variante du pi-calcul appliqué. La sémantique de ces processus n'a pas été définie dans l'article initial présentant Squirrel. L'outil utilise à la place une représentation nommée systèmes d'actions, pour laquelle une sémantique bien définie existe. La première contribution de cette thèse est de définir cette sémantique et de fournir une traduction correcte du pi-calcul vers la représentation interne des protocoles de l'outil. Ensuite, pour automatiser les preuves écrites avec Squirrel, nous concevons un système de types pour les preuves de secret dans le modèle calculatoire. Nous prouvons la correction de ce système de types et l'implémentons dans l'outil, en supportant le chiffrement symétrique et asymétrique.