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

要約

電子投票システムの設計と実装は困難な作業です。
ここでは正式な分析が非常に役立ちます。
特に、投票システムがどのように機能するか、およびシステムのどの要件が関連するかについての理解を深めることができます。
この論文では、最先端のモデル チェッカー Uppaal が投票プロトコルのモデリングと事前検証に適した環境を提供することを提案します。
これを説明するために、Pr\^et \`a 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\^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.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google