From db8404daa57a5876f41aa230684a4cb810c6b57d Mon Sep 17 00:00:00 2001 From: Dustin Kern <dustin.kern@h-da.de> Date: Sat, 23 Apr 2022 14:45:39 +0000 Subject: [PATCH] Update README.md based on feedback --- Privacy_Properties/README.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/Privacy_Properties/README.md b/Privacy_Properties/README.md index 3cdc38a..5b90aab 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) | -- GitLab