PaiolaBlanchetInria15

Bruno Blanchet Back to publications

Miriam Paiola and Bruno Blanchet. From the Applied Pi Calculus to Horn Clauses for Protocols with Lists. Research Report RR-8823, Inria, December 2015.

Get the paper

.pdf, 990 Kb

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.

Bibtex


@TECHREPORT{PaiolaBlanchetInria15,
  TITLE = {From the Applied Pi Calculus to {H}orn Clauses for Protocols with Lists},
  AUTHOR = {Paiola, Miriam and Blanchet, Bruno},
  URL = {https://hal.inria.fr/hal-01239290},
  TYPE = {Research Report},
  NUMBER = {RR-8823},
  PAGES = {45},
  INSTITUTION = {{Inria}},
  YEAR = {2015},
  MONTH = DEC,
  PDF = {https://hal.inria.fr/hal-01239290/file/RR-8823.pdf},
  HAL_ID = {hal-01239290},
  HAL_VERSION = {v1}
}

E-mail/Courrier électronique : Bruno.Blanchet@trap-inria.fr (remove trap-)