From 6ca52fd666157ae2a7c8315c2e4d7eebd97f5541 Mon Sep 17 00:00:00 2001 From: Timm Lauser <timm.lauser@h-da.de> Date: Fri, 18 Feb 2022 15:55:15 +0100 Subject: [PATCH] Added hyperlinks to the filenames of model files in README --- README.md | 21 ++++++++++----------- 1 file changed, 10 insertions(+), 11 deletions(-) diff --git a/README.md b/README.md index f36169b..89cfbb0 100644 --- a/README.md +++ b/README.md @@ -19,19 +19,18 @@ In the following, we list which property of our extension is addressed by which **Security_Properties** | Security Property | Tamarin File(s) | |:--------------------------------------------------|:-------------------------| -| _SR<sub>2</sub>_ - Secure Credential Installation | daa_pnc_credential_installation.spthy | -| _SR<sub>3</sub>_ - Secure Charge Autorization | daa_pnc_charge_authorisation_online.spthy <br> daa_pnc_charge_authorisation_offline.spthy | -| _SR<sub>4</sub>_ - Charge Data Authenticity | daa_pnc_charge_authorisation_online.spthy <br> daa_pnc_charge_authorisation_offline.spthy | +| _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>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** The files with the keyword *anonymity* in their filename contain a model for a weaker version of the properties. - -| Privacy Property | Tamarin File(s) | Oracle | -|:-----------------------------------------------------------|:---------------------------------------------------------------------------------------------------------|:-| -| _PR<sub>2</sub>_ - Unlinkable Credential Installation | daa_pnc_anonymity_credential_installation.spthy <br> daa_pnc_unlinkability_credential_installation.spthy | oracle_credential_installation.py | -| _PR<sub>3</sub>_ - Unlinkable Charge Autorization | daa_pnc_anonymity_charge_authorisation.spthy <br> daa_pnc_unlinkability_charge_authorisation.spthy | oracle_charge_authorisation.py | -| _PR<sub>4</sub>_ - Unlinkable CDRs | daa_pnc_anonymity_cdrs.spthy <br> daa_pnc_unlinkability_cdrs.spthy | oracle_cdrs.py | -| _PR<sub>5</sub>_ - 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 | +|:-----------------------------------------------------------|:---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------|:-| +| _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>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) | ## Original Tamarin DAA model @@ -39,7 +38,7 @@ Our models are based on the models from the following paper: Stephan Wesemeyer, Christopher J.P. Newton, Helen Treharne, Liqun Chen, Ralf Sasse, and Jorden Whitefield. 2020. Formal Analysis and Implementation of a TPM 2.0-based Direct Anonymous Attestation Scheme. In Proceedings of the 15th ACM Asia Conference on Computer and Communications Security (ASIA CCS '20). Association for Computing Machinery, New York, NY, USA, 784–798. DOI:https://doi.org/10.1145/3320269.3372197 -Their Tamarin models can be found at https://github.com/tamarin-prover/tamarin-prover/tree/dddaccbe981343dde1a321ce0c908585d4525918/examples/asiaccs20-eccDAA. +Their Tamarin models can be found at https://github.com/tamarin-prover/tamarin-prover/tree/dddaccbe981343dde1a321ce0c908585d4525918/examples/asiaccs20-eccDAA. The changes/extension to their model can be summarized as follows: (i) Adaptions/additions to the model rules in order to represent the e-mobility-specific roles/processes within the context (e.g., the introduction of the CPS role between the host and issuer in the credential provisioning process or the validation of charge authorization via the EMSP in addition to the DAA-Signature verification by the CP/Verifier), (ii) changes to model rules in order to represent the changes to the base DAA Join and Certify processes; e.g., the possibility of no live interaction with the credential issuer during installation due to the use of credential pools or the binding of session keys to the ISO 15118 session), (iii) definition of new lemmas in order to verify correctness as well as the identified security/privacy requirements, and (iv) performance optimizations such that the new models terminate within a reasonable time frame via the adaption of oracles (to work with the new/changed rules) and the addition of source/reuse lemmas. Our changes roughly amount to 54 new rules, 16 changed rules, 32 new lemmas, 18 changed lemmas, and 5 adapted oracles. -- GitLab