biblio.bib

@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 =	 {Accepted for publication},
}


@inproceedings{CKR-cav18,
  abstract =	 {In this paper we describe the DeepSec prover, a tool
                  for security-protocol analysis deciding equivalence
                  properties, modelled as trace equivalence of two
                  processes in a dialect of the applied pi calculus.},
  address =	 {Oxford, UK},
  author =	 {Cheval, Vincent and Kremer, Steve and Rakotonirina,
                  Itsaka},
  booktitle =	 {{P}roceedings of the 30th {I}nternational {C}onference
                  on {C}omputer {A}ided {V}erification, {P}art {II} ({CAV}'18)},
  doi =		 {10.1007/978-3-319-96142-2_4},
  month =	 jul,
  publisher =	 {Springer},
  title =	 {The DEEPSEC prover},
  year =	 2018,
  acronym =	 {CAV'18},
  url =		 {https://hal.inria.fr/hal-01763138/document},
}


@InProceedings{CKR-ccs19,
  abstract =	 {Verification of privacy-type properties for
                  cryptographic protocols in an active adversarial
                  environment, modelled as a behavioural equivalence
                  in concurrent-process calculi, exhibits a high
                  computational complexity. While undecidable in
                  general, for some classes of common cryptographic
                  primitives the problem is coNEXP-complete when the
                  number of honest participants is bounded. \par In
                  this paper we develop optimisation techniques for
                  verifying equivalences, exploiting symmetries
                  between the two processes under study.  We
                  demonstrate that they provide a significant (several
                  orders of magnitude) speed-up in practice, thus
                  increasing the size of the protocols that can be
                  analysed fully automatically. },
  address =	 {London, UK},
  author =	 {Cheval, Vincent and Kremer, Steve and Rakotonirina,
                  Itsaka},
  booktitle =	 {{P}roceedings of the 26th {ACM} {C}onference on {C}omputer
                  and {C}ommunications {S}ecurity ({CCS}'19)},
  month =	 nov,
  pages =        {905--922},
  publisher =	 {ACM},
  title =	 {Exploiting Symmetries When Proving Equivalence
                  Properties for Security Protocols},
  year =	 2019,
  acronym =	 {{CCS}'19},
  nmonth =	 11,
  doi =		 {10.1145/3319535.3354260},
}

@article{AF-tcs04,
  author    = {Martín Abadi and
               Cédric Fournet},
  title     = {Private authentication},
  journal   = {Theor. Comput. Sci.},
  volume    = {322},
  number    = {3},
  pages     = {427--476},
  year      = {2004},
}

@article{ABF-jacm18,
  author    = {Martín Abadi and Bruno Blanchet and Cédric Fournet},
  title     = {The Applied Pi Calculus: Mobile Values, New Names, and Secure Communication},
  journal   = {J. {ACM}},
  volume    = {65},
  number    = {1},
  pages     = {1:1--1:41},
  year      = {2018},
  url       = {https://doi.org/10.1145/3127586},
  doi       = {10.1145/3127586},
}

@inproceedings{BDH-concur15,
  author =       {Baelde, David and Delaune, St{\'e}phanie and
Hirschi, Lucca},
  booktitle =    {{P}roc.\ 26th {I}nternational {C}onference on {C}oncurrency
{T}heory ({CONCUR}'15)},
  DOI =          {10.4230/LIPIcs.CONCUR.2015.497},
  month =        sep,
  pages =        {497-510},
  publisher =    {Leibniz-Zentrum f{\"u}r Informatik},
  series =       {Leibniz International Proceedings in Informatics},
  title =        {Partial Order Reduction for Security Protocols},
  volume =       42,
  year =         2015,
}

@Article{BCK-jcs20,
  author = 	 {Babel, Kushal and Cheval, Vincent and Kremer, Steve},
  title = 	 {On the semantics of communications when verifying
    equivalence properties},
  journal = 	 {Journal of Computer Security},
  volume =       {28},
  number =       {1},
  pages =        {71-127},
  year =	 2020,
  doi =		 {10.3233/JCS-191366},
  url =		 {https://hal.inria.fr/hal-02446910/document},
}