diff --git a/README.md b/README.md index 841b945367ccdcdec936b243c07d83591f76f3b8..8679bf666007c44c3c7d9cb61f4c78d26b747566 100644 --- a/README.md +++ b/README.md @@ -17,17 +17,17 @@ The Tamarin prover (https://tamarin-prover.github.io/) is required to verify the In the following, we list which property of our extension is addressed by which Tamarin model. **Security_Properties** -| Security Property | Tamarin File(s) | -|:----------------------------------------|:-----------------------------------| -| $SR_2$ - Secure Credential Installation | daa_pnc_credential_installation.spthy | -| $SR_3$ - Secure Charge Autorization | daa_pnc_charge_authorisation_online.spthy <br> daa_pnc_charge_authorisation_offline.spthy | -| $SR_4$ - Charge Data Authenticity | daa_pnc_charge_authorisation_online.spthy <br> daa_pnc_charge_authorisation_offline.spthy | +| Security Property | Tamarin File(s) | +|:-------------------------------------|:--------------------------------------| +| SR2 - Secure Credential Installation | daa_pnc_credential_installation.spthy | +| SR3 - Secure Charge Autorization | daa_pnc_charge_authorisation_online.spthy <br> daa_pnc_charge_authorisation_offline.spthy | +| SR4 - Charge Data Authenticity | daa_pnc_charge_authorisation_online.spthy <br> daa_pnc_charge_authorisation_offline.spthy | **Privacy_Properties** The files with the keyword *anonymity* in their file name contain a model for a weaker version of the properties. -| Privacy Property | Tamarin File(s) | Oracle | -|:-------------------------------------------------|:---------------------------------------------------------------------------------------------------------|:-| -| $PR_2$ - Unlinkable Credential Installation | daa_pnc_anonymity_credential_installation.spthy <br> daa_pnc_unlinkability_credential_installation.spthy | oracle_credential_installation.py | -| $PR_3$ - Unlinkable Charge Autorization | daa_pnc_anonymity_charge_authorisation.spthy <br> daa_pnc_unlinkability_charge_authorisation.spthy | oracle_charge_authorisation.py | -| $PR_4$ - Unlinkable CDRs | daa_pnc_anonymity_cdrs.spthy <br> daa_pnc_unlinkability_cdrs.spthy | oracle_cdrs.py | -| $PR_5$ - Unlinkability of EV Users and Locations | daa_pnc_anonymity_ev_users_locations.spthy <br> daa_pnc_unlinkability_ev_users_locations.spthy | oracle_ev_users_locations.py | +| Privacy Property | Tamarin File(s) | Oracle | +|:----------------------------------------------|:---------------------------------------------------------------------------------------------------------|:-| +| PR2 - Unlinkable Credential Installation | daa_pnc_anonymity_credential_installation.spthy <br> daa_pnc_unlinkability_credential_installation.spthy | oracle_credential_installation.py | +| PR3 - Unlinkable Charge Autorization | daa_pnc_anonymity_charge_authorisation.spthy <br> daa_pnc_unlinkability_charge_authorisation.spthy | oracle_charge_authorisation.py | +| PR4 - Unlinkable CDRs | daa_pnc_anonymity_cdrs.spthy <br> daa_pnc_unlinkability_cdrs.spthy | oracle_cdrs.py | +| PR5 - Unlinkability of EV Users and Locations | daa_pnc_anonymity_ev_users_locations.spthy <br> daa_pnc_unlinkability_ev_users_locations.spthy | oracle_ev_users_locations.py |