@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,
  publisher =	 {{IEEE} Computer Society Press},
  title =	 {DEEPSEC: Deciding Equivalence Properties in Security
                  Protocols - Theory and Practice},
  year =	 2018,
  acronym =	 {{S\&P}'18},
  note =	 {\textbf{Distinguished paper award}},
}