@COMMENT This file was generated by bib2html.pl version 0.94
@COMMENT written by Patrick Riley
@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},
}