Timing attacks in security protocols: symbolic framework and proof techniques

Timing attacks in security protocols: symbolic framework and proof techniques. Vincent Cheval and Véronique Cortier. In Proceedings of the 4th Conference on Principles of Security and Trust (POST'15), pp. 280–299, Lecture Notes in Computer Science 9036, Springer, London, UK, April 2015.

Download

[PDF] [HTML]

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.

BibTeX

@inproceedings{post15-time-equiv,
  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.
\par
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.},
  address =     {London, UK},
  author =     {Cheval, Vincent and Cortier, V\'eronique},
  booktitle =     {{P}roceedings of the 4th {C}onference on
                  {P}rinciples of {S}ecurity and {T}rust (POST'15)},
  month =     apr,
  publisher =     {Springer},
  series =     {Lecture Notes in Computer Science},
  title =     {Timing attacks in security protocols: symbolic framework and proof techniques},
  year =     2015,
  acronym =     {{POST}'15},
  volume = {9036},
  pages = {280--299},
  DOI = {10.1007/978-3-662-46666-7_15},
                  {https://members.loria.fr/VCortier/files/Papers/POST2015-equiv-time.pdf},
}