# 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 |
|:-----------------------------------------------------------|:-------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------|:-|
| _PR<sub>2</sub>_ - Unlinkable Credential Installation      | [daa_pnc_anonymity_credential_installation.spthy](daa_pnc_anonymity_credential_installation.spthy) <br> [daa_pnc_unlinkability_credential_installation.spthy](daa_pnc_unlinkability_credential_installation.spthy) | [ObsEquOracle_credential_installation.py](ObsEquOracle_credential_installation.py) |
| _PR<sub>3</sub>_ - Unlinkable Charge Autorization          | [daa_pnc_anonymity_charge_authorisation.spthy](daa_pnc_anonymity_charge_authorisation.spthy) <br> [daa_pnc_unlinkability_charge_authorisation.spthy](daa_pnc_unlinkability_charge_authorisation.spthy)             | [ObsEquOracle_charge_authorisation.py](ObsEquOracle_charge_authorisation.py) |
| _PR<sub>4</sub>_ - Unlinkable CDRs                         | [daa_pnc_anonymity_cdrs.spthy](daa_pnc_anonymity_cdrs.spthy) <br> [daa_pnc_unlinkability_cdrs.spthy](daa_pnc_unlinkability_cdrs.spthy)                                                                             | [ObsEquOracle_cdrs.py](ObsEquOracle_cdrs.py) |
| _PR<sub>5</sub>_ - Unlinkability of EV Users and Locations | [daa_pnc_anonymity_ev_users_locations.spthy](daa_pnc_anonymity_ev_users_locations.spthy) <br> [daa_pnc_unlinkability_ev_users_locations.spthy](daa_pnc_unlinkability_ev_users_locations.spthy)                     | [ObsEquOracle_ev_users_locations.py](ObsEquOracle_ev_users_locations.py) |