LP3Verif
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
Tested versions
OS / CVC / LP3 Version | Java jdk.java.net | Java Version Oracle.com/java | Java Version Oracle.com/java |
---|---|---|---|
Ubuntu 20.0.4 / cvc4-1.8-x86_64-linux-opt / V1.1 | 16.0.1 O.K. | 11.0.11 O.K. | 16.0.1 O.K. |
Window 10 / cvc4-1.8-win64-opt.exe / V1.1 | 16.0.1 O.K. | 11.0.11 O.K. | 16.0.1 O.K. |
Mac OS 11 Cvc4 / V1.1 | 16.0.1 O.K. | 11.0.11 O.K. | 16.0.1 O.K. |
Prereq
- Get one of the supported java packages (see matrix). You need the jdk Version, the jre does not work.
- 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).
- 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. - 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 /.
Run
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
Protocols
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
Crypto
- Ghinita et al.
- Trust no one
- MaPIR
- SpaceTwist