E-voting and secure human-server communication
Tomas Zgraggen · Repository for Publications and Research Data (ETH Zurich) · 2014
Security-relevant protocols often concern the communication between a human user and a server.Models of these protocols are generally imprecise; for instance, they do not include the human as an agent in the model.Some of these issues can be addressed by using the HISP model, which attempts to offer a more realistic underlying system of human-server communication.The HISP model is currently missing important features such as strong authentication properties.In this master's thesis, we improve the HISP model by extending it with additional channel properties such as replay-free channels for the interaction between humans and devices, as well as security properties such as injective agreement.We characterize the HISP topologies using these new properties, and apply our modifications and our insights to model and verify a draft proposal for a Swiss E-voting protocol.We discuss a flaw found in this protocol and suggest a possible fix.