Paper 2025/1901 Original: eprint.iacr.org/2025/1901 ↗
Towards formal verification and corrupted setup security for the SwissPost voting system
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.
Metadata
- Available format(s)
PDF- Category
- Cryptographic protocols
- Publication info
- Preprint.
- History
- 2026-05-21: last updated
- 2025-10-11: published
- Short URL
- https://ia.cr/2025/1901
- License
- https://creativecommons.org/licenses/by/4.0/
BibTeX
@misc{cryptoeprint:2025/1901,
author = {Sevdenur Baloglu and Sergiu Bursuc and Reynaldo Gil-Pons and Sjouke Mauw},
title = {Towards formal verification and corrupted setup security for the SwissPost voting system},
howpublished = {Cryptology {ePrint} Archive, Paper 2025/1901},
year = {2025},
url = {https://eprint.iacr.org/2025/1901}
}