Model Checkers Are Cool: How to Model Check Voting Protocols in Uppaal

TL;DR

This paper demonstrates how Uppaal, a model checker, can be effectively used to model and verify voting protocols, including properties like receipt-freeness, aiding in understanding and improving e-voting systems.

Contribution

It introduces a method for modeling and verifying voting protocols in Uppaal, showcasing its applicability despite language limitations.

Findings

Successfully modeled Prêt à Voter in Uppaal

Verified receipt-freeness property in the model

Showed Uppaal's usefulness for e-voting protocol analysis

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.