From the Applied Pi Calculus to Horn Clauses for Protocols with Lists

Résumé : 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.
Type de document :
Rapport
[Research Report] RR-8823, Inria. 2015, pp.45
Liste complète des métadonnées

https://hal.inria.fr/hal-01239290
Contributeur : Bruno Blanchet <>
Soumis le : lundi 7 décembre 2015 - 15:52:36
Dernière modification le : vendredi 16 septembre 2016 - 15:07:56
Document(s) archivé(s) le : mardi 8 mars 2016 - 14:45:00

Fichiers

RR-8823.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01239290, version 1

Collections

Citation

Miriam Paiola, Bruno Blanchet. From the Applied Pi Calculus to Horn Clauses for Protocols with Lists. [Research Report] RR-8823, Inria. 2015, pp.45. <hal-01239290>

Partager

Métriques

Consultations de
la notice

183

Téléchargements du document

45