From 41045908b9c978f71f144ec23e46f861f437908e Mon Sep 17 00:00:00 2001 From: Dustin Kern <dustin.kern@h-da.de> Date: Tue, 26 Apr 2022 19:47:08 +0000 Subject: [PATCH] Update README.md to add docker setup --- README.md | 31 +++++++++++++++++++++++++++++-- 1 file changed, 29 insertions(+), 2 deletions(-) diff --git a/README.md b/README.md index c80a606..ed68b98 100644 --- a/README.md +++ b/README.md @@ -8,9 +8,18 @@ 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. +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). +The README files in the subfolders [Security_Properties](Security_Properties/) and [Privacy_Properties](Privacy_Properties/) provide a general explanation of how to run the Tamarin proof(s). +Additionally, at the beginning of each model file, the specific 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 following subsections provide examples on how to setup Tamarin 1.6.0 using either Homebrew or Docker. +Please consult the [Tamarin-Prover Manual](https://tamarin-prover.github.io/manual/tex/tamarin-manual.pdf) for more details on installation and usage instructions. + +### Tamarin Setup using Homebrew + 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): @@ -37,7 +46,25 @@ 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. + +### Tamarin Setup using Docker + +Alternatively, the provided Dockerfile (based on the file found [here](https://github.com/rsasse/tamarin-prover-docker/blob/0d1b7fa10943fbae731772ad15f6a919f61a7dcf/Dockerfile)) can be used to setup Tamarin 1.6.0 and run the proofs as follows (tested on Ubuntu 20.04.1 LTS; assumes that [Docker](https://docs.docker.com/) is already installed): + +``` +# Clone the git and build the docker image +git clone https://code.fbi.h-da.de/seacop/daa-pnc-tamarin.git +cd daa-pnc-tamarin +sudo docker build -t tamarin . + +# Afterwards the proofs can be run via the docker image by replacing 'tamarin-prover' with 'docker run --rm -v $PWD:/workspace tamarin' +# in the respective commands that are described in the subfolders Security_Properties and Privacy_Properties, e.g.: +cd Security_Properties +time sudo docker run --rm -v $PWD:/workspace tamarin daa_pnc_credential_installation.spthy \ + --heuristic=S --quit-on-warning --prove +RTS -N8 -RTS +``` + + ## Security and Privacy Properties -- GitLab