Install Tamarin, three options:


1. Use the Docker Container Image provided at:
https://gricad-gitlab.univ-grenoble-alpes.fr/vigourth/tamarin-docker


2. Install the latest version of Tamarin from the official website:
https://tamarin-prover.github.io
Installation instructions for Linux (various distributions) and MacOS can be found in the manual: https://tamarin-prover.github.io/manual/book/002_installation.html


3. Use a VirtualBox VM at the link provided from this course website.
Username: tutorial
Password: PASSWORD


-------------------------------------------------------------------------

Then open your browser at address:  http://127.0.0.1:3001
A first example to consider is the 'tutorial example' available from this course website.

------------------------------------------------------------------------


Tamarin non-interactive mode:
   tamarin-prover YourExample.spthy
   
Tamarin interactive mode:
   tamarin-prover  interactive YourExample.spthy
           or, if you use the provided docker image:
   docker run --pull=always gricad-registry.univ-grenoble-alpes.fr/vigourth/tamarin-docker:latest YourExample.spthy

   
Tamarin interactive mode that allows to generate (when it is  possible) automatically the "sources lemma": 
   tamarin-prover  interactive  --auto-sources YourExample.spthy
          or, if you use the provided docker image:
   docker run --pull=always gricad-registry.univ-grenoble-alpes.fr/vigourth/tamarin-docker:latest --auto-sources /  



Tamarin "equivalence"  mode:
   tamarin-prover  interactive --diff YourExample.spthy
      or, if you use the provided docker image:
  docker run --pull=always gricad-registry.univ-grenoble-alpes.fr/vigourth/tamarin-docker:latest -diff /