Secure Communication with Humans
Establishing a secure communication channel between two parties is a nontrivial problem, especially when one or both are humans. Unlike computers, humans are error-prone and cannot perform strong cryptographic operations without supporting technology. However, the technology humans rely on may itself be compromised.
This project aims to formally model and analyze systems in which humans, computers, and supporting devices interact, taking human limitations into account.
- Modeling Human Errors in Security Protocols by David Basin, Sasa Radomirovic, and Lara Schmid presented at CSF 2016. Full version (PDF, 349 KB) of the paper. Tamarin specification files (ZIP, 59 KB) for all protocols appearing in the paper.
- A Complete Characterization of Secure Human-Server Communication by David Basin, Sasa Radomirovic, and Michael Schläpfer presented at CSF 2015. Full version (PDF, 420 KB) of the paper. Tamarin specification files (ZIP, 71 KB) for all protocols appearing in the full version of the paper.
- Guided Specification and Analysis of a Loyalty Card System by Laurent Cuennet, Marc Pouly, and Sasa Radomirovic presented at GramSEC 2015. Paper (PDF, 255 KB) and Tamarin specification files (ZIP, 26 KB) for two loyalty points protocols.
- Michael Schläpfer, Secure end-to-end communication in remote internet voting, 2016. [PDF]
Master and Bachelor Theses
- Andrina Denzler, Automatic Analysis of Communication Protocols with Human Errors, 2016. [PDF (PDF, 1.9 MB)] Tamarin Specification Files (ZIP, 70 KB), Source Code (ZIP, 7 KB).
- Lara Schmid, Human Errors in Secure Communication Protocols, 2015. [PDF (PDF, 918 KB)], Tamarin Specification Files (ZIP, 247 KB).
Precompiled binaries of Tamarin for Linux, Windows, and Mac OS X and sources are available. Read the compilation and installation instructions. More information about the Tamarin prover is given on the Tamarin prover site.