Skip to Main content Skip to Navigation

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 metadata

Cited literature [16 references]  Display  Hide  Download
Contributor : Bruno Blanchet Connect in order to contact the contributor
Submitted on : Monday, December 7, 2015 - 3:52:36 PM
Last modification on : Friday, January 21, 2022 - 3:15:26 AM
Long-term archiving on: : Tuesday, March 8, 2016 - 2:45:00 PM


Files produced by the author(s)


  • HAL Id : hal-01239290, version 1



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⟩



Les métriques sont temporairement indisponibles