On communication models when verifying equivalence properties (extended version)

Abstract : Symbolic models for security protocol verification, following the sem-inal ideas of Dolev and Yao, come in many flavors, even though they share the same ideas. A common assumption is that the attacker has complete control over the network: he can therefore intercept any message. Depending on the precise model this may be reflected either by the fact that any protocol output is directly routed to the adversary, or communications may be among any two participants, including the attacker — the scheduling between which exact parties the communication happens is left to the attacker. These two models may seem equivalent at first glance and, depending on the verification tools, either one or the other semantics is implemented. We show that, unsurprisingly, they indeed coincide for reachability properties. However, when we consider indistinguishability properties, we prove that these two semantics are incomparable. We also introduce a new semantics, where internal communications are allowed but messages are always eavesdropped by the attacker. We show that this new semantics yields strictly stronger equivalence relations. We also identify two subclasses of protocols for which the three semantics coincide. Finally, we implemented verification of trace equivalence for each of these semantics in the APTE tool and compare their performances on several classical examples.
Type de document :
Communication dans un congrès
6th International Conference on Principles of Security and Trust (POST), 2017, Uppsala, Sweden. 2017
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01438639
Contributeur : Steve Kremer <>
Soumis le : mardi 17 janvier 2017 - 21:07:10
Dernière modification le : samedi 21 juillet 2018 - 14:12:01
Document(s) archivé(s) le : mardi 18 avril 2017 - 15:47:11

Fichier

main.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01438639, version 1

Relations

Citation

Kushal Babel, Vincent Cheval, Steve Kremer. On communication models when verifying equivalence properties (extended version). 6th International Conference on Principles of Security and Trust (POST), 2017, Uppsala, Sweden. 2017. 〈hal-01438639〉

Partager

Métriques

Consultations de la notice

459

Téléchargements de fichiers

126