Symbolic verification of privacy-type properties for security protocols with XOR

Abstract : In symbolic verification of security protocols, process equivalences have recently been used extensively to model strong secrecy, anonymity and unlinkability properties. However, tool support for automated analysis of equivalence properties is limited compared to trace properties, e.g., modeling authentication and weak notions of secrecy. In this paper, we present a novel procedure for verifying equivalences on finite processes, i.e., without replication, for protocols that rely on various cryptographic primitives including exclusive or (xor). We have implemented our procedure in the tool AKISS, and successfully used it on several case studies that are outside the scope of existing tools, e.g., unlinkability on various RFID protocols, and resistance against guessing attacks on protocols that use xor.
Type de document :
Communication dans un congrès
CSF 2017 - 30th IEEE Computer Security Foundations Symposium, Aug 2017, Santa Barbara, United States. pp.15
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01533708
Contributeur : Steve Kremer <>
Soumis le : mardi 6 juin 2017 - 17:21:26
Dernière modification le : mercredi 16 mai 2018 - 11:24:10
Document(s) archivé(s) le : jeudi 7 septembre 2017 - 14:03:28

Fichier

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

Identifiants

  • HAL Id : hal-01533708, version 1

Citation

David Baelde, Stéphanie Delaune, Ivan Gazeau, Steve Kremer. Symbolic verification of privacy-type properties for security protocols with XOR. CSF 2017 - 30th IEEE Computer Security Foundations Symposium, Aug 2017, Santa Barbara, United States. pp.15. 〈hal-01533708〉

Partager

Métriques

Consultations de la notice

663

Téléchargements de fichiers

116