Model Checker for Location Privacy Properties in Location-Based Services
LP3Verif is an open-source model checking tool for verification of location privacy properties of location privacy-preserving mechanisms (LPPM).
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 sigma-calculus, a process calculus to model LPPMs and their privacy guarantees.
LP3Verif is a model checking tool to verify location privacy properties of LPPMs using the sigma-calculus. LP3Verif is written in Java and can be executed from the command line to verify LPPM protocols specified in .lp3 syntax as described in the manual.
Source code and binaries at Github:
Here you can find the most common protocols modeled in LP3 syntax: