Skip to content
Snippets Groups Projects
Normal view Permalink
README.md 1.09 KiB
Newer Older
  • Learn to ignore specific revisions
    • Timm Lauser's avatar
    Added additional execution instructions to subfolders
    Timm Lauser committed
    1 2 3 4 5 6 
    # 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:
    Dustin Kern's avatar
    details for test machine  
    Dustin Kern committed
    7 
    `tamarin-prover <filename> --heuristic=<I|S> --prove --quit-on-warning`
    Timm Lauser's avatar
    Added additional execution instructions to subfolders
    Timm Lauser committed
    8 9 10 
    
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.
    Dustin Kern's avatar
    details for test machine  
    Dustin Kern committed
    11 12 13 14 
    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.
    Timm Lauser's avatar
    Added additional execution instructions to subfolders
    Timm Lauser committed
    15 
    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).