David Baelde, Stéphanie Delaune, and Lucca Hirschi. POR for Security Protocol Equivalences -- Beyond Action-Determinism. In Proceedings of the 23rd European Symposium on Research in Computer Security (ESORICS'18), Lecture Notes in Computer Science, Springer, Barcelona, Spain, 2018.
Formal methods have proved effective to automatically analyse protocols. Recently, much research has focused on verifying trace equivalence on protocols, which is notably used to model interesting privacy properties such as anonymity or unlinkability. Several tools for checking trace equivalence rely on a naive and expensive exploration of all interleavings of concurrent actions, which calls for partial-order reduction (POR) techniques. In this paper, we present the first POR technique for protocol equivalences that does not rely on an action-determinism assumption: we recast trace equivalence as a reachability problem, to which persistent and sleep set techniques can be applied, and we show how to effectively apply these results in the context of symbolic execution. We report on a prototype implementation, improving the tool DeepSec.
@inproceedings{BDH-esorics18,
abstract = {Formal methods have proved effective to automatically analyse
protocols.
Recently, much research has focused on verifying
trace equivalence on protocols,
which is notably used to model interesting privacy
properties such as anonymity or
unlinkability. Several tools for checking trace equivalence
rely on a naive and expensive exploration of all interleavings of
concurrent actions, which calls for
partial-order reduction (POR) techniques.
In this paper, we present the first POR technique for protocol equivalences
that does not rely on an action-determinism assumption:
we recast trace equivalence as a reachability problem,
to which persistent and sleep set techniques can be applied,
and we show how to
effectively apply these results in the context of symbolic
execution.
We report on a prototype implementation,
improving the tool DeepSec.
},
address = {Barcelona, Spain},
author = {Baelde, David and Delaune, St{\'e}phanie and Hirschi, Lucca},
title = {POR for Security Protocol Equivalences -- Beyond Action-Determinism},
booktitle = {{P}roceedings of the 23rd {E}uropean {S}ymposium on {R}esearch in {C}omputer {S}ecurity (ESORICS'18)},
year = {2018},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
acronym = {{ESORICS}'18},
}