Raffinements de la résolution et vérification de protocoles cryptographiques
Institution:
Cachan, Ecole normale supérieureDisciplines:
Directors:
Abstract EN:
The cryptographie protocols are a field in full extension, in particular with the development of Internet and other supports of remote payments. The formalization of such protocols in the form of clauses is of considerable interest that many results of decidability and proof strategies are already known. We present the architecture of the modular tool of resolution which has developed during the thesis, based on the ordered resolution with function of selection. We show how to treat this refinement of the resolution on an abstract language of terms. Then we present the various languages of concrete terms which we implemented. We show then, in application, how we can use our tool for the checking of cryptographie protocols, in particular for the checking of the protocol of establishment of a group key IKA. 1, using an associative and commutative theory.
Abstract FR:
Les protocoles cryptographiques sont un domaine en pleine extension, notamment avec le développement d'internet et autres supports de règlements à distance. La formalisation de tels protocoles sous forme de clauses présente l'intérêt non négligeable que beaucoup de résultats de décidabilité et de stratégies de preuves sont d'hors et déjà connus. Nous présentons l'architecture de l'outil modulaire de résolution qui a été développé au cours de la thèse, basée sur la résolution ordonnée avec fonction de sélection. Nous montrons comment traiter ce raffinement de la résolution sur un langage de termes abstrait. Puis nous présentons les différents langages de termes concrets que nous avons implémenté. Nous montrons ensuite, en application, comment nous pouvons utiliser notre outil pour la vérification de protocoles cryptographiques, notamment pour la vérification du protocole d'établissement d'une clef de groupe IKA. L, utilisant une théorie associative et commutative.