Strategy Logics for the Verification of Security Protocols

安全协议验证的策略逻辑

• 批准号: EP/V009214/1
• 负责人: Francesco Belardinelli
• 金额: $ 1.15万
• 依托单位: Imperial College London
• 依托单位国家: 英国
• 项目类别: Research Grant
• 财政年份: 2021
• 资助国家: 英国
• 起止时间: 2021 至 无数据
• 项目状态: 已结题
• 来源: https://gtr.ukri.org/projects?ref=EP%2FV009214%2F1
• 关键词: Strategy; Logics; Verification; Security; Protocols

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.

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

项目成果

Bisimulations for verifying strategic abilities with an application to the ThreeBallot voting protocol

通过应用 ThreeBallot 投票协议来验证战略能力的双向模拟

• DOI: 10.1016/j.ic.2020.104552
• 发表时间: 2021
• 期刊: Information and Computation
• 影响因子: 1
• 作者: Belardinelli F