README.md

# Security Properties model files

These files have been developed and verified with Tamarin version 1.6.0. 

They can be verified with the following Tamarin command:

`tamarin-prover <filename> --heuristic=<I|S> --prove --quit-on-warning`

Hereby, `<filename>` has to be replaced with the name of the file that shall be verified (see the comment at the beginning of the files). Optionally, the number of Thread used by Tamarin can be specified by appending ` +RTS -N<number of threads> -RTS`, which can improve verification times.

Depending on `<filename>`, the heuristic should be set to `I` or `S` to optimize verification times. For `daa_pnc_credential_installation.spthy` use `--heuristic=S`.
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**.