Location privacy-preserving mechanisms (LPPM) were introduced to protect users of location-based services (LBS) from the privacy threat of leaked personal data. These mechanisms alter the communication to the LBS in such a way that no malicious party can derive sensitive personal data. In the literature one can find many different LPPMs with varying privacy guarantees but so far no formal framework exists for comparing all of these mechanisms and their privacy guarantees. We propose the σ-calculus, which enables the modeling of LPPMs and location privacy guarantees. The calculus entails a process language, a property language, and a temporal-K-less-epistemic modal logic that enables the verification of location privacy properties on process models. The σ-calculus is a novel process calculus that is based on standard set operations that are computationally cheap, yet sufficient for modeling privacy violations in LBS communication. The calculus is the first formal framework to model and reason about a wide array of LPPMs. Furthermore, we present model checking algorithms that enable the automatic verification of location privacy properties. We evaluate the expressiveness of our process language by modeling a significant number of LPPMs from the literature and the expressiveness of our property language by describing a benchmark set of location privacy properties. Furthermore, we demonstrate the verification of a privacy property with an extended example of an LPPM algorithm designer. We developed the tool LP3Verif that implements our model checking algorithms. The open-source tool is written in Java and uses the SMT solver CVC4 as back end.
