From the Applied Pi Calculus to Horn Clauses for Protocols with Lists
Du pi calcul appliqué aux clauses de Horn pour les protocoles qui utilisent des listes
Résumé
Recently, we presented an automatic technique for proving secrecy and authentication properties for security protocols that manipulate lists of unbounded length, for an unbounded number of sessions. That work relies on an extension of Horn clauses, generalized Horn clauses, designed to support unbounded lists, and on a resolution algorithm on these clauses. However, in that previous work, we had to model protocols manually with generalized Horn clauses, which is unpractical.
In this work, we present an extension of the input language of ProVerif, a variant of the applied pi calculus, to model protocols with lists of unbounded length. We give its formal meaning, translate it automatically to generalized Horn clauses, and prove that this translation is sound.
Nous avons récemment présenté une technique automatique pour prouver des propriétés de secret et d'authentification pour des protocoles cryptographiques qui manipulent des listes de longueur non-bornée. Ce travail est fondé sur une extension des clauses de Horn, les clauses de Horn généralisées, conçue pour traiter les listes non-bornées, et sur un algorithme de résolution sur ces clauses. Cependant, dans ce travail précédent, nous devions modéliser les protocoles manuellement avec des clauses de Horn généralisées, ce qui est compliqué en pratique. Dans ce rapport, nous présentons une extension du langage d'entrée de ProVerif, une variante du pi calcul appliqué, pour modéliser les protocoles avec des listes de longueur non-bornée. Nous définissons sa signification formelle, le traduisons automatiquement en clauses de Horn généralisées, et prouvons que cette traduction est correcte.
Origine : Fichiers produits par l'(les) auteur(s)
Loading...