Formal Verification with the Tamarin Prover

The Tamarin prover is a security protocol verification tool that supports both falsification and unbounded verification in the symbolic model. Security protocols are specified as multiset rewriting systems and analysed with respect to (temporal) first-order properties and a message theory that models Diffie-Hellman exponentiation combined with a user-defined subterm-convergent rewriting theory.

Using recently developed techniques that involve fine-grained adversary models and a flexible property specification language, we aim to investigate existing security protocols from a new angle. Topics of interest include attack finding, tool development, and formal modeling. Recent examples include an analysis of the TLS v1.3 standard, and tool improvements.

Desirable Prerequisites for Student Projects

Previous exposure to protocol analysis, e.g. the Information Security course, is extremely helpful. Some experience with the Tamarin Prover, e.g. from the Information Security exercises and for master students the Formal Methods for Information Security course or the Information Security Lab, is helpful, but not required. Depending whether the project is extending Tamarin, modeling new protocols or developing new analysis methods, knowledge of applied cryptography, networking protocols or Haskell may be useful. Note: Whilst Tamarin is written in Haskell, no Haskell knowledge is required to use Tamarin or develop its theory.

Previous Theses

Master's

Lara Schmid's master thesis[PDF]: on how one can model human errors in secure communication protocols.
Mauro Zenoni's master thesis[PDF]: SCION's Hidden Paths Design Formal Security Analysis[zip].
Angela Rellstab's master thesis[PDF]: Formalizing and Verifying Generations of AKA Protocols[zip].
Sandra Dünki's master thesis[PDF]: Modelling and Analysis of Web Applications in Tamarin[zip].
Guillaume Girol's master thesis[PDF]: Formalizing and Verifying the Security Protocols from the Noise Framework[zip].

Bachelor's

Staub's bachelor thesisexternal page [PDF]: about the implementation of the original version of Tamarin's GUI.
Andrina Denzler's bachelor thesis[PDF]: on how to automate the analysis of communications protocols with human errors.
Dorela Kozmai's bachelor thesis[PDF]: on how to translate Tamarin specifications into Alice&Bob protocol notation, with implementation available[zip].
Michel Keller's bachelor thesis[PDF]: about translating Alice&Bob protocol notation into Tamarin's input language, with implementation available[tar.gz].
Xenia Hofmeier's bachelor thesis[PDF]: Formal Analysis of Web Single-Sign On Protocols using Tamarin[zip].
Andris Suter-Dörig's bachelor thesis[PDF]: Formalizing and Verifying the Security Protocols from the Noise Framework[zip].
David Lanzenberger's bachelor thesis[PDF]: 5G protocols analysis and model for Tamarin[zip].
Vincent Stettler's bachelor thesis[PDF]: TLS1.3,v13 analysis and model for Tamarin[zip].

Further Information

Please contact Ralf Sasse, Xenia Hofmeier, Felix Linker, or see the group's project page.