Selected publications at LSV

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.

@inproceedings{BDH-esorics18,
   address = {Barcelona, Spain},
   author = {David Baelde and St{\'e}phanie Delaune and Lucca Hirschi},
   booktitle = {{P}roceedings of the 23rd {E}uropean {S}ymposium on {R}esearch in {C}omputer {S}ecurity ({ESORICS}'18)},
   DOI = {10.1007/978-3-319-99073-6\_19},
   editor = {Javier L{\'{o}}pez and Jianying Zhou and Miguel Soriano},
   month = sep,
   pages = {385-405},
   publisher = {Springer},
   series = {Lecture Notes in Computer Science},
   title = {{POR} for Security Protocol Equivalences - Beyond Action-Determinism},
   url = {https://arxiv.org/abs/1804.03650},
   volume = {11098},
   year = {2018},
}

About LSV

Select by Year