Lengths may break privacy -- or how to check for equivalences with length

Vincent Cheval 1 Véronique Cortier 2 Antoine Plet 3
2 CASSIS - Combination of approaches to the security of infinite states systems
FEMTO-ST - Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies, Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
Abstract : Security protocols have been successfully analyzed using symbolic models, where messages are represented by terms and protocols by processes. Privacy properties like anonymity or untraceability are typically expressed as equivalence between processes. While some decision procedures have been proposed for automatically deciding process equivalence, all existing approaches abstract away the information an attacker may get when observing the length of messages. In this paper, we study process equivalence with length tests. We first show that, in the static case, almost all existing decidability results (for static equivalence) can be extended to cope with length tests. In the active case, we prove decidability of trace equivalence with length tests, for a bounded number of sessions and for standard primitives. Our result relies on a previous decidability result from Cheval et al [15] (without length tests). Our procedure has been implemented and we have discovered a new flaw against privacy in the biometric passport protocol.
Type de document :
Communication dans un congrès
Natasha Sharygina and Helmut Veith. CAV'13 - 25th International Conference on Computer Aided Verification - 2013, Jul 2013, Saint Petersbourg, Russia. Springer, 8044, pp.708-723, 2013, Lecture Notes in Computer Science. 〈10.1007/978-3-642-39799-8_50〉
Liste complète des métadonnées

https://hal.inria.fr/hal-00881065
Contributeur : Véronique Cortier <>
Soumis le : jeudi 7 novembre 2013 - 14:09:15
Dernière modification le : jeudi 15 février 2018 - 08:48:14

Lien texte intégral

Identifiants

Citation

Vincent Cheval, Véronique Cortier, Antoine Plet. Lengths may break privacy -- or how to check for equivalences with length. Natasha Sharygina and Helmut Veith. CAV'13 - 25th International Conference on Computer Aided Verification - 2013, Jul 2013, Saint Petersbourg, Russia. Springer, 8044, pp.708-723, 2013, Lecture Notes in Computer Science. 〈10.1007/978-3-642-39799-8_50〉. 〈hal-00881065〉

Partager

Métriques

Consultations de la notice

334