diff --git a/Privacy_Properties/privacy_properties.md b/Privacy_Properties/privacy_properties.md
new file mode 100644
index 0000000000000000000000000000000000000000..9cd94574fb8c365777bd32e0fc30c2d7ae34fc9c
--- /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 0000000000000000000000000000000000000000..58a5d43e20e38266590fab7a4cd68cdb30a0d317
--- /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