Skip to content
Snippets Groups Projects
Select Git revision
  • master default protected
1 result
Blame Permalink
Code owners
Assign users and groups as approvers for specific file changes. Learn more.
README.md 1.09 KiB

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 commandline --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).