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

Abstract : 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.
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, May 25, 2018 - 12:02:06 PM
Long-term archiving on : 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

350

Files downloads

134