Schupp, SibylleSibylleSchupp1137288833Bavendiek, KaiKaiBavendiek2022-03-252022-03-252022Technische Universität Hamburg (2022)http://hdl.handle.net/11420/12100Sogenannte 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.enhttps://creativecommons.org/licenses/by/4.0/Process calculusModal logicModel Checkinglocation based servicelocation privacyIngenieurwissenschaftenDoctoral Thesis10.15480/882.425810.15480/882.4258Federrath, HannesHannesFederrathPhD Thesis