Stéphanie Delaune: Automating security analysis: symbolic equivalence of constraint systems

Automating security analysis: symbolic equivalence of constraint systems

Vincent Cheval, Hubert Comon-Lundh, and Stéphanie Delaune. Automating security analysis: symbolic equivalence of constraint systems. In Proceedings of the 5th International Joint Conference on Automated Reasoning (IJCAR'10), pp. 412–426, Lecture Notes in Artificial Intelligence 6173, Springer-Verlag, Edinburgh, Scotland, UK, July 2010.

Download

[PDF]

Abstract

We consider security properties of cryptographic protocols, that are either trace properties (such as confidentiality or authenticity) or equivalence properties (such as anonymity or strong secrecy).
Infinite sets of possible traces are symbolically represented using deducibility constraints. We give a new algorithm that decides the trace equivalence for the traces that are represented using such constraints, in the case of signatures, symmetric and asymmetric encryptions. Our algorithm is implemented and performs well on typical benchmarks. This is the first implemented algorithm, deciding symbolic trace equivalence.

BibTeX

@inproceedings{CCD-ijcar10,
  abstract =      {We consider security properties of cryptographic
                   protocols, that are either trace properties (such as
                   confidentiality or authenticity) or equivalence
                   properties (such as anonymity or strong secrecy).\par
                   Infinite sets of possible traces are symbolically
                   represented using \emph{deducibility constraints}. We
                   give a new algorithm that decides the trace
                   equivalence for the traces that are represented using
                   such constraints, in the case of signatures,
                   symmetric and asymmetric encryptions. Our algorithm
                   is implemented and performs well on typical
                   benchmarks. This is the first implemented algorithm,
                   deciding symbolic trace equivalence.},
  address =       {Edinburgh, Scotland, UK},
  author =        {Cheval, Vincent and Comon{-}Lundh, Hubert and
                   Delaune, St{\'e}phanie},
  booktitle =     {{P}roceedings of the 5th {I}nternational {J}oint
                   {C}onference on {A}utomated {R}easoning ({IJCAR}'10)},
  OPTDOI =           {10.1007/978-3-642-14203-1_35},
  editor =        {Giesl, J{\"u}rgen and Haehnle, Reiner},
  month =         jul,
  pages =         {412-426},
  publisher =     {Springer-Verlag},
  series =        {Lecture Notes in Artificial Intelligence},
  title =         {Automating security analysis: symbolic equivalence of
                   constraint systems},
  volume =        {6173},
  year =          {2010},
  acronym =       {{IJCAR}'10},
  nmonth =        {7},
  lsv-category =  {intc},
  wwwpublic =     {public and ccsb},
}