电子投票协议中的自然战略能力与安全评估

# 电子投票协议中的自然战略能力与安全评估 ## 1. 背景引入 在安全分析领域，以往常常过于关注系统的技术层面，默认用户会遵循协议设计者规定的步骤。然而在现实中，人类参与者往往不会如此。那些使用困难且成本高的安全机制，即便旨在保护用户免受攻击，也常被用户忽视。 以电子投票协议为例，通常期望满足收据自由性（即选民不应获得可用于破坏其投票匿名性的证书）和抗胁迫性（选民应能欺骗潜在胁迫者，按照自己的意愿投票）。近年来，在开发既抗胁迫又能让选民验证选举结果的投票系统方面取得了显著进展，如 Prêt à Voter 协议及其实现 vVote，该协议曾用于 2014 年澳大利亚维多利亚州的选举。 但投票系统具备选民可验证机制并不意味着它就更安全可靠。这关键取决于有多少选民会实际验证他们的选票，而这又取决于该机制的易懂性和易用性。对于抗胁迫性和收据自由性机制，以及任何可选的安全机制都是如此。如果用户觉得机制复杂繁琐且可避免使用，他们就会选择不使用。 因此，关键问题往往不是某个机制是否能提供安全保障，而是能提供多大程度的安全保障。本文提出了一种基于用户战略行为复杂性的分级安全概念，即安全属性 ϕ 的满足程度可以通过以下两点来定义： - 选民为使 ϕ 成立所需执行的策略的复杂性； - 用户在实现过程中必须投入的资源。 获取 ϕ 越简单、成本越低，安全程度就越高。 ## 2. 研究方法 ### 2.1 建模投票过程 第一步是将协议描述划分为松散耦合的组件，即代理。在电子投票场景中，通常包括选民、选举基础设施、计票员等。 对于每个代理，定义其局部模型，包括位置（代理的局部状态）和位置之间的带标签边（局部转换）。转换对应代理执行的操作。例如，选民扫描选票后处于“扫描中”状态，可执行“输入投票”操作，从而进入“已投票”状态。 使用 Uppaal 模型检查器为分布式和多智能体系统创建这些局部模型，其具有灵活的建模语言和直观的图形用户界面。全局模型由代理的局部模型组成，每个全局状态代表代理局部状态的一种可能配置。 ### 2.2 自然战略能力 多智能体系统的许多相关属性涉及代理及其群体的战略能力。例如，选民可验证性可理解为选民检查其投票是否正确登记和计票的能力；收据自由性可理解为胁迫者（通常在选民协助下）无法获取选民投票证据的能力。 战略推理逻辑，如 ATL 和战略逻辑，为表达代理行为及其动态提供了简洁的语言。例如，ATL 公式 ⟨⟨cust⟩⟩F ticket 表示客户 cust 无论其他代理采取何种行动，最终都能获得票证。如果 cust 有一个策略，其每个执行路径在未来某个时刻都满足 ticket，则该规范成立。 在多智能体系统中，策略被理解为条件计划。正式地，策略被定义为从系统状态序列（即游戏的可能历史）到行动的函数。本文使用更简单的位置策略概念，即从状态到行动的函数。但现实生活中的过程可能有大量可能状态，这会导致策略非常复杂，而人类在处理组合复杂对象方面能力较差。 为更好地模拟人类代理的战略制定方式，本文提出使用基于条件 - 行动规则列表的更人性化的策略表示方法。条件对于位置策略由布尔公式给出，在一般情况下由布尔公式的正则表达式给出。此外，只考虑复杂度不超过给定界限的策略，这与常识推理和规划的经典方法以及人类学习和使用概念的实证结果一致。 ### 2.3 自然策略及其复杂性 自然策略：设 B(Propa) 是代理 a 可观察到的原子命题 Propa 上的布尔公式集合。在电子投票场景