Automated verification of equivalence properties of cryptographic protocols
Rohit Chadha, Ștefan Ciobâcă, and Steve Kremer. Automated verification of equivalence properties of cryptographic protocols. In Programming Languages and Systems ---Proceedings of the 21th European Symposium on Programming (ESOP'12), pp. 108–127, Lecture Notes in Computer Science 7211, Springer, Tallinn, Estonia, March 2012.
doi:10.1007/978-3-642-28869-2_6
Download
[PDF] [PDF (long version)] [HTML]
Abstract
Indistinguishability properties are essential in formal verification of cryptographic protocols. They are needed to model anonymity of cryptographic protocols. They are needed to model anonymity properties, strong versions of confidentiality and resistance to offline guessing attacks, and can be conveniently modeled using process equivalences. We present a novel procedure to verify equivalence properties for bounded number of sessions. 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 which can be modeled by an optimally reducing convergent rewrite system. Although, we were unable to prove its termination, it has been implemented in a prototype tool and has been effectively tested on examples, some of which were outside the scope of existing tools.
BibTeX
@inproceedings{CCK-esop12,
abstract = {Indistinguishability properties are essential in
formal verification of cryptographic protocols. They
are needed to model anonymity of cryptographic
protocols. They are needed to model anonymity
properties, strong versions of confidentiality and
resistance to offline guessing attacks, and can be
conveniently modeled using process equivalences. We
present a novel procedure to verify equivalence
properties for bounded number of sessions. 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 which can be
modeled by an optimally reducing convergent rewrite
system. Although, we were unable to prove its
termination, it has been implemented in a prototype
tool and has been effectively tested on examples,
some of which were outside the scope of existing
tools.},
address = {Tallinn, Estonia},
author = {Chadha, Rohit and Ciob{\^a}c{\u{a}}, {\c{S}}tefan and Kremer, Steve},
booktitle = {{P}rogramming {L}anguages and {S}ystems~---{P}roceedings of the 21th {E}uropean {S}ymposium on {P}rogramming ({ESOP}'12)},
DOI = {10.1007/978-3-642-28869-2_6},
editor = {Seidl, Helmut},
month = mar,
pages = {108-127},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
title = {Automated verification of equivalence properties of
cryptographic protocols},
volume = {7211},
year = {2012},
acronym = {{ESOP}'12},
nmonth = {3},
}