From 6e06f51da85e44ffc75af3fd29dd1ef40ded9117 Mon Sep 17 00:00:00 2001
From: Dustin Kern <dustin.kern@h-da.de>
Date: Sat, 23 Apr 2022 14:43:36 +0000
Subject: [PATCH] Update README.md based on feedback

---
 Security_Properties/README.md | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/Security_Properties/README.md b/Security_Properties/README.md
index 062e75d..2acae5d 100644
--- a/Security_Properties/README.md
+++ b/Security_Properties/README.md
@@ -13,3 +13,5 @@ For both `daa_pnc_charge_authorisation_*.spthy` models use `--heuristic=I`.
 Some lemmas use an oracle heuristic (via `[heuristic=o]` at the lemma definition), which overwrites the command line `--heuristic=<I|S>` argument in Tamarin version 1.6.0.
 
 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).
+
+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**.
-- 
GitLab