Toolchains

There are multiple tools that use Tamarin as a backend.

Alice&Bob input

There exists a tool that translates Alice&Bob-specifications to Tamarin: http://www.infsec.ethz.ch/research/software/anb.html

Tamarin-Troop

If you want to export a SAPIC file to multiple provers, and find out which prover works fastest for a lemma in the file, the python script tamarin-troop can help you.

First, tamarin-troop will export your SAPIC file and lemma to the provers you choose. Currently, it supports ProVerif, Deepsec, GSVerif, and Tamarin. Then, it will run the provers concurrently, report the result and the time the first prover took to finish, and abort the calls to the other provers.

To get tamarin-troop copy etc/tamarin-troop.py into your $PATH.

How to use Tamarin-Troop

Tamarin-troop requires a python 3 installation to work. Moreover, it expects the provers to be in your path under their usual names (i.e tamarin-prover for tamarin, proverif for ProVerif etc.)

We now go over its most important command-line parameters and their semantics. Invoke

    ./tamarin-troop.py --help

for more information.

• -file path_to_your_sapic_file is the only required argument. This is the path to your SAPIC file.

• -t arg1 arg2 … tells tamarin-troop to concurrently call the Tamarin-prover on the SAPIC file. For each argument, tamarin-troop will call Tamarin with the argument. The double-dashes are added by tamarin-troop. There is no need to type them out. You can give this parameter multiple times. If you do, tamarin-troop makes multiple calls to Tamarin using the cross-product of the given arguments.

  For instance,

  ./tamarin-troop.py -file nsl-no_as-untagged.spthy -t help auto-sources

  results in the following calls to Tamarin:

  Executing 'tamarin-prover nsl-no_as-untagged.spthy --prove --help'
  Executing 'tamarin-prover nsl-no_as-untagged.spthy --prove --auto-sources'

  The call

  ./tamarin-troop.py -file nsl-no_as-untagged.spthy -t help auto-sources -t help auto-sources

  leads to the following calls:

  Executing 'tamarin-prover nsl-no_as-untagged.spthy --prove --help --help'
  Executing 'tamarin-prover nsl-no_as-untagged.spthy --prove --help --auto-sources'
  Executing 'tamarin-prover nsl-no_as-untagged.spthy --prove --auto-sources --help'
  Executing 'tamarin-prover nsl-no_as-untagged.spthy --prove --auto-sources --auto-sources'

• -p arg1 arg2 … tells tamarin-troop to concurrently call ProVerif on the translated SAPIC file. Tamarin-troop stores the translated SAPIC file in the directory it resides in. The generated file is called input_file_proverif.pv; where input_file is the original SAPIC file. The semantics are the same as -t.

• -d arg1 arg2 … tells tamarin-troop to concurrently call Deepsec on the translated SAPIC file. Again, an intermediate file is generated by tamarin-troop. The same naming convention applies. The semantics are the same as -t and -p.

• -l lemma1 lemma2 … tells tamarin-troop to export the lemmas lemma1 lemma2 …. For calls to Tamarin this is done by adding the –prove=lemmaX flag. For each lemma tamarin-troop will make one call to Tamarin. For ProVerif and Deepsec, tamarin-troop uses the –lemma=lemmaX flag to only export a single lemma to the ProVerif/Deepsec file.

  If the user gives no lemma, tamarin-troop exports ALL lemmas to ProVerif/Deepsec, and tries to prove all lemmas with Tamarin. However, tamarin-troop currently assumes that there is only one lemma/query in a file if no lemmas are given. Thus, not specifying any lemmas only makes sense if the original SAPIC file contains exactly one lemma.

• -H {s,S,c,C,i,I} … tells tamarin-troop to call Tamarin with the given heuristics. If other arguments for Tamarin are supplied via the -t parameters, the before mentioned cross-product semantics apply.

• -D Flag1 Flag2 … tells tamarin-troop to use the flags Flag1 Flag2… when calling Tamarin on the SAPIC file, and when generating the ProVerif/ Deepsec files.

• –diff tells tamarin-troop to use Tamarins –diff flag for calls to Tamarin and ProVerif/ Deepsec file generation.

• –gs tells tamarin-troop to use the GSVerif pre-processor on a ProVerif file before calling ProVerif.

• -to sets a timeout for the calls tamarin-troop starts. The default is 5 seconds.