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:
https://github.com/Sinnloshausen/LP3Verif
 

1. Get one of the supported java packages (see matrix). You need the jdk Version, the jre does not work.
2. Download CVC4 (https://cvc4.github.io/downloads.html )and if necessary follow the installation instructions from the user manual (http://cvc4.cs.stanford.edu/wiki/User_Manual).
3. Download the packages under Releases (right pages side) from github.com/Sinnloshausen/LP3Verif
   LP3Verif.zip (compiled java)
   Source Code (zip, containes protocol examples)
   and unpack into a directory of your choice.
4. In the unzipped LP3Verif folder edit the tool.config file with the editor of your choice.
   Edit the solver path to the absolute path where your CVC4 binaries are located. If necessary edit the name of the solver, e.g., "cvc4.exe" for windows.

Under Windows you can use the unix path sign / or \\.

Then edit the smt2 path and name to a file of your choice. This file will be used by the smt solver and can contain additional
tracing/debug information for LP3Verif.

Doublecheck that you have all paths ending with a /.
 

Use one of the tested java versions to run LP3Verif with any of the
protocols files.

Depending on your operating system you can now create a shell/batch script to start the executable .jar file:

The command java -jar "LP3Verif.jar" starts LP3Verif in interactive mode where a command line prompt will ask for a path to an .lp3 file.

Calling LP3Verif with the additional argument -lp3 path/file.lp3 directly starts the verification of the specified .lp3 file.

e.g. Unix
jdk-11.0.11/bin/java -jar LP3Verif.jar -lp3 LP3Verif-1.1/Protocols/feelingbased.lp3

e.g. MacOS
jdk-11.0.11/Contents/Home/bin/java -jar LP3Verif.jar -lp3 LP3Verif-1.1/Protocols/feelingbased.lp3

e.g. Windows:
c:\users\elvis\lp3\jdk-11.0.11\bin\java -jar LP3Verif.jar -lp3 LP3Verif-1.1\Protocols\beresford.lp3
 

Here you can find the most common protocols modeled in LP3 syntax:

Mix Zones
- Beresford et al.
- Freudiger et al.
- Gong et al.
- Xinxin et al.
- MobiMix

Generalization
- Privacygrid
- CliqueCloak
- PRIVE
- Lee et al.
- ReverseCloak
- Casper
- L2P2
- Xu et al.
- feeling-based
- Location Diversity

Dummies
- Kato et al.
- Kido et al.
- SpotME
- SybilQuery
- MobiPriv

Perturbation
- Assam et al.
- Hoh et al.
- CAP

Cache
- CaDSA
- MobiCrowd

Crypto
- Ghinita et al.
- Trust no one
- MaPIR
- SpaceTwist