Timing attacks in security protocols: symbolic framework and proof techniques

Vincent Cheval 1 Véronique Cortier 1
1 CASSIS - Combination of approaches to the security of infinite states systems
FEMTO-ST - Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies (UMR 6174), Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
Abstract : We propose a framework for timing attacks, based on (a variant of) the applied-pi calculus. Since many privacy properties, as well as strong secrecy and game-based security properties, are stated as process equivalences, we focus on (time) trace equivalence. We show that actually, considering timing attacks does not add any complexity: time trace equivalence can be reduced to length trace equivalence, where the attacker no longer has access to execution times but can still compare the length of messages. We therefore deduce from a previous decidability result for length equivalence that time trace equivalence is decidable for bounded processes and the standard cryptographic primitives. As an application, we study several protocols that aim for privacy. In particular, we (automatically) detect an existing timing attack against the biometric passport and new timing attacks against the Private Authentication protocol.
Type de document :
Communication dans un congrès
4th Conference on Principles of Security and Trust (POST 2015), Apr 2015, Londres, United Kingdom. 2015
Liste complète des métadonnées

https://hal.inria.fr/hal-01103618
Contributeur : Véronique Cortier <>
Soumis le : jeudi 15 janvier 2015 - 10:24:21
Dernière modification le : vendredi 6 juillet 2018 - 15:06:10

Identifiants

  • HAL Id : hal-01103618, version 1

Citation

Vincent Cheval, Véronique Cortier. Timing attacks in security protocols: symbolic framework and proof techniques. 4th Conference on Principles of Security and Trust (POST 2015), Apr 2015, Londres, United Kingdom. 2015. 〈hal-01103618〉

Partager

Métriques

Consultations de la notice

259