International Association
for Cryptologic Research

The Swiss Post voting system is one of the most advanced cryptographic voting protocols deployed for political elections, offering end-to-end verifiability and vote privacy. It provides significant documentation and independent scrutiny reports. Still, we argue that two significant pillars of trust need to be further developed. One is formal verification accompanied by machine-checked proofs. The second is security in presence of a corrupt setup component. In this work, we propose formal specifications of a simplified version of the Swiss Post voting protocol and initial verification results with the Tamarin prover. We also propose a revised protocol design that mitigates risks from a corrupt setup, and a prototype implementation of necessary zero-knowledge proofs.