Skip to Main content Skip to Navigation
Reports

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.
Complete list of metadatas

Cited literature [16 references]  Display  Hide  Download

https://hal.inria.fr/hal-01239290
Contributor : Bruno Blanchet <>
Submitted on : Monday, December 7, 2015 - 3:52:36 PM
Last modification on : Friday, October 25, 2019 - 3:42:03 PM
Document(s) archivé(s) le : Tuesday, March 8, 2016 - 2:45:00 PM

Files

RR-8823.pdf
Files produced by the author(s)

Identifiers

  • 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⟩

Share

Metrics

Record views

375

Files downloads

145