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.
翻译:设计和实施电子投票系统是一项艰巨的任务。 正式分析在这方面大有帮助。 特别是,正式分析可以使人们更好地了解投票系统如何运作,以及该系统有哪些相关要求。 在本文中,我们建议,最先进的模型检查员Upppaal为模拟和初步核查投票协议提供一个良好的环境。 为了说明这一点,我们提出了一个普尔吉特·卡瓦选民的Uppaal模型,以及一些自然扩展。我们还展示了如何核实一种无收据的变体,尽管模型检查员的财产规格语言严重限制。