Lengths May Break Privacy – Or How to Check for Equivalences with Length

Cheval, Vincent and Cortier, Véronique and Plet, Antoine (2013) Lengths May Break Privacy – Or How to Check for Equivalences with Length. In: Shargina, Natasha and Veith, Helmut, eds. Computer Aided Verification. Lecture Notes in Computer Science, 8044. Springer-Verlag Berlin, St Petersburg, Russia pp. 708-723. ISBN 978-3-642-39798-1. E-ISBN 978-3-642-39799-8. (doi:https://doi.org/10.1007/978-3-642-39799-8_50) (Full text available)

PDF - Publisher pdf
Download (275kB) Preview
[img]
Preview
PDF (The long version of the paper) - Supplemental Material
Download (325kB) Preview
[img]
Preview
Official URL
http://dx.doi.org/10.1007/978-3-642-39799-8_50

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 (without length tests). Our procedure has been implemented and we have discovered a new flaw against privacy in the biometric passport protocol.

Item Type: Conference or workshop item (Paper)
Uncontrolled keywords: Cryptographic protocols, Formal verification, Symbolic model, Automatic, Equivalence properties, Lengh 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: Faculties > Sciences > School of Computing > Security Group
Depositing User: Vincent Cheval
Date Deposited: 23 Jan 2015 11:13 UTC
Last Modified: 23 Jan 2015 11:18 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/46726 (The current URI for this page, for reference purposes)
  • Depositors only (login required):

Downloads

Downloads per month over past year