论文标题
模型检查器很酷：如何在Uppaal中模型检查投票协议
Model Checkers Are Cool: How to Model Check Voting Protocols in Uppaal
论文作者
论文摘要
电子投票系统的设计和实施是一项艰巨的任务。正式分析在这里可能有很大的帮助。特别是，它可以更好地了解投票系统的工作原理以及系统上的要求。在本文中，我们建议最先进的模型检查器Uppaal为对投票协议进行建模和初步验证提供了一个良好的环境。为了说明这一点，我们提出了Prêt -à选民的Uppaal模型，以及一些自然的扩展。尽管模型检查器中财产规范语言严重限制，但我们还展示了如何验证收据变体的变体。
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êt à 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.
