[Resource Topic] 2025/1901: Towards formal verification and corrupted setup security for the SwissPost voting system

Welcome to the resource topic for 2025/1901

Title:
Towards formal verification and corrupted setup security for the SwissPost voting system

Authors: Sevdenur Baloglu, Sergiu Bursuc, Reynaldo Gil-Pons, Sjouke Mauw

Abstract:

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.

ePrint: https://eprint.iacr.org/2025/1901

See all topics related to this paper.

Feel free to post resources that are related to this paper below.

Example resources include: implementations, explanation materials, talks, slides, links to previous discussions on other websites.

For more information, see the rules for Resource Topics .