Morten Dahl, Stéphanie Delaune, and Graham Steel. Formal Analysis of Privacy for Anonymous Location Based Services. In Revised Selected Papers of the Workshop on Theory of Security and Applications (TOSCA'11), pp. 98–112, Lecture Notes in Computer Science 6993, Springer, Saarbrücken, Germany, January 2012.
We propose a framework for formal analysis of privacy in location based services such as anonymous electronic toll collection. We give a formal definition of privacy, and apply it to the VPriv scheme for vehicular services. We analyse the resulting model using the ProVerif tool, concluding that our privacy property holds only if certain conditions are met by the implementation. Our analysis includes some novel features such as the formal modelling of privacy for a protocol that relies on interactive zero-knowledge proofs of knowledge and list permutations.
@inproceedings{DDS-tosca11,
abstract = {We propose a framework for formal analysis of privacy
in location based services such as anonymous
electronic toll collection. We give a formal
definition of privacy, and apply it to the VPriv
scheme for vehicular services. We analyse the
resulting model using the ProVerif tool, concluding
that our privacy property holds only if certain
conditions are met by the implementation. Our
analysis includes some novel features such as the
formal modelling of privacy for a protocol that
relies on interactive zero-knowledge proofs of
knowledge and list permutations.},
address = {Saarbr{\"u}cken, Germany},
author = {Dahl, Morten and Delaune, St{\'e}phanie and
Steel, Graham},
booktitle = {{R}evised {S}elected {P}apers of the {W}orkshop on
{T}heory of {S}ecurity and {A}pplications
({TOSCA}'11)},
OPTDOI = {10.1007/978-3-642-27375-9_6},
editor = {M{\"o}dersheim, Sebastian A. and
Palamidessi, Catuscia},
month = jan,
pages = {98-112},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
title = {Formal Analysis of Privacy for Anonymous Location
Based Services},
volume = {6993},
year = {2012},
acronym = {{TOSCA}'11},
nmonth = {1},
conf-year = {2011},
conf-month = mar,
lsv-category = {intc},
wwwpublic = {public and ccsb},
}