These files have been developed and verified with Tamarin version 1.6.0.
...
...
@@ -10,9 +10,9 @@ Hereby, `<filename>` has to be replaced with the name of the file that shall be
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).
| PR5 - 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) |
| _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) |