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.
CITATION STYLE
Dahl, M., Delaune, S., & Steel, G. (2015). Formal analysis of privacy for anonymous location based services. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6993, pp. 98–112). Springer Verlag. https://doi.org/10.1007/978-3-642-27375-9_6
Mendeley helps you to discover research relevant for your work.