A procedure for deciding symbolic equivalence between sets of constraint systems

Abstract : We consider security properties of cryptographic protocols that can be modelled using trace equivalence, a crucial notion when specifying privacy-type properties, like anonymity, vote-privacy, and unlinkability. Infinite sets of possible traces are symbolically represented using deducibility constraints. We describe an algorithm that decides trace equivalence for protocols that use standard primitives and that can be represented using such constraints. More precisely, we consider symbolic equivalence between sets of constraint systems, and we also consider disequations. Considering sets and disequations is actually crucial to decide trace equivalence for processes that may involve else branches and/or private channels (for a bounded number of sessions). Our algorithm for deciding symbolic equivalence between sets of constraint systems is implemented and performs well in practice. Unfortunately, it does not scale up well for deciding trace equivalence between processes. This is however the first implemented algorithm deciding trace equivalence on such a large class of processes.
Type de document :
Article dans une revue
Information and Computation, Elsevier, 2017, 255, pp.94 - 125. 〈10.1016/j.ic.2017.05.004〉
Liste complète des métadonnées

Littérature citée [32 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01584242
Contributeur : Vincent Cheval <>
Soumis le : jeudi 5 octobre 2017 - 11:56:04
Dernière modification le : jeudi 11 janvier 2018 - 06:27:43

Fichier

CCD-ic17.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Citation

Vincent Cheval, Hubert Comon-Lundh, Stéphanie Delaune. A procedure for deciding symbolic equivalence between sets of constraint systems. Information and Computation, Elsevier, 2017, 255, pp.94 - 125. 〈10.1016/j.ic.2017.05.004〉. 〈hal-01584242〉

Partager

Métriques

Consultations de la notice

318

Téléchargements de fichiers

34