David Baelde, Stéphanie Delaune, and Lucca Hirschi. A reduced semantics for deciding trace equivalence using constraint systems. In Proceedings of the 3rd International Conference on Principles of Security and Trust (POST'14), pp. 1–21, Lecture Notes in Computer Science 8414, Springer, Grenoble, France, April 2014.
Many privacy-type properties of security protocols can be modelled using trace equivalence properties in suitable process algebras. It has been shown that such properties can be decided for interesting classes of finite processes (i.e., without replication) by means of symbolic execution and constraint solving. However, this does not suffice to obtain practical tools. Current prototypes suffer from a classical combinatorial explosion problem caused by the exploration of many interleavings in the behaviour of processes. Modersheim et al. have tackled this problem for reachability properties using partial order reduction techniques. We revisit their work, generalize it and adapt it for equivalence checking. We obtain an optimization in the form of a reduced symbolic semantics that eliminates redundant interleavings on the fly.
@inproceedings{BDH-post14,
abstract = {Many privacy-type properties of security protocols
can be modelled using trace equivalence properties in
suitable process algebras. It has been shown that
such properties can be decided for interesting
classes of finite processes (i.e.,~without
replication) by means of symbolic execution and
constraint solving. However, this does not suffice to
obtain practical tools. Current prototypes suffer
from a classical combinatorial explosion problem
caused by the exploration of many interleavings in
the behaviour of processes. Modersheim et~al. have
tackled this problem for reachability properties
using partial order reduction techniques. We revisit
their work, generalize it and adapt it for
equivalence checking. We obtain an optimization in
the form of a reduced symbolic semantics that
eliminates redundant interleavings on the fly.},
address = {Grenoble, France},
author = {Baelde, David and Delaune, St{\'e}phanie and
Hirschi, Lucca},
booktitle = {{P}roceedings of the 3rd {I}nternational {C}onference
on {P}rinciples of {S}ecurity and {T}rust
({POST}'14)},
OPTDOI = {10.1007/978-3-642-54792-8_1},
editor = {Abadi, Mart{\'\i}n and Kremer, Steve},
month = apr,
pages = {1-21},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
title = {A~reduced semantics for deciding trace equivalence
using constraint systems},
volume = {8414},
year = {2014},
acronym = {{POST}'14},
nmonth = {4},
lsv-category = {intc},
wwwpublic = {public and ccsb},
}