Skip to content
Snippets Groups Projects
Normal view Permalink
README.md 1.13 KiB
Newer Older
  • Learn to ignore specific revisions
    • Timm Lauser's avatar
    Added security property files for Tamarin 1.6.1
    Timm Lauser committed
    1 2 3 4 5 6 7 8 9 
    # Security Properties model files for Tamarin 1.6.1

Our files have been developed and verified with Tamarin version 1.6.0. With [Tamarin version 1.6.1](https://github.com/tamarin-prover/tamarin-prover/releases/tag/1.6.1), the precedence of the heuristics used for proof generation has been altered, which affects the proof generation for the security property files of our model. 

Here, we provide updated files that will use the correct heuristics with Tamarin version 1.6.1. They can be run with the following command:

`tamarin-prover <filename> --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. In opposite to the files for Tamarin version 1.6.0, the default heuristic for all lemmas where we do not require a custom oracle is specified in the file itself and no longer via a command-line argument as this would now take precedence over heuristics explicitly specified with the lemmas.