Abstract
There is an increasing number of cyber-systems (e.g., payment, transportation, voting, critical-infrastructure systems) whose security depends intrinsically on human users. A security ceremony expands a security protocol with everything that is considered out-of-band to it, including, in particular, the mistakes that human users might make when participating actively in the security ceremony. In this paper, we introduce a novel approach for the formal analysis of security ceremonies. Our approach defines mutation rules that model possible behaviors of a human user, and automatically generates mutations in the behavior of the other agents of the ceremony to match the human-induced mutations. This allows for the analysis of the original ceremony specification and its possible mutations, which may include the way in which the ceremony has actually been implemented. To automate our approach, we have developed the tool X-Men, which is a prototype that extends Tamarin, one of the most common tools for the automatic unbounded verification of security protocols. As a proof of concept, we have applied our approach to two real-life case studies, uncovering a number of concrete vulnerabilities.
| Original language | English |
|---|---|
| Title of host publication | Proceedings of the 5th IEEE European Symposium on Security and Privacy, EuroS&P 2020 |
| Publisher | IEEE Computer Science Press |
| Number of pages | 18 |
| Publication status | Accepted/In press - 24 Mar 2020 |