Skip to main content

Timing attacks: symbolic framework and proof techniques

Cheval, Vincent and Cortier, Véronique (2015) Timing attacks: symbolic framework and proof techniques. In: Focardi, Riccardo and Myers, Andrew, eds. Principles of Security and Trust 4th International Conference. Lecture Notes in Computer Science . Springer, Berlin, Germany, pp. 280-299. ISBN 978-3-662-46665-0. E-ISBN 978-3-662-46666-7. (doi:10.1007/978-3-662-46666-7_15) (KAR id:46881)

PDF Publisher pdf
Language: English
Download (268kB) Preview
[thumbnail of CC-post15.pdf]
Preview
This file may not be suitable for users of assistive technology.
Request an accessible format
PDF (The long version of the paper) Supplemental Material
Language: English
Download (549kB) Preview
[thumbnail of The long version of the paper]
Preview
This file may not be suitable for users of assistive technology.
Request an accessible format
Official URL
https://dx.doi.org/10.1007/978-3-662-46666-7_15

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.

Item Type: Book section
DOI/Identification number: 10.1007/978-3-662-46666-7_15
Additional information: To appear
Uncontrolled keywords: Cryptographic protocols, Formal verification, Symbolic model, Automatic, Timing attacks
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 75 Electronic computers. Computer science
Q Science > QA Mathematics (inc Computing science) > QA 9 Formal systems, logics
Divisions: Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
Depositing User: Vincent Cheval
Date Deposited: 23 Jan 2015 12:04 UTC
Last Modified: 16 Feb 2021 13:22 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/46881 (The current URI for this page, for reference purposes)
  • Depositors only (login required):

Downloads

Downloads per month over past year