Strategy Logics for the Verification of Security Protocols

在当今的网络世界中，安全和投票协议的验证是一个日益重要的主题。总部设在英国的开放权利组织认为，缺乏测试、审计程序不足以及对电子投票的系统或流程设计关注不够，使“选举容易出错和欺诈”。因此，越来越多的电子投票系统的采用，需要这些系统进行认证，以防止可能的恶意行为，包括共谋和胁迫来自第三方。为此，形式化方法可以提供数学上精确的技术和工具，用于认证的投票协议。事实上，形式化方法已经显示出了它们的价值，例如，在发现几种攻击中，包括对Needham-Schroeder协议的中间人攻击，Needham-Schroeder协议是最广泛使用的公钥认证协议之一，在这个项目中，我们的目标是开发用于正式验证安全属性的技术，基于表达性逻辑规范语言的（电子）投票协议。具体而言，该项目的建议旨在捕捉有关安全的密码方面，这是不容易表达的符号推理，通过扩展流行的逻辑与方程理论的多代理系统代表编码和解码的消息。我们打算将由此产生的框架应用于验证各种投票协议的属性，如抗干扰性，无收据性和匿名性（例如，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.