diff --git a/Security_Properties/README.md b/Security_Properties/README.md
index 062e75d68ebb0a0cccbfaa36c70994d70909118c..2acae5d5ebe9ea0316ed274b3bd2b347b2c92b42 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**.