Paper 2025/1901
Towards formal verification and corrupted setup security for the SwissPost voting system
, University of Luxembourg, University of Luxembourg, University of Luxembourg, University of LuxembourgAbstract
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.
- Keywords
- security modelselectronic votingformal verificationcorrupt setup
- Contact author(s)
-
sevdenurbaloglu @ gmail com
sbursuc @ gmail com
gilcu3 @ gmail com
sjouke mauw @ uni lu - History
- 2026-05-21: revised
- 2025-10-11: received
- See all versions
- Short URL
- https://ia.cr/2025/1901
- License
-
CC BY
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}
}
