DEEPSEC: Deciding Equivalence Properties in Security Protocols - Theory and Practice
Vincent Cheval, Steve Kremer, and Itsaka Rakotonirina. DEEPSEC: Deciding Equivalence Properties in Security Protocols - Theory and Practice. In Proceedings of the 39th IEEE Symposium on Security and Privacy (S&P'18), pp. 525–542, IEEE Computer Society Press, San Francisco, CA, USA, May 2018. Distinguished paper award.
doi:10.1109/SP.2018.00033
Download
[PDF] [PDF (long version)] [HTML]
Abstract
Automated verification has become an essential part in the security evaluation of cryptographic protocols. Recently, there has been a considerable effort to lift the theory and tool support that existed for reachability properties to the more complex case of equivalence properties. In this paper we contribute both to the theory and practice of this verification problem. We establish new complexity results for static equivalence, trace equivalence and labelled bisimilarity and provide a decision procedure for these equivalences in the case of a bounded number of sessions. Our procedure is the first to decide trace equivalence and labelled bisimilarity exactly for a large variety of cryptographic primitives---those that can be represented by a subterm convergent destructor rewrite system. We implemented the procedure in a new tool, Deepsec. We showed through extensive experiments that it is significantly more efficient than other similar tools, while at the same time raises the scope of the protocols that can be analysed.
BibTeX
@inproceedings{CKR-sp18,
abstract = {Automated verification has become an essential part
in the security evaluation of cryptographic
protocols. Recently, there has been a considerable
effort to lift the theory and tool support that
existed for reachability properties to the more
complex case of equivalence properties. In this
paper we contribute both to the theory and practice
of this verification problem. We establish new
complexity results for static equivalence, trace
equivalence and labelled bisimilarity and provide a
decision procedure for these equivalences in the
case of a bounded number of sessions. Our procedure
is the first to decide trace equivalence and
labelled bisimilarity exactly for a large variety of
cryptographic primitives---those that can be
represented by a subterm convergent destructor
rewrite system. We implemented the procedure in a
new tool, \textsc{Deepsec}. We showed through
extensive experiments that it is significantly more
efficient than other similar tools, while at the
same time raises the scope of the protocols that can
be analysed.},
address = {San Francisco, CA, USA},
author = {Cheval, Vincent and Kremer, Steve and Rakotonirina,
Itsaka},
booktitle = {{P}roceedings of the 39th IEEE Symposium on Security
and Privacy (S\&P'18)},
month = may,
pages = {525--542},
publisher = {{IEEE} Computer Society Press},
title = {DEEPSEC: Deciding Equivalence Properties in Security
Protocols - Theory and Practice},
year = 2018,
doi = {10.1109/SP.2018.00033},
acronym = {{S\&P}'18},
nmonth = 5,
={https://csdl.computer.org/csdl/proceedings/sp/2018/4353/00/435301a525.pdf},
={https://hal.inria.fr/hal-01698177/file/main.pdf},
note =
{\textbf{\href{https://www.ieee-security.org/TC/SP2018/awards.html}{Distinguished
paper award}}},
}