diff --git a/Privacy_Properties/README.md b/Privacy_Properties/README.md index 3cdc38ad458412a063272f9a4e3222fc3fa9b962..5b90aab38e7db4640309230e286ccd3a03247308 100644 --- a/Privacy_Properties/README.md +++ b/Privacy_Properties/README.md @@ -10,6 +10,8 @@ Hereby, `<filename>` has to be replaced with the name of the file that shall be 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). +By default, Tamarin prints its verification steps to the console. Note that the most important output is the **summary of summaries** at the end of execution, which should indicate that all lemmas were **verified**. + | 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) |