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}}},
}