From c8fed01a72b5b6d7bc18cfa4c61ad4cfb924ab46 Mon Sep 17 00:00:00 2001 From: Timm Lauser <timm.lauser@h-da.de> Date: Fri, 18 Feb 2022 16:08:40 +0100 Subject: [PATCH] Added additional execution instructions to subfolders --- Privacy_Properties/privacy_properties.md | 18 ++++++++++++++++++ Security_Properties/security_properties.md | 11 +++++++++++ 2 files changed, 29 insertions(+) create mode 100644 Privacy_Properties/privacy_properties.md create mode 100644 Security_Properties/security_properties.md diff --git a/Privacy_Properties/privacy_properties.md b/Privacy_Properties/privacy_properties.md new file mode 100644 index 0000000..9cd9457 --- /dev/null +++ b/Privacy_Properties/privacy_properties.md @@ -0,0 +1,18 @@ +# Security 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). + +| Privacy Property | Tamarin File(s) | Oracle | +|:----------------------------------------------|:-------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------|:-| +| PR2 - 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) | +| PR3 - 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) | +| PR4 - 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) | +| 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) | diff --git a/Security_Properties/security_properties.md b/Security_Properties/security_properties.md new file mode 100644 index 0000000..58a5d43 --- /dev/null +++ b/Security_Properties/security_properties.md @@ -0,0 +1,11 @@ +# Security 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> --heuristic=I --prove --quit-on-warning` + +Hereby, `<filename>` has to be replaced with the name of the file that shall be verified (see the comment at the beginning of the files). 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 the python oracle is used during verification, it is important that it is located in the same folder as the command is run (and that the oracle file is executable). \ No newline at end of file -- GitLab