@COMMENT This file was generated by bib2html.pl version 0.94
@COMMENT written by Patrick Riley
@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&more=yes}{21st
Annual Best of Computing list of notable books and
articles for 2016}}},
}