From the Applied Pi Calculus to Horn Clauses for Protocols with Lists (bibtex)
by Miriam Paiola, Bruno Blanchet
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.
Reference:
From the Applied Pi Calculus to Horn Clauses for Protocols with Lists (Miriam Paiola, Bruno Blanchet), 2015.
Bibtex Entry:
@techreport{paiola:hal-01239290,
  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},
  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.}
}
Powered by bibtexbrowser