Model Checkers Are Cool: How to Model Check Voting Protocols in Uppaal
Cryptography and Security
2023-10-19 v3 Artificial Intelligence
Logic in Computer Science
Multiagent Systems
Abstract
The design and implementation of an e-voting system is a challenging task. Formal analysis can be of great help here. In particular, it can lead to a better understanding of how the voting system works, and what requirements on the system are relevant. In this paper, we propose that the state-of-art model checker Uppaal provides a good environment for modelling and preliminary verification of voting protocols. To illustrate this, we present an Uppaal model of Pr\^et \`a Voter, together with some natural extensions. We also show how to verify a variant of receipt-freeness, despite the severe limitations of the property specification language in the model checker.
Keywords
Cite
@article{arxiv.2007.12412,
title = {Model Checkers Are Cool: How to Model Check Voting Protocols in Uppaal},
author = {Wojciech Jamroga and Yan Kim and Damian Kurpiewski and Peter Y. A. Ryan},
journal= {arXiv preprint arXiv:2007.12412},
year = {2023}
}