A Method for Verifying Privacy-Type Properties: The Unbounded Case

Lucca Hirschi, David Baelde, and Stéphanie Delaune. A Method for Verifying Privacy-Type Properties: The Unbounded Case. In Proceedings of the 37th IEEE Symposium on Security and Privacy (S&P'16), IEEE Computer Society Press, San Jose, CA, USA, May 2016.

Download

[PDF] 

Abstract

In this paper, we consider the problem of verifying anonymity and unlinkability in the symbolic model, where protocols are represented as processes in a variant of the applied pi calculus notably used in the ProVerif tool. Existing tools and techniques do not allow one to verify directly these properties, expressed as behavioral equivalences. We propose a different approach: we design two conditions on protocols which are sufficient to ensure anonymity and unlinkability, and which can then be effectively checked automatically using ProVerif. Our two conditions correspond to two broad classes of attacks on unlinkability, corresponding to data and control-flow leaks.
This theoretical result is general enough to apply to a wide class of protocols. In particular, we apply our techniques to provide the first formal security proof of the BAC protocol (e-passport). Our work has also lead to the discovery of new attacks, including one on the LAK protocol (RFID authentication) which was previously claimed to be unlinkable (in a weak sense) and one on the PACE protocol (e-passport).

BibTeX

@inproceedings{HBD-sp16,
  abstract =	 {In this paper, we consider the problem of verifying
                  anonymity and unlinkability in the symbolic model,
                  where protocols are represented as processes in a
                  variant of the applied pi calculus notably used in
                  the ProVerif tool. Existing tools and techniques do
                  not allow one to verify directly these properties,
                  expressed as behavioral equivalences. We propose a
                  different approach: we design two conditions on
                  protocols which are sufficient to ensure anonymity
                  and unlinkability, and which can then be effectively
                  checked automatically using ProVerif. Our two
                  conditions correspond to two broad classes of
                  attacks on unlinkability, corresponding to data and
                  control-flow leaks.\par This theoretical result is
                  general enough to apply to a wide class of
                  protocols. In particular, we apply our techniques to
                  provide the first formal security proof of the BAC
                  protocol (e-passport). Our work has also lead to the
                  discovery of new attacks, including one on the LAK
                  protocol (RFID authentication) which was previously
                  claimed to be unlinkable (in a weak sense) and one
                  on the PACE protocol (e-passport).},
  address =	 {San Jose, CA, USA},
  author =	 {Hirschi, Lucca and Baelde, David and Delaune,
                  St\'ephanie},
  booktitle =	 {{P}roceedings of the 37th IEEE Symposium on Security
                  and Privacy (S\&P'16)},
  month =	 may,
  publisher =	 {{IEEE} Computer Society Press},
  title =	 {A Method for Verifying Privacy-Type Properties: The
                  Unbounded Case},
  year =	 2016,
  acronym =	 {{S\&P}'16},
  nmonth =	 5,
  url =		 {http://projects.lsv.ens-cachan.fr/ukano/f/HBD16.pdf},
                  ={http://projects.lsv.ens-cachan.fr/ukano/f/HBD16.pdf},
}