Ceremony Analysis Meets Verifiable Voting: Individual Verifiability in Helios

摘要

The Helios verifiable voting system offers voters an opportunity to verify the integrity of their individual vote, that it is cast, and included in the final count, as intended. While not all voters have to verify, these steps can be cumbersome for those who aim to carry them out. Therefore, new verification processes have been proposed in order to improve usability. Voters can use a web-based verifier provided by any one of several independent verification institutes, or a smartphone app developed and provided by these institutes. In this work, we describe these verification processes as ceremonies, and thus model the human peer's interaction. We undertake a security analysis applying an adaptive threat model suited to analysing human-device and human-human channels. More realistic threats on these channels are identified, compared to those from an analysis using a Dolev-Yao attacker.