Update README.md based on feedback

README.md

@@ -8,9 +8,36 @@ In the following, we first provide usage instructions for our model, then we lis
 
 ## Execution Instructions
 
-The [Tamarin prover](https://tamarin-prover.github.io/) is required to verify the model. Our files have been developed and verified with [Tamarin version 1.6.0](https://github.com/tamarin-prover/tamarin-prover/releases/tag/1.6.0). At the beginning of each model file, the command to generate the corresponding Tamarin proof(s) is given, together with its expected output and the verification times on our test machine (a Lenovo ThinkPad T14 Gen 1 with an AMD® Ryzen 7 pro 4750u CPU and 16GB RAM), which can be used as an orientation. Please note that these instructions are for Tamarin 1.6.0, later versions of Tamarin might require minor modifications. For example, in Tamarin 1.6.1, the precedence of specified heuristics has been changed, affecting proof generation for the [Security_Properties](Security_Properties/) model files.
+The [Tamarin prover](https://tamarin-prover.github.io/) is required to verify the model. Our files have been developed and verified with [Tamarin version 1.6.0](https://github.com/tamarin-prover/tamarin-prover/releases/tag/1.6.0). At the beginning of each model file, the command to generate the corresponding Tamarin proof(s) is given, together with its expected output and the verification times on our test machine (a Lenovo ThinkPad T14 Gen 1 with an AMD® Ryzen 7 pro 4750u CPU and 16GB RAM), which can be used as an orientation.
+In short, the verification times for security-related models range from 14 to 20 minutes and for privacy-related models from 9 to 333 minutes.
+Please note that these instructions are for Tamarin 1.6.0, later versions of Tamarin might require minor modifications. For example, in Tamarin 1.6.1, the precedence of specified heuristics has been changed, affecting proof generation for the [Security_Properties](Security_Properties/) model files.
+The Tamarin documentation recommends to use Homebrew for the installation (cf. [Tamarin Installation](https://tamarin-prover.github.io/manual/book/002_installation.html)).
+Homebrew can, for example, be used to install Tamarin 1.6.0 as follows (tested on Ubuntu 20.04.1 LTS):
 
-Please consult the [Tamarin-Prover Manual](https://tamarin-prover.github.io/manual/tex/tamarin-manual.pdf) for installation and usage instructions. In addition, Python is required for the oracles.
+
+```
+# Install Homebrew:
+/bin/bash -c "$(curl -fsSL https://raw.githubusercontent.com/Homebrew/install/HEAD/install.sh)"
+
+# Add Homebrew to your PATH:
+echo 'eval "$(/home/linuxbrew/.linuxbrew/bin/brew shellenv)"' >> $HOME/.profile
+eval "$(/home/linuxbrew/.linuxbrew/bin/brew shellenv)"
+
+# Install Tamarin:
+wget https://github.com/tamarin-prover/tamarin-prover/releases/download/1.6.0/tamarin-prover-1.6.0.x86_64_linux.bottle.tar.gz
+export HOMEBREW_NO_INSTALLED_DEPENDENTS_CHECK=1
+brew install tamarin-prover/tap/maude graphviz haskell-stack
+brew install tamarin-prover-1.6.0.x86_64_linux.bottle.tar.gz
+sudo cp -s /home/linuxbrew/.linuxbrew/bin/maude /usr/bin/maude
+sudo cp -s /home/linuxbrew/.linuxbrew/bin/tamarin-prover /usr/bin/tamarin-prover
+
+# Check Version:
+tamarin-prover --version
+```
+
+If `brew install` exits with the `Error: Too many open files`, simply rerunning the command usually fixes it.
+In addition, Python is required for the oracles (installation, e.g., via `apt-get install python3`).
+Please consult the [Tamarin-Prover Manual](https://tamarin-prover.github.io/manual/tex/tamarin-manual.pdf) for more details on installation and usage instructions.
 
 ## Security and Privacy Properties