Steve Kremer: Automated verification of equivalence properties of cryptographic protocol

Automated verification of equivalence properties of cryptographic protocol

Rohit Chadha, Vincent Cheval, Ștefan Ciobâcă, and Steve Kremer. Automated verification of equivalence properties of cryptographic protocol. ACM Transactions on Computational Logic, 17(4):1–32, November 2016. Listed in ACM Computing Reviews' 21st Annual Best of Computing list of notable books and articles for 2016.
doi:10.1145/2926715

Download

[PDF] [HTML]

Abstract

Indistinguishability properties are essential in formal verification of cryptographic protocols. They are needed to model anonymity properties, strong versions of confidentiality and resistance against offline guessing attacks. Indistinguishability properties can be conveniently modeled as equivalence properties. We present a novel procedure to verify equivalence properties for a bounded number of sessions of cryptographic protocols. As in the applied pi-calculus, our protocol specification language is parametrized by a first-order sorted term signature and an equational theory which allows formalization of algebraic properties of cryptographic primitives. Our procedure is able to verify trace equivalence for determinate cryptographic protocols. On determinate protocols, trace equivalence coincides with observational equivalence which can therefore be automatically verified for such processes. When protocols are not determinate our procedure can be used for both under- and over-approximations of trace equivalence, which proved successful on examples. The procedure can handle a large set of cryptographic primitives, namely those whose equational theory is generated by an optimally reducing convergent rewrite system. The procedure is based on a fully abstract modelling of the traces of a bounded number of sessions of the protocols into first-order Horn clauses on which a dedicated resolution procedure is used to decide equivalence properties. We have shown that our procedure terminates for the class of subterm convergent equational theories. Moreover, the procedure has been implemented in a prototype tool A-KiSs (Active Knowledge in Security Protocols) and has been effectively tested on examples. Some of the examples were outside the scope of existing tools, including checking anonymity of an electronic voting protocol due to Okamoto.

BibTeX

@Article{CCCK16,
  abstract =	 {Indistinguishability properties are essential in
                  formal verification of cryptographic protocols. They
                  are needed to model anonymity properties, strong
                  versions of confidentiality and resistance against
                  offline guessing attacks. Indistinguishability
                  properties can be conveniently modeled as
                  equivalence properties. We present a novel procedure
                  to verify equivalence properties for a bounded
                  number of sessions of cryptographic protocols. As in
                  the applied pi-calculus, our protocol specification
                  language is parametrized by a first-order sorted
                  term signature and an equational theory which allows
                  formalization of algebraic properties of
                  cryptographic primitives. Our procedure is able to
                  verify trace equivalence for determinate
                  cryptographic protocols. On determinate protocols,
                  trace equivalence coincides with observational
                  equivalence which can therefore be automatically
                  verified for such processes. When protocols are not
                  determinate our procedure can be used for both
                  under- and over-approximations of trace equivalence,
                  which proved successful on examples. The procedure
                  can handle a large set of cryptographic primitives,
                  namely those whose equational theory is generated by
                  an optimally reducing convergent rewrite system. The
                  procedure is based on a fully abstract modelling of
                  the traces of a bounded number of sessions of the
                  protocols into first-order Horn clauses on which a
                  dedicated resolution procedure is used to decide
                  equivalence properties. We have shown that our
                  procedure terminates for the class of subterm
                  convergent equational theories. Moreover, the
                  procedure has been implemented in a prototype tool
                  A-KiSs (Active Knowledge in Security Protocols) and
                  has been effectively tested on examples. Some of the
                  examples were outside the scope of existing tools,
                  including checking anonymity of an electronic voting
                  protocol due to Okamoto.},
  author =	 {Chadha, Rohit and Cheval, Vincent and
                  Ciob{\^a}c{\u{a}}, {\c{S}}tefan and Kremer, Steve},
  title =	 {Automated verification of equivalence properties of
                  cryptographic protocol},
  journal =	 {ACM Transactions on Computational Logic},
  doi =		 {10.1145/2926715},
  volume =	 17,
  number =	 4,
  pages =	 {1--32},
  month =	 nov,
  nmonth =	 11,
  year =	 2016,
  url =		 {https://hal.inria.fr/hal-01306561/document},
  note =	 {\textbf{Listed in ACM Computing Reviews'
                  \href{http://www.computingreviews.com/recommend/bestof/notableitems.cfm?bestYear=2016&amp;more=yes}{21st
                  Annual Best of Computing list of notable books and
                  articles for 2016}}},
}