README.md

Privacy Properties model files

These files have been developed and verified with Tamarin version 1.6.0.

They can be verified with the following Tamarin command:

tamarin-prover <filename> --quit-on-warning --diff --heuristic=O --oraclename=<oracle name> --prove

Hereby, <filename> has to be replaced with the name of the file that shall be verified and <oracle name> with the name of the corresponding oracle (see the comment at the beginning of the files as well as the table below). Optionally, the number of Thread used by Tamarin can be specified by appending +RTS -N<number of threads> -RTS, which can improve verification times.

As python oracles are used during verification, it is important that they are located in the same folder as the command is run (and possess the correct file permissions to be executable).

By default, Tamarin prints its verification steps to the console. Note that the most important output is the summary of summaries at the end of execution, which should indicate that all lemmas were verified.

Privacy Property	Tamarin File(s)	Oracle
PR2 - Unlinkable Credential Installation	daa_pnc_anonymity_credential_installation.spthy daa_pnc_unlinkability_credential_installation.spthy	ObsEquOracle_credential_installation.py
PR3 - Unlinkable Charge Autorization	daa_pnc_anonymity_charge_authorisation.spthy daa_pnc_unlinkability_charge_authorisation.spthy	ObsEquOracle_charge_authorisation.py
PR4 - Unlinkable CDRs	daa_pnc_anonymity_cdrs.spthy daa_pnc_unlinkability_cdrs.spthy	ObsEquOracle_cdrs.py
PR5 - Unlinkability of EV Users and Locations	daa_pnc_anonymity_ev_users_locations.spthy daa_pnc_unlinkability_ev_users_locations.spthy	ObsEquOracle_ev_users_locations.py