Teaching Materials for the Tamarin Prover

This repository contains teaching materials related to the Tamarin Prover. These materials complement the official Tamarin manual.

General support

Understanding dependency graphs (handout)

The following PDF can be used as a reference handout for understanding dependency graphs.

• Handout: dependency graphs

(Update coming with more explanation of specific adversary nodes)

Tutorials

The core Tamarin team and other contributors have developed different tutorials over time. Below you can find three tutorials.

1. One-day tutorial

(Originally given at EuroSnP/Eurocrypt 2017)

• Morning slides PDF (Libreoffice source file)

• Afternoon slides PDF (Libreoffice source file)

• Tamarin model files (ZIP archive version)

• Handouts to print:

  • Exercises
  • Naxos protocol description
  • Dependency graphs

Authors: David Basin, Cas Cremers, Jannik Dreier, and Ralf Sasse.

2. Toy protocol exercise

• Tamarin toy protocol exercise.

Author: Benjamin Kiesl

3. Tamarin workshop

• Tamarin workshop (2-4 hours).

Author: Felix Linker

License

All the materials in the tamarin-prover/teaching repository are provided under a Creative Commons Attribution license (CC-BY).