David Baelde, Stéphanie Delaune, and Lucca Hirschi. A reduced semantics for deciding trace equivalence. Logical Methods in Computer Science, 13(2), 2017.
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. Mödersheim 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 optimisation in the form of a reduced symbolic semanticsthat eliminates redundant interleavings on the fly. The obtainedpartial order reduction technique hasbeen integrated in a tool called Apte.We conducted complete benchmarks showingdramatic improvements.
@article{BDH-lmcs17,
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.
M\"odersheim 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 optimisation in the form of a reduced symbolic semantics
that eliminates redundant interleavings on the fly. The obtained
partial order reduction technique has
been integrated in a tool called Apte.
We conducted complete benchmarks showing
dramatic improvements.},
author = {Baelde, David and Delaune, St{\'e}phanie and
Hirschi, Lucca},
OPTDOI = {10.2168/LMCS-10(2:11)2014},
journal = {Logical Methods in Computer Science},
OPTmonth = jun,
title = {A reduced semantics for deciding trace equivalence},
volume = {13},
number = {2},
year = {2017},
OPTnmonth = {6},
lsv-category = {jour},
wwwpublic = {public and ccsb},
}