Process Calculus for Modeling and Quantifying Location Privacy

In the mobile wireless Internet, location privacy is serious concerns. As a response to these concerns, many (formal) location-privacy protection mechanisms (LPPMs) and evaluation metrics for LPPMs have been proposed. It is necessary to integrate formal models into assessments, because this integration can deduce the gap between them: after designing a LPPM, we adopt this integration to formalize and measure it. In this paper, we propose a probabilistic process calculus to model the obfuscation-based schemes (OBS, one LPPM ) and use the relative entropy to measure the degree of location privacy OBS can leak. We integrate the two approaches into one unified model. Examples demonstrate the accuracy of our model. Our work decreases the gap between the formalization and the measurement for OBS.