Sogenannte Mechanismen zum Präservieren von Standortdatenschutz (LPPM) benutzen unterschiedliche mathematische Ansätze, um in der Kommunikation mit Standortbezogenen Diensten persönliche Daten der Nutzer zu beschützen. Diese LPPM versprechen verschiedene Datenschutz-Garantien, die nicht per se vergleichbar sind. Wir schlagen den σ-Calculus vor, der ein Prozesskalkül zum Modellieren von LPPM und deren Datenschutzeigenschaften ist. Des Weiteren präsentieren wir das Model-Checking-Tool LP3Verif, das, basierend auf dem σ-Calculus, Standortdatenschutzeigenschaften von LPPM automatisch verifizieren kann.

Location privacy-preserving mechanisms (LPPM) use different computational approaches to protect personal data in queries to location-based services. These LPPMs give different privacy claims that are not per se comparable. We propose the σ-calculus, a process calculus to model LPPMs and their privacy guarantees. Furthermore, we present LP3Verif, which is a model checking tool to verify location privacy properties of LPPMs using the σ-calculus.