POR for Security Protocol Equivalences: Beyond Action-Determinism - INRIA - Institut National de Recherche en Informatique et en Automatique Accéder directement au contenu
Chapitre D'ouvrage Année : 2018

POR for Security Protocol Equivalences: Beyond Action-Determinism

Résumé

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.
Fichier principal
Vignette du fichier
BDH_ESORICS18.pdf (407.83 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-02390219 , version 1 (21-09-2020)

Identifiants

Citer

David Baelde, Stéphanie Delaune, Lucca Hirschi. POR for Security Protocol Equivalences: Beyond Action-Determinism. ESORICS, pp.385-405, 2018, ⟨10.1007/978-3-319-99073-6_19⟩. ⟨hal-02390219⟩
241 Consultations
62 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More