安全电子投票算法的性能与可靠性建模：基于马尔可夫过程代数的分析

理论计算机科学电子笔记128（2005）45-58www.elsevier.com/locate/entcs一种安全电子投票算法的可执行性奈杰尔·托马斯1英国泰恩河畔纽卡斯尔大学计算机科学学院摘要本文考虑了一个安全的电子投票方案的性能和可靠性建模该方案提供了安全的可验证盲投票，但这种安全级别的管理开销相当大利用马尔可夫过程代数建立了n个分布式投票者基本系统的性能模型该模型支持常见的状态空间爆炸问题。因此，开发一个更简单的模型，以允许更大和更实际的相关系统进行研究。原始模型，然后扩展到包括选民可能会失败的可能性，并考虑两种模式的恢复。使用从测量该计划的实施获得的数据，以确定近似的准确性的模型进行数值评估。关键词：安全投票方案，性能建模，PEPA1介绍使电子投票安全已经是二十多年来的一个活跃的研究课题，并且自从Chaum[2]开始使用匿名通道来分离选民和选票以来，已经引入了许多安全的电子投票方案投票场景发生在许多情况下，以在分布式系统中执行许多任务，以及促进人类活动之间的投票。最公开可见的安全投票形式是在政治选举中使用在线投票系统，这一做法已在若干国家采用。这种形式的投票有几个明显的要求。1电子邮件：nigel. ncl.ac.uk1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.01.01246N. Thomas/Electronic Notes in Theoretical Computer Science 128（2005）45• 只有登记的选民才能投票。• 选民只投票一次。• 不应该知道谁投票，或者他们如何投票。这些因素意味着在这种情况下使用的任何投票方案必须提供足够的认证、投票管理和所谓的盲机制，同时在潜在不安全的通信介质上操作。Fujioka等人[6]将这些要求形式化为完整性（所有选票都正确计算），健全性（不诚实的选民不能破坏选举），隐私性（选票），不可重复使用性（不能投票两次），资格（投票），公平性（投票），可验证性（结果）。此外，Iversen [9]介绍了收据自由的要求;许多协议都会发出某种形式的收据或令牌，以向投票者证明系统的行为与它一样。应该的然而，这些收据可能被不诚实的选民用来证明他们以某种方式投票，从而促进投票。许多安全投票方案在某种程度上依赖于加密数据，即使使用快速处理器，加密和解密也会增加数据处理的开销。然而，由于需要额外的通信以确保满足安全投票的要求，因此产生了重大的安全的投票方案通常使用某种形式的匿名通道、数字签名、盲签名、可信机构和多个密钥密码来分离投票者、投票机构、投票本身和投票计数。显然，在提供这些测量时存在大量开销，因此这种系统的性能具有明显的实际意义。2一种安全的电子投票算法本文考虑了Fujoika等人提出的一个安全的电子投票方案，该方案已经在至少两个系统SENSUS [5]和EVOX [7]中实现。该方案包括任意数量的投票者，一个管理员颁发投票权，和一个计数器收集选票，并确定结果。匿名通道用于在投票者和收集器/计数器之间传递该方案是这样描述的。• 准备：选民i(i) 选择投票策略。(ii) 使用比特承诺方案ci来承诺策略。(iii) 使承诺的选票变瞎，bi。(iv) 在盲法选票上签名。(v) 将已签名的盲法选票发送给管理员，盲法选票N. Thomas/Electronic Notes in Theoretical Computer Science 128（2005）4547以及唯一的投票者ID，IDi。• 行政：行政人员(i) 接收来自投票者i的消息。(ii) 检查选民i的投票权。(iii) 检查投票人i尚未投票。(iv) 验证签名;如果有效，请在盲态选票上签名。(v) 把sai发给选民i。(vi) 当管理期结束时，发布一个包含每个{IDj，bj，svj}。• 投票：投票人i(i) 揭盲sai给由管理员，bai签名的选票.(ii) 检查签名。(iii) 将{ci，bai}通过一个匿名的信道发送到客户端。• 收集：柜台(i) 接收来自投票者i的消息。(ii) 在一个列表中添加{N，ci，bi}，其中N是唯一的参考号。(iii) 收集期结束后，公布一份清单，{N，ci，bai}。• 开幕式：选民i(i) 检查投票是否出现在计数器发布的列表中;如果没有，请上诉。(ii) 将比特提交密钥ki通过匿名的频道• 计数：计数器(i) 使用ki检索投票策略。(ii) 检查策略是否有效。(iii) 当所有的选票都被计算出来后，公布最终结果。3简单PEPA模型[8]中给出了PEPA的正式介绍，在本节中给出了简短的非正式摘要。PEPA是一个马尔可夫过程代数，它只支持在给定速率下负指数分布的行为。用PEPA编写的规范表示马尔可夫过程，可以映射到连续时间马尔可夫链（CTMC）。系统在PEPA中的活动和组件方面进行了详细说明。活动（α，r）由以下类型描述的活动，α，和相关的负指数分布的速率布西翁河该比率可以是任何正实数，或者是未指定的48N. Thomas/Electronic Notes in Theoretical Computer Science 128（2005）45defdefdefdefdefdefdefdefdefdefdefdefdefdefdef使用符号T。 描述组件的语法如下：P =（α，r）.P|P + Q| P/L|PD Q|一L成分（α，r）.P以速率r执行α型活动，然后表现得像P。组件P+Q的行为要么像P，要么像Q，结果行为由第一个要完成的活动给出通讯器-成分P/L的行为完全类似于P，除了集合L中的活动被隐藏，它们的类型不可见，而是作为未知类型τ出现。并发组件可以被同步，PDQ，这样，L合作集合L涉及两个分量的参与在PEPA共享活动以参与者的最慢速率发生，并且如果如果某个组成部分中未指定某个比率，则该组成部分相对于该类型的活动是被动的。用并行组合子来表示具有不同活动的同步，即： PQPDQ. Ad=efP∅给出常数A表示分量P的行为。上述算法在PEPA中建模如下。V oter0 =（choose，c1）.V oter01+（choose C，T）.V oter4V oter01 =（bitcommit，b1）.V oter02+（bitshC，T）.Voter4V oter 02 =（blind，b2）.V oter03+（bitshC，T）.Voter4V oter03 =（blind，b3）.V oter04+（blind shc，T）.V oter4V oter 04 =（sign，s1）.V oter05+（blind shc，T）.V oter4Voter0 5=（sendA，s2）. （sendV，T）.V oter1+（sendshC，T）.V oter4V oter 1 =（unblind，u1）.V oter11+（sendshC，T）.V oter4Voter1 1=（unblind，u2）.V oter 1 2+（shortC，T）.Voter 4 V oter 1 2 =（verify，v2）.V oter 1 3+（shortC，T）.V oter 4 V oter 1 3 =（verify，v3）.V oter 1 4+（shortC，T）.V oter 4 V oter 1 4=（sendC，s6）.（C，T）.V oter2+（C，T）.V oter4V oter2 =（检查，第4页）。V oter3+（检查，（1 − p）c4）。（发送公司第7条）。Voter3 =（appeal，a1）. （sendCo，s7）.V oter4V oter 4 =（new，T）.Voter0Administrator=（sendA，T）. （检查，c2）。（检查2，c3）。（verify，v1）.N. Thomas/Electronic Notes in Theoretical Computer Science 128（2005）4549（签署第3条）。（签署第4条）。（第5条）。+（pshA，p1）. （新，T）.署长50N. Thomas/Electronic Notes in Theoretical Computer Science 128（2005）45defdefdefdef收集器i=（sendC，T）。（verify，v4）. （verify，v5）. （添加a2）。集电极i+1+（Ω shA，T）。（见第2页）计数器i，0≤i N收集器N=（N shA，T）。（C）第2页。计数器N计数器i=（sendCo，T）。（check，c5）.计数器i−1，0

下载后可阅读完整内容，剩余1页未读，立即下载