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.

翻译：电子投票系统的设计与实现是一项具有挑战性的任务。形式化分析在此能提供很大帮助，尤其有助于更深入地理解投票系统的工作机制以及系统相关需求的界定。本文提出，最先进的模型检查器Uppaal为投票协议的建模与初步验证提供了良好的环境。为说明这一点，我们展示了Prêt à Voter的Uppaal模型及其若干自然扩展。同时，尽管模型检查器中的属性规范语言存在严重限制，我们仍展示了如何验证一种收据不可抵赖性变体。