Secure Communication with Humans
Members
Introduction
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.
Publications
- Modeling Human Errors in Security Protocols by David Basin, Sasa Radomirovic, and Lara Schmid presented at CSF 2016. DownloadFull version (PDF, 349 KB)vertical_align_bottom of the paper. DownloadTamarin specification files (ZIP, 59 KB)vertical_align_bottom 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. DownloadFull version (PDF, 420 KB)vertical_align_bottom of the paper. DownloadTamarin specification files (ZIP, 71 KB)vertical_align_bottom 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. DownloadPaper (PDF, 255 KB)vertical_align_bottom and DownloadTamarin specification files (ZIP, 26 KB)vertical_align_bottom for two loyalty points protocols.
PhD Theses
- 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. [DownloadPDF (PDF, 1.9 MB)vertical_align_bottom] DownloadTamarin Specification Files (ZIP, 70 KB)vertical_align_bottom, DownloadSource Code (ZIP, 7 KB)vertical_align_bottom.
- Lara Schmid, Human Errors in Secure Communication Protocols, 2015. [DownloadPDF (PDF, 918 KB)vertical_align_bottom], DownloadTamarin Specification Files (ZIP, 247 KB)vertical_align_bottom.
Software
external pagePrecompiled binaries of Tamarincall_made for Linux, Windows, and Mac OS X and external pagesourcescall_made are available. Read the external pagecompilation and installation instructionscall_made. More information about the Tamarin prover is given on the Tamarin prover site.