数据匿名与隐私分析在电子投票协议中的形式化处理

理论计算机科学电子笔记168（2007）5-28www.elsevier.com/locate/entcsFOO投票方案中的数据匿名性S. Mauw J. Verschuren E.P. de Vink1埃因霍温理工大学数学与计算机科学系P.O. Box 5600 MB荷兰摘要我们研究的隐私，这是被称为数据匿名的许多方面之一，在正式的上下文中。 数据匿名表示某些观察到的数据（例如投票）是否可以归因于用户（在本例中为投票者）。通过分析一个著名的电子投票协议，我们验证了数据匿名的形式化处理。关键词：电子投票，匿名与隐私，数据匿名，属性集，安全协议的形式化方法1介绍电子服务使用者的私隐当然不是理所当然的事。电子服务，如忠诚计划和支付系统（例如电子拍卖和电子收费）可能会在隐私领域产生严重后果目前可预见的发展，如RFID [4]，导致在这方面越来越多的关注。在“隐私”的框架在通用标准[31]中，功能类FPR区分了隐私的四个方面匿名性，我们研究的主题，确保某人可以使用资源或服务，而不透露其身份。假名确保某人可以在不披露其身份的情况下使用资源或服务，但仍然可以对这种使用负责。不可链接性确保某人可以多次使用资源或服务，而其他人无法将这些使用链接在一起。不可链接性与匿名性的区别在于，尽管在匿名性中用户也是未知的，但是可以提供不同动作之间的关系。不可观察性确保某人可以在没有其他人，尤其是第三方的情况下使用资源或服务。1 通讯作者。 电子邮件地址：evink@win.tue.nl1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2006.11.0016S. Mauw等人/理论计算机科学电子笔记168（2007）5各方，能够观察到资源或服务正在被使用。非正式定义，如上所述，对于理解不同的隐私概念是必不可少的，但只允许非正式地调查一个系统除了[31]，匿名的非正式定义在[34，16，42]中给出。关于匿名的正式定义，文献中提出了几种表达匿名的方法Halpern和它们正式规定了信息隐藏的要求，特别是匿名性。关于这些属性的推理可能使用认知逻辑。Hughes和Shmatikov [30]将系统的行为描述为一组函数。信息隐藏属性，如匿名性，是通过攻击者对这些功能的了解来形式化的。在这方面，休斯和什马蒂科夫谈到了攻击者的功能观。作者表明，功能视图框架能够指定任何协议形式主义和任意攻击者模型的信息隐藏属性。描述了表征匿名性和不可链接性方面的信息理论方法，例如，在Serjantov和Danezis [47]、Diaz等人撰写的文章 [22]并由Steinbrech erandKo？psell l [49]。另一种表示匿名形式的方法是通过进程代数来完成的。Schneider和Sidiropoulos [46]在提出匿名定义时使用CSP。它们定义了关于事件集合A的匿名性。与A相关的关联性意味着，如果A中的任何事件发生，它同样可能是A中的任何其他事件。在[37]中，继P Fitzmann等人[42]之后，本作者通过引入匿名群AG的概念给出了匿名性的正式定义。匿名组精确地表示从入侵者的角度来看是相同的用户组入侵者无法区分匿名组中的某个用户和其他用户。随后，在[37]中，分析了洋葱路由网络[26，50，52]在何种程度上以及在何种条件下实现了网络匿名协议的概率分析，沿着Shmatikov [48]为Crowds [44]所做的工作路线，在Onion Routing [50]和Tarzan [24]中建立的路径已经在[3]中报道。在这篇文章中，它表明，存在着匿名的另一个方面，在第[46]和[37]条中正式述及。在那里，重点是定义什么可以被称为控制匿名。这是指隐藏事件的发起者。这种匿名性在匿名通信网络中起着重要作用。当考虑其他系统（例如电子投票系统）时，人们希望证明某些信息（特定投票）不能与其发起者（即投票人）相关。换句话说，数据的来源必须保密。这个属性在这里被称为数据匿名性。为了对数据匿名性进行推理，我们需要一个模型，在这个模型中，不仅可以对事件的发生进行推理换句话说，需要一个比[46]和[37]中在本文中，我们将集中在数据匿名S. Mauw等人/理论计算机科学电子笔记168（2007）57并定义一个正式的框架来推理这个概念。如前所述，数据匿名在投票系统中起着至关重要的作用电子投票系统旨在为记录和清点选票提供方便、高效和安全的设施。电子投票可以用于实现小规模的地方选举，如股东大会到全面的全国选举。Lipmaa [36]发现了电子投票的两种情况：kiosk投票（使用特殊硬件在某些固定位置投票）或使用一般可用设备的互联网投票例如PC或移动电话。在文献中，发现几组要求适用于电子投票方案[6，25，20]。这些要求并不相同。在[19]中，Cranor和Cytron对文献进行了调查，并制定了四个与安全相关的核心属性。（1）不应更改投票。(2)应该不可能造成不考虑有效投票的情况。(3)另一方面，无效票不应计入最后计票。（1）只有合格的选民才能投票。(2)这些选民只能投票一次。每个人都应该能够独立地核实计票是否正确。隐私（1）任何人都不可能将投票与选民联系起来。(2)此外，选民不能证明她以特定的方式投票为了满足上述要求，电子投票系统的设计者已经在系统中的不同实体之间设计了安全协议。这些协议的目标是保证系统即使在入侵者存在的情况下也能满足要求。很明显，我们的数据匿名概念是指隐私要求的第一部分广义上讲，可以辨别两组电子投票方案：（i）使用同态加密的方案（例如，参见[6，17，18，29]）;（ii）要求匿名通道的方案，该匿名通道用于在投票时隐藏选民的身份（包括[14，25，40，11]）。Fujioka，Okamoto和Ohta [25]的投票方案-我们专注于此，我们将其称为FOO投票方案-使用盲签名。在使用盲签名的投票方案中，投票者从管理员处获得令牌在此注册阶段之后，投票者可以打开令牌并通过匿名通道将其加密投票（由管理员签名）发送到计数器。最后，投票者将她的解密密钥--同样通过匿名通道--发送到计数器。解密后，计数器将投票添加到计数中。完整的电子投票协议将在下面的第3节中进行非正式和正式的描述如前所述，FOO方案使用匿名通道。然而，在Fujioka、Okamoto和Ohta的论文中，他们并没有对匿名通道提出明确的要求已经提出了几个匿名渠道和分析 我们提到[12，44，41，32，26，50，52]和[21，43]。对FOO投票方案的非正式分析[25，45]表明，它满足了8S. Mauw等人/理论计算机科学电子笔记168（2007）5数据匿名要求。Herschberg，Cranor和Cytron对基于FOO的投票系统EVOX和Sensus [28，19]进行了非正式分析。Herschberg [28]得出结论，在EVOX系统中，只有当匿名通道被破坏时，数据匿名方面才会受到损害，也就是说，如果通道向计数器透露了有关投票来源的信息。Cranor和Cytron [19]认为，Sensus系统满足了隐私要求的第一部分，但没有实现第二部分。换句话说，Cranor认为Sensus完全实现了数据匿名，但它并没有阻止选民以某种方式投票。在本文中，我们将正式分析FOO投票方案。更具体地说，我们将验证FOO在多大程度上符合数据匿名的定义在他们的论文[35]中，Kremer和Ryan对FOO投票协议的三个安全方面进行了形式化分析使用ProVerif工具[8，9]证明了公平性和合格性，而对于隐私，他们在应用的pi演算中给出了手动证明[1，2]。他们的隐私证明包括验证两个系统在观察上是在第一个系统中，投票人V1有v1票，投票人V2有v2票，而在第二个系统中，投票人V1有v2票，投票人V2有v2票。如果观察者不能区分这些系统，那么投票者和他们的选票是不可分辨的。这让人想起[46]的基于置换的方法的控制匿名性。在[39] Nielsen，Andersen和Nielson使用LY SA演算对FOO协议进行了分析。LY SA演算是π演算的一种方言，围绕着全局网络的概念[10]。在[39]中，FOO协议被形式化为LY SA。有人认为，该协议满足了准确性和可核查性以及民主和公平的要求。对于匿名性，考虑了投票者和投票的不可链接性上述方法与我们的方法之间的主要区别在于，我们定义了投票者的属性集（与匿名集互补），它包含了所有可能归因于投票者的投票。这使我们能够衡量选民的匿名性，而克雷默和瑞安的方法提供了一个是/否的答案。在FOO协议的情况下，属性集是一个有用的概念，因为Fujioka，Okamoto和Ohta并不完全清楚他们提到的同步点。这些同步是协议工作所必需的吗？是否有任何可能的替代同步点，将做？我们将能够在确定没有同步点的FOO协议的属性集我们的方法还支持设计替代方法来增加归因集，而不提供完全匿名。这种实用的匿名性对于更大规模的应用是有吸引力的，并且可以在没有所提到的同步点的情况下实现。我们对FOO投票方案的形式化利用了ACP风格的进程代数[5，23，7]。在[35]的建模中，匿名通道没有显式化。在应用的pi演算中，每个通道都是匿名的，除非输入和输出可以显式链接。通过显式地对匿名通道进行建模，我们采取了相反的立场。因此，我们可以正式表明，FOO投票方案的数据匿名性水平取决于两项：（i）S. Mauw等人/理论计算机科学电子笔记168（2007）59匿名通道;（ii）注册阶段后的同步方式我们的形式化分析表明，从数据匿名的角度来看，这些项目是相互关联的。如果在注册阶段之后没有发生同步，则只有在对匿名通道提出额外要求时才能获得数据匿名。在选民可能只有在每个人都登记后才开始投票的情况下，匿名渠道可能不那么复杂。最后，如第5节所述，我们的分析表明，如果出版媒介受到损害，则存在一个弱点。本文的组织结构如下。在第2节中，我们提供了数据匿名的正式定义在第3节中，我们描述并指定FOO投票方案。第4节提供了一个特征的匿名投票者在FOO投票计划的属性集，而第5节提出了由此产生的脆弱性分析。在第6节中，我们讨论了结论和未来的研究。2数据安全框架让数据、密钥、随机数和用户，由d、k、n和u表示，是（敏感）数据、密钥、随机数和用户的原始类。术语类由BNF给出，范围为：：= d |K |n |u|（，）|{}k|[] u因此，一个项可以是一个原始元素，一对项，用密钥k加密的项k，或者归属于用户u的项k。 属性[i]u用于将术语与用户相关联。特别是，我们将对可以链接到特定用户的敏感数据感我们用du表示数据d出现在项的子项[]u中。我们将在流程描述中使用构造[]u协议被建模为使得任何代理（包括入侵者）都不能检查或修改属性。 它应被视为元一级的一个结构;其唯一目的是便利核查。事件的类Event，由e表示，由三个元素组成：发送者、接收者、接收者，表示从用户发送者到用户接收者的术语“接收者”的通信。事件=用户×用户×条款。在e=sender，receiver，的情况下，我们使用msg（e）来表示项。在一个给定的设置中，我们固定一个类Obs事件的可观察性。迹的迹类，由迹=事件迹给出，范围为t，由事件的所有有限迹一个系统S的语义是由迹的集合trace（S）Traces给出的。我们称迹（S）为系统S的迹集。函数obs：Traces→Traces定义为：obs（ε）=εobs（e·t）= e·obs（t）如果e ∈Obs o b s（e·t）= o b s（t）i f e∈/Obs。显然，对于任何t∈Traces，obs（t）∈Obs成立。我们使用符号<$∈t10S. Mauw等人/理论计算机科学电子笔记168（2007）5，（，）left（，）右，k{}k， k dec[编辑]对于一个术语，如果，对于一些发送者发送者和接收者接收者，发送者、接收者、接收者是t的事件。我们用符号d∈ut表示一个数据d，如果d∈u∈t表示某个项，则用迹t表示。对于迹t，如果没有数据d，则d∈ut成立，则我们写为：我们使用a作为Data=Data{}的典型元素。知识集的类Know，由K表示，是术语子集的集合，即Know=P（Terms）。对于特定的情况，我们固定一个知识集I∈Know，称为初始入侵者知识。辅助功能知道：知道×轨迹→知道，在一分钟内给出，返回知识集K和轨迹t，从知识K开始沿着轨迹t建立的知识。首先，我们需要一个知识集的闭包概念我们说，如果可以通过重复使用表1中的推导规则从K推导出，则可以从知识集K推导出项K，记为K。表1：知识推导规则然后，知识集K的闭包闭包（K）由下式给出：闭包（K）={|{\fn黑体\fs19\bord1\shad1\1cHD8AFAF\4cHC08000\b0}基于闭包的概念，函数know可以由下式给出：已知（K，ε）=K知道（K，e·t）=知道（J，t）其中J=闭包（K<${msg（e）}）。请注意，上述定义中的知识积累忽略了发送者和接收者的角色。因此，可以观察到痕迹的所有通信为了弥补这一点，我们使用函数obs来防止收集特定的流量为了处理加密术语，我们引入了标记的概念，这是一种辅助技术机制，用于标记观察者或入侵者无法解密的术语。本质上，在密钥k、l、m不在特定知识集中的情况下，对于项k、k和ρ，有助于区分两个迹{k}k·{k}l与{ρ}m· {ρ}m，同时识别两个迹线{k}k· {k}l和{k}l· {k}k。第一我们引入了具有典型元素τ的标签类Tags。TagTerms类构造类似于类Terms，但添加了标记作为新的基本成分。因此，也由BNF给出的TagTerms：：= d|K|n|u|τ|（，）|{}k|u.S. Mauw等人/理论计算机科学电子笔记168（2007）511KKKKK类TagTraces是标记事件的有限字符串的集合，即三元组的有限字符串：sender，receiver，sender，其中sender∈TagTerms。一个标签是一个内射映 射 θ ： 术 语 → 标 签 。 给 定 知 识 集 K 和 标 记 θ ， 解 释 函 数 intθ ：Terms→TagTerms如下：intθ（p）=p对于p=d，k，n，uintθ（（，））=（intθ（），intθ（））K K Kintθ（{n}k）={intθ（n）}k如果k∈KK Kint θ（{k}k）=θ（{k}k）ifk∈/Kintθ（[] u）=[intθ（）] u。K K因此，如果项{k}用不属于所考虑的知识集的密钥k加密，则组合项{k}k被解释为标签，即标签θ（{k}k）∈由标签θ产生的标签。现在，考虑两个迹t，tJ∈迹-如果它们产生相同的知识并且在标签的重命名之前是相等的，则相对于知识集K，记为tKtJ，它们是等价的，即，知道（K，t）=知道（K，tJ）存在一个双射β：Tags→Tags使得intθ（t）=intβ<$θ（tJ），对任意LL标记θ和L=know（K，t）。例如，对于迹t1={d1}k·d2·{d3}l，t2={d3}l·d2·{d1}k，知识集K满足k，l∈/K，并且一个知识集可以聚集 θ，其中τ1=θ（{d1}k）·d2·θ（{d3}l）= τ1·d2·τ3，其中τ1= θ（{d1}k）并且τ3= θ（{d3}l）。如果β：Tags→Tags是切换τ1和τ3的标签的双射，我们得到intβθ（t2）=β（t3）·d2β（t1）=τ1·d2·τ3。 因此，t1≠Kt2。另一方面，没有双射γ：Tags→ Tags假设τ1τ3，将验证γ（τ1）=τ1和γ（τ3）=τ1。对于上面的t1和t3={d1}k·d2·{d1}k，w= vet1/vkt3。标记背后的思想是，系统的不同运行中的不同位串可以表示相同的加密信息。这种差异可能是由于非本质现象，特别是在另一轮中对随机数的不同选择。位串的识别在同一个系统运行中没有意义，因为不同的位串代表真正不同的数据。最后，我们能够给出我们的归属概念的定义集定义2.1设S是一个具有迹集trace（S）、可测值集Obs和初始入侵者知识I的系统。用户u关于迹t∈迹（S）的属性集ASt（u）由下式给出：ASt（u）={a |<$tJ∈ traces（S）：obs（t）<$Iobs（tJ）<$a ∈utJ}.因此，给定系统运行t，如果对于某个轨迹tJ，从入侵者的角度来看与轨迹t相同，即t = t j，则数据d可以归属于用户ud出现在tJ中的某个消息中与u相关联的子项中。12S. Mauw等人/理论计算机科学电子笔记168（2007）5例如，如果u是一个投票者，t是一个投票协议的运行，那么u如果从入侵者的角度来看，每一个收集到的投票都可以归因于u，那么在这次运行中是匿名的。如果ASt（u）包含在t中收集的所有投票，则会出现这种情况。如果在迹tJ中，观测等效于迹t，没有数据d与用户u相关联，则可以将特殊元素d分配给用户u。假设s（S）={t1，t2，t3}，其中t1=[{d1}k]u·[d2]v·{[d3]w}l，t2={[d3]u}l·[d2]v·{[d1]u}k ， t3={[d1]u}k·[d2]v·{[d1]w}kanddd2/=k，l∈/I ，w e have，对于u，ASt1（u）={d1，d3}asd1<$u[d1]u∈t1，1<$It2anddd3<$u{[d3]u}l∈t2. 对于用户v，它保持ASt1（v）={d2}，因为只有d2与v相关联。此外，对于用户w，我们有ASt1（w）={d3}是单例。在t2中，没有数据与w相关联，而迹t3与参考迹t1并不明显等价。3FOO投票计划在本节中，我们将介绍Fujioka，Okamoto和Ohta在1992年提出的投票方案首先，我们给出了一个非正式的解释，这是作为一个正式的描述的基础。3.1非正式说明在本节中，我们将解释Fujioka，Okamoto和Ohta [25]提出的电子投票协议，也称为FOO投票方案。该方案声称满足一些安全要求，其中之一是选民的隐私。我们将使用图1中的消息序列图中的协议的非正式表示来解释该协议。表2总结了说明中出现的符号。该协议描述了管理员、多个投票者和计数器之间的通信。管理员的作用是检查投票人是否有资格投票，并在投票人的（盲法）选票上签名。计数器的作用是收集所有（匿名）选票并公布。我们专注于个人选民的协议交互。 投票者v通过选择他的随机秘密密钥k（v）和随机现时数n（v）开始，他的选票b（v）。通过用他的密钥加密他的选票，他构造了一个提交的选票cb。在稍后的阶段，投票人将通过（匿名）提供cb和k（v）来公开他的选票。接下来，投票人用他的秘密随机数来隐藏他的选票，这产生了bcb。为此，他使用了用“盲”表示的盲法。为了确保这是他的盲选票，他签署的结果，这给sv。投票人将他的身份、盲化的已提交选票和签名的盲化的已提交选票发送给管理员，以便允许管理员检查投票人（仍然）有资格投票并验证v管理员通过签名并将签名的盲化承诺投票sa返回给投票者来确认接收到的投票。 管理员使用的签名算法是所谓的盲签名技术[13]。其目的是，投票人可以通过以下方式从已签名的盲化承诺选票中获得已签名的承诺选票：S. Mauw等人/理论计算机科学电子笔记168（2007）513vb（v）k（v）n（v）选民身份选民选票选民钥匙投票者V的CB{b}k（v） 承诺投票BCBcbn（v） 盲法承诺投票SV签署V（BCB）由vsa检查（v）签署a（bcb）盲法提交的选票，V可以投票吗？验证x（p，sp）scb=sa/n（v）L1签署a（cb）p是否真的被x签名？由一名加密投票L2公开投票表2：使用的应用揭盲操作符（用/表示）。形式上，这要求签名和设盲操作互换。因此，在验证了管理员的签名之后，投票人可以导出SCB，这是由管理员签名的他的承诺选票在此之后，管理员的角色结束，投票人与计数器通信从投票人发送到计数器的消息通过匿名渠道进行，因此无法检索消息发送者的身份。投票人将其提交的选票cb及其签名版本scb发送给计数器，计数器验证它确实由管理员签名。他将从所有投票者接收到的信息存储在列表L1中，并且在所有投票者投票之后（或者在某个截止日期过去之后），他公布该列表。每个投票者现在都可以验证他提交的选票是否在列表中，并将打开提交选票的密钥发送到计数器（再次使用匿名通道）。计数器打开选票，并最终公布第二个列表L2，包含所有打开的选票。请注意，我们只解释了协议的主线。我们没有具体说明如果其中一个参与者试图破坏投票而导致其中一个检查失败会发生什么。有兴趣的读者可以参14S. Mauw等人/理论计算机科学电子笔记168（2007）5考[25]了解详情。S. Mauw等人/理论计算机科学电子笔记168（2007）515图1：FOO电子投票协议。16S. Mauw等人/理论计算机科学电子笔记168（2007）53.2正式规格接下来，我们提供了进程代数中FOO投票方案的正式规范（参见，例如，[5、23、7]）。这个进程代数允许我们给出FOO投票方案的所有迹的集合的紧凑和正式的规范。 然而，应该注意的是，我们对匿名性的处理并不依赖于任何特定的形式主义，只要它支持对痕迹的推理。对于不熟悉所选规范语言的读者，我们总结了所使用的结构的含义。 一个过程是通过一个（可能是递归的）方程来具体化的。 一个过程可以由多个数据值来参数化。 可以使用操作符组合进程。 我们用·表示顺序组合，+表示非确定性选择，x∈X表示+在一个索引集X上的推广，表示（交错）并行表达式，x∈X表示在一个索引集X上的推广。并行组合操作符还提供了一种通过同步来同步两个进程的方法，记录通信事件。通信功能的定义采用以下形式：|b = c，表示如果事件a和b并行发生，则它们将导致事件c。为了封装部分通信（即强制事件同步），使用封装操作符H，其中H是必须同步的通信事件的集合除了这些流程级的操作符之外，我们还需要一些数据级的操作符和额外的数据类型。其中大部分已经在上面定义过了。此外，我们定义类型List1、List2和Bu_bu我们使用运算符来表示将元素添加到列表以及添加到缓冲器。删除一个元素用g表示。 我们用πn表示元组的第n个元素上的投影，并且我们推广了这种符号以显而易见的方式应用到元组列表中。我们用V和V_s分别表示所有（潜在）投票者和所有选票的集合。投票者扮演用户的角色，如第2节所述。由于协议的非正式描述没有指定匿名通道的精确特征（令人惊讶的是，在文献中没有标准定义因此，除了信息规范中提到的三个过程之外，我们将定义另外两个过程，代表匿名渠道和发布媒介。因此，我们认为过程行政（S）， 计数器（L1，L2），通道（B），发布器（L1，L2），以及一类过程Voter（v），其中L1∈List1，L2∈List2，S∈V，B∈Bu ∈ V，v∈V.此外，我们使用子进程CounterJ、PublisherJ和PublisherJJ。使用这些过程的简写符号c，a，ch，p，我们用Dest={c，a，ch，p}V表示消息的源和目的地的集合。S. Mauw等人/理论计算机科学电子笔记168（2007）517可能的事件取自字母表E ={sx→y（？），rx→y（？）|x，y∈Dest，n∈Terms}。例如，事件sv→a（n）意味着投票者v发送了一条消息n，显然是给管理员的。同样地，rch→c（k）表示计数器接收到一个消息k，显然来自信道。在形式描述中，我们将使用简写符号cb表示{b}k，bcb表示cb/n，sv用于sigv（bcb），sa用于siga（bcb），scb用于sa/n（v）。我们努力通过排除所有例外情况来获得最低限度的规范。在理解了前一节中协议的非正式描述之后，正式的代数规范相对容易阅读。 然而，我们将解释我们所做的设计决策的一些复杂性投票人（v）=Σb∈键，k ∈键，n ∈随机数sv→a（v，bcb，sv）·ra→v（sa）·sv→ch（cb，scb）·ΣL1∈List1，（cb，scb）∈L1rp→v（L1）·sv→ch（{[b]v}k，k）·Σ（L1，L2）∈List1×List2rp→v（L1，L2）.投票者首先（非确定性地）选择他的选票、密钥和随机数。在此选择过程中，我们没有使用内部事件来明确这一点，我们假设这个选择完全在选民的控制之此外，我们要求不同的选民选择不同的密钥和不同的随机数。在发送第一条消息后，投票人收到由管理员（sa）签名的盲化承诺选票作为一个例外，这个读事件之前没有求和。原因是，虽然投票者不能自己构建这个消息，但他可以验证接收到的数据是否满足要求。给定一个确定性签名算法，将只有一个这样的术语。只选择这种有效签名项的能力由sa的扩展的句法形式表示，即siga（bcb），其中bcb为投票者所知。当投票人打开他的选票时，通过将他的密钥经由信道发送到计数器，我们将不得不建模，即将打开的投票归因于这个特定的用户。这种属性并不影响系统的行为，也不是入侵者可以观察到的。包括这种归属的唯一原因是通过确定可能归属于该选民的选票来对系统进行正式分析。 请注意，我们并没有要求选民明确地与选举的不同阶段同步。唯一可以扮演这个角色的事件是从发布者接收列表ΣAdmin（S）=v∈V，n∈Terms r v→a（v，n，sigv（n））·s a→v（siga（n））·Admin（S\{v}）.管理过程是由一组选民参数化的，18S. Mauw等人/理论计算机科学电子笔记168（2007）51投票 在向投票者发送了签名的选票之后，用户将从该集合中删除。计数器（L1，L2）=Σ∈Termsrch→c（+sc→p（L1）·计数器J（L1，L2）计数器J（L1，L2）=·计数器J（L，Ln（n，k，dec（））n∈π1（L1），k ∈Keys，deck（n）∈Keys+sc→p（L2）.ch→c12k计数器分两个阶段进行，这两个阶段由两个不同的过程变量建模。在第一阶段，计数器收到管理员签署的条款。从第一阶段到第二阶段的过渡是以非确定性的方式建模的。这允许我们在计数器使该转换“过早”的情况下验证系统。在第二阶段，计数器接受允许他打开已提交选票的密钥。我们注意到，条件<$∈π1（L1）应解释为不考虑用户属性在<$N。第二阶段的结束也被非确定性地建模。通道（B）=Σv∈V，n∈项rv→ch（n）·信道（B<${n}）Σ+n∈B s ch→c（n）·Channel（B g {n}）。匿名通道接收来自投票者的消息，这些消息被添加到缓冲器。或者，通道可以从缓冲器中选择任何消息，并将其传递给计数器。jJJ发布者（L1，L2）=LJ∈List1rc→p（L1）·发布者（L1，L2）发布者J（L1，L2）=<$v∈Vsp→v（L1）<$rc→p（LJ）·发布者JJ（L1，LJ）2 2发布者JJ（L1，L2）= v∈Vsp →v（L1，L2）.发布者进程从计数器接受一个列表并将其发送给所有投票者。在发布第一个列表的过程中，发布者还可以接收第二个列表，之后这个列表也会被分发。最后，我们指定完整的系统FOO作为其所有代理的并行组合。因此，我们认为，FOO= H（ v∈VVoter （ v ）Admin （V ） Counter （，） Channel （） Publisher（））。我们用所有投票者的集合初始化管理员，用空列表和缓冲器初始化其他进程。通信功能匹配读取和发送事件，即s x→y（x）|r x→y（n）= c x→y（n）S. Mauw等人/理论计算机科学电子笔记168（2007）519对于x，y∈Dest和x∈Terms。事件cx→y（x）是第2节中介绍的抽象事件x，y，x的具体形式。封装或禁止事件的集合H由下式给出：H ={sx→y（？），rx→y（？）|x，y∈Dest，n∈Terms}。现在，通过应用在例如[5]中描述的熟悉的操作语义，可以轻松地遵循指定系统的轨迹轨迹集（FOO）匿名通道的定义要求其输入事件不能被内部观察到truder。因此，我们定义可观察事件的集合Obs ={c x→y（x）|（x，y）/=（v，ch），n∈Terms}. 我们不会对最初的入侵者知识岛原因是我们会考虑所有选民都被信任的情况，也会考虑部分选民可能不被信任的情况。不受信任的投票者将通过假设他们选择的选票、密钥和随机数是入侵者最初知道的来建模。4FOO属性集为了刻画投票者的属性集，我们需要一个辅助定义。谓词acmatch（i，t）在跟踪t中保持为真，直到位置i，由管理员签名的盲投票的数量与计数器接收的覆盖投票的数量完全匹配。索引i使得acmatch（i，t）在FOO系统的跟踪t中的特定属性是，在t中不晚于位置i登记的选民必须发送计数器收集到的覆盖选票之一。定义4.1谓词acmatch由下式给出acmatch（i，t）i≤len（t）#{j |j i，它保持tJ [j] = cch→c（{b}k，siga（{b}k））。因此，tJ [j]仍然是不匹配的。在第二种情况下，我们可以选择索引i和j，使得tJ [i] = c a→v（siga（{b}k<$n）），tJ [j] =c ch→c（{b}k，siga（{b}k））。由于tJ [i]和tJ [j]匹配，因此j∈chunk（i，tJ）。通过对唯一键的假设，我们得出，对于没有索引l，22S. Mauw等人/理论计算机科学电子笔记168（2007）5tJ [l] = c ch→c（{[b] v}k，k）。利用等价性tItJ，类似于上面的推理，得到t的相应指数。因此，也可以得出，RHSt（v）。Q为了证明定理4.2的另一半，我们需要一个组合结果。假设a一般来说，一个人不可能在不打乱优先顺序的情况下改变对的排列。 例如，在一个示例中， 在迹线a1a2b1b2中，我们可以交换b1和b2，同时保持a1<$b1和a2<$b2，但是 在a1b1a2b2中我们不能。 粗略地说，只要某个a在同一个块中就像任何b与ab一样，我们可以找到一个包含一对特定的a和b的出现的配对，它尊重优先级。引理4.6设w是长度为2s的字符串，其中符号ar， br，对于 1≤r≤