This folder contains the files corresponding to the case studies presented in this manuscript.
The subfolder chap3 contains the Tamarin files for the case studies presented in Chapter 3 and some additional material corresponding to:
- encodings of unlinkability using diff-equivalence for the Basic Hash protocol;
- experiments with GSVerif on a simplified version of the LAK protocol;
- experiments with Tamarin and the XOR operator.
The subfolder chap4 contains the Squirrel files for the case studies presented in Chapter 4.
The results presented in this manuscript were obtained with the following versions of tools:
- Tamarin, develop version (commit 23c9eef) [https://github.com/tamarin-prover/tamarin-prover/tree/23c9eefb9fc41216ac08f922935d0baa9bd47b9b]
- ProVerif 2.00 [https://prosecco.gforge.inria.fr/personal/bblanche/proverif/]
- GSVerif [https://sites.google.com/site/globalstatesverif]
- Squirrel, master version (commit cd0dd44) [https://github.com/squirrel-prover/squirrel-prover/tree/cd0dd445d0e5d739f059730d9f54b7d2c21dc694]