Strategy Logics for the Verification of Security Protocols

在当今的网络世界中，安全和投票协议的验证是一个日益重要的主题。总部位于英国的开放权利组织辩称，缺乏测试、审计程序不充分，以及对电子投票的系统或程序设计重视不足，都会使“选举容易出错和舞弊”。因此，越来越多的人采用电子投票系统，需要对这些系统进行认证，以防止可能的恶意行为，包括串通和来自第三方的胁迫。为此，形式方法可以提供数学上精确的技术和工具来认证投票协议。事实上，形式化方法已经显示了它们的价值，例如，在发现了几种攻击，包括对Needham-Schroeder协议的中间人攻击，这是最广泛使用的公钥认证协议之一，17年来一直没有被注意到。在这个项目中，我们的目标是开发基于可表达的基于逻辑的规范语言的(电子)投票协议的安全属性的形式化验证技术。具体地说，该项目提案旨在通过用等式理论扩展多智能体系统的流行逻辑来表示消息的编码和解码，来捕获与安全有关的密码学方面，这些方面不容易通过符号推理来表达。我们打算将所得到的框架应用于对广泛的投票协议(例如，ThreeBallot、Selene、Foo)的抗胁迫、无接收和匿名性等性质的验证，从而为它们的正式认证奠定基础。

The verification of security and voting protocols is a subject of ever increasing importance in today's networked world. The UK-based Open Rights Group has argued that a lack of testing, inadequate audit procedures, and insufficient attention given to system or process design with electronic voting leaves "elections open to error and fraud". Hence, the growing adoption of electronic voting systems requires these systems to be certified against possible malicious behaviours, including collusion and coercion from third parties.To this end, formal methods can provide mathematically precise techniques and tools for the certification of voting protocols. Indeed, formal methods have already shown their value, for instance, in the discoveryof several attacks, including a man-in-the-middle attack on the Needham-Schroeder protocol, one of the most widely-used public-key authentication protocols, that went unnoticed for 17 years.In this project we aim at developing techniques for the formal verification of security properties of (electronic) voting protocols based on expressive logic-based specification languages. Specifically, the project proposal aims at capturing cryptographic aspects pertaining to security, which are not readily expressible by symbolic reasoning, by extending popular logics for multi-agent systems with equational theories to represent encoding and decoding of messages. We intend to apply the resulting framework to the verification of properties such as coercion-resistance, receipt-freeness, and anonymity to a wide range of voting protocols (e.g., ThreeBallot, Selene, FOO), thus laying the foundation for their formal certification.