diff --git a/Privacy_Properties/README.md b/Privacy_Properties/README.md index 5b90aab38e7db4640309230e286ccd3a03247308..fcbec84ef7fcd665af16ff1f1aa0b1f67f2994b3 100644 --- a/Privacy_Properties/README.md +++ b/Privacy_Properties/README.md @@ -15,6 +15,6 @@ By default, Tamarin prints its verification steps to the console. Note that the | 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>3</sub>_ - Unlinkable Charge Authorization | [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) | diff --git a/README.md b/README.md index ed68b9869aef25429b85ac5c4031fba1f8308a1b..49657f3cc17709688161b7fade55644e3270ffed 100644 --- a/README.md +++ b/README.md @@ -74,7 +74,7 @@ In the following, we list which property of our extension is addressed by which | Security Property | Tamarin File(s) | |:--------------------------------------------------|:-------------------------| | _SR<sub>2</sub>_ - Secure Credential Installation | [daa_pnc_credential_installation.spthy](Security_Properties/daa_pnc_credential_installation.spthy) | -| _SR<sub>3</sub>_ - Secure Charge Autorization | [daa_pnc_charge_authorisation_online.spthy](Security_Properties/daa_pnc_charge_authorisation_online.spthy) <br> [daa_pnc_charge_authorisation_offline.spthy](Security_Properties/daa_pnc_charge_authorisation_offline.spthy) | +| _SR<sub>3</sub>_ - Secure Charge Authorization | [daa_pnc_charge_authorisation_online.spthy](Security_Properties/daa_pnc_charge_authorisation_online.spthy) <br> [daa_pnc_charge_authorisation_offline.spthy](Security_Properties/daa_pnc_charge_authorisation_offline.spthy) | | _SR<sub>4</sub>_ - Charge Data Authenticity | [daa_pnc_charge_authorisation_online.spthy](Security_Properties/daa_pnc_charge_authorisation_online.spthy) <br> [daa_pnc_charge_authorisation_offline.spthy](Security_Properties/daa_pnc_charge_authorisation_online.spthy) | **Privacy_Properties** @@ -82,7 +82,7 @@ The files with the keyword *anonymity* in their filename contain a model for a w | Privacy Property | Tamarin File(s) | Oracle | |:-----------------------------------------------------------|:---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------|:-| | _PR<sub>2</sub>_ - Unlinkable Credential Installation | [daa_pnc_anonymity_credential_installation.spthy](Privacy_Properties/daa_pnc_anonymity_credential_installation.spthy) <br> [daa_pnc_unlinkability_credential_installation.spthy](Privacy_Properties/daa_pnc_unlinkability_credential_installation.spthy) | [ObsEquOracle_credential_installation.py](Privacy_Properties/ObsEquOracle_credential_installation.py) | -| _PR<sub>3</sub>_ - Unlinkable Charge Autorization | [daa_pnc_anonymity_charge_authorisation.spthy](Privacy_Properties/daa_pnc_anonymity_charge_authorisation.spthy) <br> [daa_pnc_unlinkability_charge_authorisation.spthy](Privacy_Properties/daa_pnc_unlinkability_charge_authorisation.spthy) | [ObsEquOracle_charge_authorisation.py](Privacy_Properties/ObsEquOracle_charge_authorisation.py) | +| _PR<sub>3</sub>_ - Unlinkable Charge Authorization | [daa_pnc_anonymity_charge_authorisation.spthy](Privacy_Properties/daa_pnc_anonymity_charge_authorisation.spthy) <br> [daa_pnc_unlinkability_charge_authorisation.spthy](Privacy_Properties/daa_pnc_unlinkability_charge_authorisation.spthy) | [ObsEquOracle_charge_authorisation.py](Privacy_Properties/ObsEquOracle_charge_authorisation.py) | | _PR<sub>4</sub>_ - Unlinkable CDRs | [daa_pnc_anonymity_cdrs.spthy](Privacy_Properties/daa_pnc_anonymity_cdrs.spthy) <br> [daa_pnc_unlinkability_cdrs.spthy](Privacy_Properties/daa_pnc_unlinkability_cdrs.spthy) | [ObsEquOracle_cdrs.py](Privacy_Properties/ObsEquOracle_cdrs.py) | | _PR<sub>5</sub>_ - Unlinkability of EV Users and Locations | [daa_pnc_anonymity_ev_users_locations.spthy](Privacy_Properties/daa_pnc_anonymity_ev_users_locations.spthy) <br> [daa_pnc_unlinkability_ev_users_locations.spthy](Privacy_Properties/daa_pnc_unlinkability_ev_users_locations.spthy) | [ObsEquOracle_ev_users_locations.py](Privacy_Properties/ObsEquOracle_ev_users_locations.py) |