A procedure for deciding symbolic equivalence between sets of constraint systems

Vincent Cheval, Hubert Comon-Lundh, and Stéphanie Delaune. A procedure for deciding symbolic equivalence between sets of constraint systems. Information and Computation, 255(1):94 – 125, August 2017.
doi:10.1016/j.ic.2017.05.004

Download

[PDF] [HTML] 

Abstract

We consider security properties of cryptographic protocols that can be modelled using trace equivalence, a crucial notion when specifying privacy-type properties, like anonymity, vote-privacy, and unlinkability. Infinite sets of possible traces are symbolically represented using deducibility constraints. We describe an algorithm that decides trace equivalence for protocols that use standard primitives and that can be represented using such constraints. More precisely, we consider symbolic equivalence between sets of constraint systems, and we also consider disequations. Considering sets and disequations is actually crucial to decide trace equivalence for processes that may involve else branches and/or private channels (for a bounded number of sessions). Our algorithm for deciding symbolic equivalence between sets of constraint systems is implemented and performs well in practice. Unfortunately, it does not scale up well for deciding trace equivalence between processes. This is however the first implemented algorithm deciding trace equivalence on such a large class of processes.

BibTeX

@Article{SD-jlamp16,
  abstract =	 {We consider security properties of cryptographic
                  protocols that can be modelled using trace
                  equivalence, a crucial notion when specifying
                  privacy-type properties, like anonymity,
                  vote-privacy, and unlinkability. Infinite sets of
                  possible traces are symbolically represented using
                  deducibility constraints. We describe an algorithm
                  that decides trace equivalence for protocols that
                  use standard primitives and that can be represented
                  using such constraints. More precisely, we consider
                  symbolic equivalence between sets of constraint
                  systems, and we also consider
                  disequations. Considering sets and disequations is
                  actually crucial to decide trace equivalence for
                  processes that may involve else branches and/or
                  private channels (for a bounded number of
                  sessions). Our algorithm for deciding symbolic
                  equivalence between sets of constraint systems is
                  implemented and performs well in
                  practice. Unfortunately, it does not scale up well
                  for deciding trace equivalence between
                  processes. This is however the first implemented
                  algorithm deciding trace equivalence on such a large
                  class of processes.},
  author =	 {Cheval, Vincent and Comon-Lundh, Hubert and Delaune,
                  St{\'e}phanie},
  title =	 {A procedure for deciding symbolic equivalence
                  between sets of constraint systems},
  journal =	 {Information and Computation},
  year =	 2017,
  month =	 aug,
  pages =	 {94 - 125},
  doi =		 {10.1016/j.ic.2017.05.004},
  volume =	 255,
  number =	 1,
                  ={http://people.irisa.fr/Stephanie.Delaune/PUBLICATIONS/CCD-ic16.pdf},
}