模型检测器很酷：如何在 Uppaal 中对投票协议进行模型检测
Model Checkers Are Cool: How to Model Check Voting Protocols in Uppaal
AI总结：
本文提出使用模型检测器 Uppaal 对投票协议进行建模与初步验证，通过构建 Prêt à Voter 模型及其扩展，展示了在属性规范语言受限下验证收据无关性变体的方法。
摘要：
电子投票系统的设计与实现是一项具有挑战性的任务。形式化分析在此能提供极大帮助。特别是，它能让人更好地理解投票系统的工作原理，以及系统上哪些需求是相关的。在本文中，我们提出最先进的模型检测器 Uppaal 为投票协议的建模和初步验证提供了良好环境。为了说明这一点，我们给出了 Prêt à Voter 的 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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
