基于Coral的多播组密钥管理协议自动化模型检测与分析

理论计算机科学电子笔记125（2005）125-144www.elsevier.com/locate/entcs基于Coral的格雷厄姆·斯蒂尔1，2艾伦·邦迪3爱丁堡大学信息学院，爱丁堡，EH8 9LE，苏格兰摘要本文描述了两个多播组密钥管理协议在一阶归纳模型中的建模，并通过自动归纳反例发现器CORAL发现了以前未知的攻击。这些类型的协议以前没有在主动入侵者的情况下进行过分析。CORAL被证明是一个适合工作的工具，因为与大多数发现攻击的自动化工具不同，它直接处理开放式模型，其中代理的数量和它们扮演的角色是无限的。 此外，CORAL在案例研究的过程中，我们还讨论了其他问题，围绕多播协议分析，包括确定目标的协议相对于预期的信任模型，建模的控制条件，这是相当复杂的比标准的两个和三个党的协议，和有效的搜索的状态空间所产生的模型，它有一个更大的分支率比标准协议。保留字：安全协议分析，组组播密钥管理1介绍在分析[7]中给出的两方和三方协议的标准语料库方面，密码安全协议分析领域可以说是饱和的。许多研究的注意力现在已经转向试图扩大[1]本文中报告的工作是在第一作者作为德国卡尔斯鲁厄大学和意大利热那亚大学的访问研究员得到欧洲“微积分”计划的支持时进行的2电子邮件：graham. ed.ac.uk3 电子邮件地址：bundy@ed.ac.uk1571-0661 © 2005由Elsevier B. V.出版，CC BY-NC-ND许可下开放获取。doi：10.1016/j.entcs.2004.05.023126G. Steel，A.Bundy/Electronic Notes in Theoretical Computer Science 125（2005）125技术的范围，例如分组协议[14，27，24]。术语这可以采取在代理之间运行的单个密钥建立的形式，或者一系列请求加入和离开具有关联密钥更新的组的形式。一些协议涉及可信密钥服务器。对组协议的重大攻击已经出现在文献中，但这些都是通过患者的笔和纸分析发现的[22 ]第20段。尝试扩展自动工具来分析此类协议的结果好坏参半（见§2）。Taghdiri和Jackson [27]发表了对Tanaka和Sato提出的组组播密钥管理协议的分析，[28]第10段。他们能够找到主要的论据，并提出了一个新的，改进的协议版本。然而，他们的模型是相当弱的：特别是，它不包括一个积极的攻击者。 在本文中，我们研究了它们的改进，协议使用CORAL，[24]，并展示它如何发现两种新的攻击和原来的一样严重此外，我们还研究了Iolus密钥管理协议[18]，该协议在Taghdiri的硕士论文[ 26 ]中进行了分析又一次，C口头能够找到一个攻击。为了进行分析，必须开发CORAL其原因将在下文对案例研究的描述中阐明。在成功地建模和攻击这些协议时，我们给出了进一步证明了C口服方法;虽然运行时间通常是缓慢的，我们可以非常快速地使Horn子句模型适应新类型的协议。此外，发现的攻击明显长于Clark-Jacob语料库中通常发现的攻击[7]，以及CORAL之前发现的攻击[24]。要在这些设备上实现真正快速的攻击发现时间，协议，应该可以采用专门构建的协议分析工具，尽管可能需要大量的工作。我们在第5节中考察了这种可能性。本文的组织如下：在§2中，我们回顾了以前的工作组协议分析。 在第3节中，我们描述了第一个案例研究，关于Taghdiri和Jackson对Tanaka-Sato协议的改进版本。 关于Iolus协议的第二个案例研究见第4节。在整个案例研究中，我们强调了一些关于多播协议建模的一般性问题这些观点在第5节中进行了总结，我们在其中讨论了吸取的教训和有待解决的问题。第6段载有结论和进一步工作的计划。G. Steel，A.Bundy/Electronic Notes in Theoretical Computer Science 125（2005）1251272背景密码安全协议分析的领域现在太大了，无法在这里涵盖。最近的一项调查可以在[15]中找到在本节中，我们将简要回顾以前针对组协议分析的工作。也许第一个正式分析群体协议的人是保尔森。他研究了由Bull和Otway提出的递归认证协议，[6]，作为他发展归纳方法的一部分，[21]。保尔森能够在一般情况下，即任何数量的参与者，建立模型，并证明了一些安全性质的任意大小的群体。Paulson的方法使用了一种类型化的高阶逻辑形式，并将安全属性作为关于跟踪属性的描述。这些属性，然后证明了感应的痕迹互动定理证明Isabelle/HOL。然而，如果协议中有一个密码，PaulsonCORAL，[24]，已被用于发现在ad-hoc无线网络中建立密钥的Asokan-Ginzboorg协议上的攻击 CORAL使用Paulson协议模型的一阶版本，并搜索所考虑的安全属性的反例，即当协议被攻击时，它搜索攻击。推理是通过一个改编的版本来进行的一阶定理证明者SPASS，[29]，使用反驳完全CORAL直接搜索系统的无限模型，没有关于会话，角色，大小的参数化除了标准的包容和重言式检查，一小组特定于域的约简规则用于修剪搜索空间。归纳模型的使用使得Asokan-GinzboorgPereira和Quisquater通过人工分析程序发现了CLIQUES协议套件[3]上的几个重大攻击[22]。CLIQUES协议套件包含许多用于建立组和组内组的协议，每个协议都有自己的安全密钥。广泛使用的是Di Jade-Hellman式求幂，[10]。Pereira和Quisquater提出了一种方法，将入侵者获得特定项的问题转化为线性方程组的解。使用这种方法，他们能够找到他们检查的每个协议中的弱点。通常，攻击涉及入侵者相当富有想象力的行为，例如，被接受为大小为4的组的成员，然后使用在该密钥建立会话中学习的值来迫使大小为3的组使用他知道的密钥，以排除他一个明显的教训，128G. Steel，A.Bundy/Electronic Notes in Theoretical Computer Science 125（2005）125Pereira和Quisquater的工作是，这类协议的设计非常棘手。很容易理解为什么CLIQUES协议的设计者没有看到这样的攻击。这加强了在其设计中使用正式方法的情况。Meadows使用NRL协议分析器（NPA）来处理解释组（GDOI）协议套件，作为将形式化方法引入协议开发设计阶段的一部分。 GDOI是一种涉及可信密钥服务器的组密钥管理方法。NPA无法处理协议的一般模型所需的无限数据结构，因此对协议进行了具体的抽象，将第二阶段限制为一个“安全关联密钥”的分发。NPA能够在协议中找到一个类型定义，该定义在后来的GDOI版本中得到了固定。然而，MeadowsNPA被扩展到处理Di Jie-Hellman指数运算，但无法找到[22]中描述的攻击。协议规范语言CAPSL [9]的设计者最近在开发扩展语言MuCAPSL [17]时将注意力转向了组协议。在将GDH.2协议翻译成他们的中间语言MuCIL之后，他们能够发现一个类型的语法。然而，他们的分析需要提前设置组成员的数量，这可能会影响发现攻击的机会。HLSPL协议语言的设计者[23]也一直致力于将其覆盖范围扩展到组协议，尽管在撰写本文时Taghdiri和Jackson [27]报告了Tanaka和Sato [28]提出的多播密钥管理方案的建模结果该协议是为组高度动态的场景而设计的，即：代理频繁地加入和离开组。 我们的想法是尽量减少 通过按需向代理提供密钥来更新密钥。Taghdiri和Jackson用Alloy规范语言形式化了协议的模型，[12]并使用Alloy的SAT检查器来搜索协议理想属性的反例。发现了几个反例，其中最严重的一个表明，该集团的当前成员将接受该集团的前成员广播的有效消息。Taghdiri和Jack-son提出了一种改进的协议.然而，他们的正式协议模型与过去25年建立的规范不同，因为没有包括主动攻击者。在本文的其余部分，我们解释了我们如何建模和分析Taghdiri和JacksonG. Steel，A.Bundy/Electronic Notes in Theoretical Computer Science 125（2005）125129是安全的），[26]，使用我们的归纳反例发现工具，C口头。我们发现，这些协议在存在主动攻击者的情况下都不安全，即使他比自动协议分析中通常使用的Dolev-Yao入侵者更弱。3TheTanaka和Sato最初提出的协议[28]主要关注在网络传输和处理器时间方面最小化密钥更新的负担。为此目的引入了两个主要的设计特征：第一个是将组划分为子组，每个子组都在密钥分发服务器（KDS）的管理KDS之间的Taghdiri和Jackson [27]通过假设一个KDS更新其密钥，所有其他KDS立即更新其密钥，从而将模型有效地减少到单个服务器来对此进行建模。在我们的模型中，我们还将注意力限制在单个服务器上。该协议的第二个设计特征是代理保留一个密钥列表，而不仅仅是一个密钥。在接收到更新的密钥后，它们会在t个时间单位内将旧密钥作为无效密钥丢弃，其中t是根据网络中的延迟设置的。密钥仅在代理向服务器发送请求时分发。当一个代理想要发送一个多播消息，或者如果他收到一个用他不知道的密钥加密的消息时，他在这两种情况下，他都将向服务器发送一条消息，给出他拥有的最新密钥的ID号，服务器将发回所有较新的密钥。只有最新的密钥用于组播广播。在Taghdiri和Jackson的分析中，这种密钥列表的保留最严重的攻击涉及组成员接受组外主体的消息组A的成员可以简单地从组内部广播消息，离开，然后使用相同的密钥广播消息。虽然组密钥由于A的离开而被更新，但是组中的其他代理仍将接受第二条消息，因为它们都具有旧密钥。为了解决这个问题，Taghdiri和Jackson建议修改协议。每个代理应该只保留他收到的最新密钥，并且在收到多播消息时，应该联系服务器以确认它是根据最新密钥加密的。这可能会导致一些消息丢失，因为网络中的延迟可能意味着在收到组播消息并向服务器发送密钥请求时，组密钥已经更改，但与潜在的安全漏洞相比，这被认为是可以接受的。130G. Steel，A.Bundy/Electronic Notes in Theoretical Computer Science 125（2005）125它是我们使用CORAL建模和分析的协议的改进版本。这样做的目的是解决Taghdiri-Jackson分析的一个主要疏忽，即在他们的模型中缺乏主动入侵者。自第一篇安全协议论文以来，就一直假设有某种类型的主动入侵者[20]。他的行为被Dolev和Yao正式化，[11]，从那时起，人们普遍认为间谍也应该能够冒充合法的代理人，例如在Lowe着名的攻击中如果有的话，与单播协议相比，多播协议似乎更有可能受到主动入侵者的攻击，如[18]所述。拦截交易的机会本来就更多，而且主体的因此，这些协议应该在完整的Dolev-Yao攻击者模型下进行分析，这是单播协议的标准。Tanaka-Sato协议假设存在单播认证协议，该协议允许服务器与加入组的新成员建立单独的密钥（IK）。此IK用于加密该成员与服务器之间的所有通信。我们建模的基础认证协议，假设存在一个长期的密钥与KDS组的每个有效的潜在成员共享。由于我们正在寻找对协议的攻击，而不是试图验证它，我们可以很容易地证明这一点。我们可以简单地采取我们发现的攻击并检查它们，看看我们实现身份验证阶段的特定方式是否被利用。本文所描述的攻击对任何初始认证协议都是有效的。此外，我们做了一个标准的假设，即间谍可以访问一个有效的长期密钥。以下是Taghdiri和Jackson所描述的协议的改进版本的描述，并在本文中建模加入本集团1.Mi→S： {|加入我们|KMi2.S→Mi： {|IkMi，Gk（n）}|KMi在消息1中，Mi想要加入组，因此在他的长期密钥KMi下发送加入请求。服务器生成新的个体密钥Ik M1和新的组密钥Gk（n）。每个组密钥都有一个唯一的ID号（n）。新的个人密钥和组密钥在消息2中被发送到加入成员。离开本集团G. Steel，A.Bundy/Electronic Notes in Theoretical Computer Science 125（2005）1251311.Mi→S：{1}|{\fn黑体\fs19\bord1\shad1\1cHD8AFAF\4cHC08000\b0}|IkM2.S→Mi：{1}|{\fn黑体\fs22\bord1\shad0\3aHBE\4aH00\fscx67\fscy66\2cHFFFFFF\3cH808080}|IkM在消息1中，Mi发送请求以在其个人密钥Ik下离开加密。服务器确认消息2中的离开，并生成新的组密钥。新的组密钥还没有分发。事实上，如果在收到对密钥的请求之前发生了另一次成员关系更改，则永远不会分发该密钥。发送消息1.Mi→史：{|发送，n}|IkM我2.S3.Mi→→我：- 你好{|nJ，Gk（nJ）}|IkMi{|我的年龄}|G k（nJ）在消息1中，代理Mi向服务器发信号，表示他想通过发送协议设计者称之为服务器检查Mi是否在组中，然后发回最新的密钥Gk（nJ）。 如果没有加入J或者自从Mi最后一次接收到密钥以来已经发生了离开，则可能是n=n，但一般情况下并非如此。在消息3中，代理Mi向组广播他的消息。接收消息1.Mj→S： {|读取，n}|IkM2.S→Mj： {|G k（nJ）}|Ik假设多播消息已经被广播，如在上面的“发送消息”片段的消息3当另一个代理Mj接收到消息时，他首先向服务器发送一个请求，以获得最新的密钥。 然后，他接收最新的密钥Gk（n，J），并且将仅接受在该密钥下加密的多播消息。评注由Taghdiri和Jackson提出的修订后的协议包含一些作为其安全改进的结果的重新定义。例如，服务器没有理由在新成员加入时将密钥发送给他，因为每当他发送或接收多播消息时，他都需要请求密钥更新。此外，在发送消息之前在密钥更新请求中发送的序列号似乎也是多余的。我我JMJ132G. Steel，A.Bundy/Electronic Notes in Theoretical Computer Science 125（2005）125此前，G. Steel，A.Bundy/Electronic Notes in Theoretical Computer Science 125（2005）125133服务器将使用它来决定发送回哪些密钥，但是在修订版本中，服务器仅发送回最新的密钥。最好用一个随机数来代替它，正如我们在第3.2节中介绍我们发现的攻击后所论证的那样。3.1C语言建模CORAL我们通过使用排序的签名，用一元函数作为排序约束，在消息元素上强制强类型。协议被建模为所有可能的踪迹的集合，即在协议的指定下由任何数量的诚实用户发送的所有可能的消息序列，以及入侵者发送的伪造消息。消息的跟踪被建模为列表。Horn子句定义了如何由协议指定的诚实代理扩展有效的跟踪进一步的子句使用Paulson使用的相同的合成和分析操作符，对入侵者可以从跟踪中以前的消息中学习的知识进行为了寻找攻击，我们提出了关于安全属性的假设，就像Paulson所做的那样。CORAL然后搜索反例，例如通过向后搜索，即，它从违反安全属性的状态向后进行，我们的模型和CORAL操作的更多细节可参见[24]。我们的模型的一个特点是，所有关于系统状态的信息，即所有相关主体的状态和知识，都存储在跟踪中，并在每次需要时从跟踪中推断出来。然后可以使用一阶规则在单个瞬间向跟踪添加任意数量的消息。这在我们对Asokan-Ginzboorg组密钥协商协议建模时特别有用然而，对于Taghdiri-Jackson协议，这并没有那么有帮助。有关系统状态的某些信息通常不会出现在跟踪中。例如，当代理离开组时，服务器会生成一个新的密钥，但该密钥不会出现在跟踪中。此外，我们的模型遵循Paulson跟踪中的唯一事件是“发送”事件，并且在Dolev-Yao攻击者存在的情况下，这些消息可能永远不会被其预期的收件人接收到。这使得很难确定在特定时间谁是合法的组，这在建模控制条件时至关重要，即诚实代理在发送协议消息之前应用的测试。即使使用134G. Steel，A.Bundy/Electronic Notes in Theoretical Computer Science 125（2005）125造成了巨大的搜索问题。因此，模型被更改为包含有关主体状态的一些信息。以前用于存储消息跟踪的一元函数m（）现在是一个arity 4函数，用于存储跟踪、计数器、服务器存储的当前组密钥以及存储为三元组列表的组的组成。三元组存储代理名称、他与服务器共享的用于组中的该会话的个体密钥以及他已经接收的最近的组多播密钥。我们在这些三元组列表上定义了一个布尔函数ingroup，它确定特定的代理是否在组中。另一个变化是我们的新鲜度模型。我们曾经使用Paulson使用的parts操作符，但在我们的协议模型中，我们有一个计数器，并使用它来模拟新鲜值。我们这样做的动机是，在一个典型的场景中，必须为单个密钥、组密钥和多播消息创建如此多的新值，以至于我们对部件字面量的检查会很快减慢搜索过程。我们将多播消息建模为hello（T），其中T是消息发送时的计数器值，从而确保所有（诚实发送的）消息都是唯一的。在选择使用基于计数器的模型之后，我们向CORAL引入了一个新的修剪规则：如果计数器变量出现在先行字面值ingroup（X， Y， Z）=true内部的项X中，则该子句是冗余的，因为这需要代理在过去的某个时间点加入组并获得现在才可用的组密钥或单个密钥。类似的检查也适用于member（X， Y）=true文字。这从搜索中消除了许多不可到达的状态。这个规则通常可以应用于使用基于刻度的模型的向后搜索工具。作为示例，在图1中，我们给出了为发送多播消息的子协议建模所需的条款。请注意，在[24]中使用的原始模型的进一步变化中，我们在发送的构造函数的第四个参数中记录每个时间点的组的组成这对于后面讨论安全属性很重要。还要注意，ingroup是arity 3函数，第三个参数返回组成员列表，而第一个参数中没有指定的agent。 这在代理离开组或更新其密钥时使用，如 图1中的第三条。需要注意的另一点是，我们仍然从跟踪中推断出有关主体的状态信息，例如，以决定它们是否应该在第三个子句中期待密钥更新消息。我们的新模型是保尔森风格的跟踪模型和基于状态的模型之间的混合，例如，在[4]中使用。G. Steel，A.Bundy/Electronic Notes in Theoretical Computer Science 125（2005）125135%%发送消息m（Trace，Group，Keysequence，Tick）=true∧ingroup（triple（principal（Mi），Ikey，key（Sq）），Group，Newgp）=true→m（cons（sent（Mi，server，encr（send（Sq），Ikey），Group），Trace），Group，Keysequence，s（Tick））=true%%服务器提供密钥m（Trace，Group，Keysequence，Tick）=true删除组（三元组（principal（Mi），Ikey，Oldk），Group，Newgp）=true删除成员（sent（X，server，encr（send（Sq），Ikey），Tgroup），Trace）=true→m（cons（sent（server，Mi，encr（pair（key（Keysequence），send（Sq）），Ikey），group），Trace），Group，Keysequence，s（Tick））=true%%代理广播他的消息，更新他的密钥 m（Trace，Group，Keysequence，Tick）=true代理组（三重（principal（Mi），Ikey，Oldk），Group，Newgp）=true代理成员（sent（X，Mi，encr（pair（key（Xk），send（Sq）），Ikey），Tg1），Trace）=true代理成员（sent（Mi，server，encr（send（Sq），Ikey），Tg2），Trace）=true→m（cons（sent（Mi，all，encr（hello（s（Tick）），key（Xk）），cons（triple（principal（Mi），Ikey，key（Xk）），Newgp）），Trace），cons（triple（principal（Mi），Ikey，key（Xk）），Newgp），Keysequence，s（Tick））=trueFig. 1. 用于对“发送”子协议进行建模的条款3.2攻击协议在[22]中，Pereira和Quisquater试图为组协议列出一个理想的安全属性列表他们定义了隐式密钥认证，即局外人无法获知组密钥;两种完全前向保密性，即长期密钥的妥协不会危及过去的会话密钥;以及抵抗已知密钥攻击，即。会话密钥的泄露不会导致未来会话密钥的丢失。然而，Taghdiri和Jackson发现原始方案设计不满足的特性不在此分类范围内。从本质上讲，这是因为我们正在分析一个协议，用于管理一个不断发展的组的组密钥，而不仅仅是为一个静态组建立一个密钥。对密钥管理协议至关重要的属性是，在组的整个演化过程中，组内的代理不应将当前在组外的代理视为组成员。我们也许可以称之为多播组真实性。对于这个协议，这个属性有两个优点：第一个，Taghdiri和Jackson称之为“局外人无法读取”，意味着组外的任何代理都不能读取组成员发送的消息。第二种，他们称之为136G. Steel，A.Bundy/Electronic Notes in Theoretical Computer Science 125（2005）125这意味着组的成员不应该接受从组外部发送的有效消息。在归纳形式主义中提出安全假设需要一些思考。我们必须将真实性的抽象概念转换为用跟踪中的消息表示的属性。对于组协议属性，我们的跟踪包括组在每个点的组成，这一点现在变得很重要。对于属性因此，我们以这种形式将该属性作为猜想提交给CORAL%对于诚实的代理Mjeqagent（Mj，spy）=false ∧%有一个跟踪包含的序列Mj广播到Gk下的组的消息%m（cons（sent（Mj，all，encr（hello（Y），Gk），Xgroup），cons（sent（X，Mj，encr（pair（Gk，send（Sq2）），Ikey），Xgroup），cons（sent（Mj，server，encr（send（Sq2），Ikey），Xgroup），Trace）），Group，Keyseq，Tick）=true%且间谍不在组中inggroup（triple（principal（spy），X3，X2），Xgroup，Newgp）=false∧%但间谍有密钥Gkin（Gk，analz（Trace））=true→这个猜想是否定的，也就是说，不应该有跟踪Trace以第一个文字中指定的3个消息结束，间谍在组外，并且消息hello（y）是在间谍知道的密钥下发送的（analz（X）是间谍可以从跟踪X中学习的术语集）。这三个最终消息必须一起指定，因为否则CORAL（正确地）发现一个相当微不足道的攻击，即间谍在服务器向Mj发送密钥更新和Mj广播他的消息之间离开组。这样他就可以合法地阅读消息，因为消息发送时他就在组中。鉴于上述猜想，CORAL给出了图2中的反例。 这是对协议的攻击，它依赖于间谍在消息13中发送重放的密钥更新消息。由于密钥自她最后一次看到它以来可能已更改，也可能未更改，因此代理a将接受此密钥。问题在于，在密钥请求中发送的新鲜度信息最少（只有代理当前持有的密钥的序列号）。 包围在发送到请求密钥更新的服务器的包内的新的随机数将减弱这种攻击。在发现这种攻击后，我们意识到，G. Steel，A.Bundy/Electronic Notes in Theoretical Computer Science 125（2005）1251371.间谍→伺服器： {| 间谍|longtermK（spy）2.服务器→间谍：{| ik（1），Gk（1）}|longtermK（spy）3.一→伺服器： {| a}|longtermK（a）4.服务器→a：{| ik（3），Gk（2）}|longtermK（a）5.间谍→伺服器： {| （1）|（1）6.服务器→间谍：{| G k（2），send（1）}|（1）7.一→伺服器： {| sendd（2）}|中国（3）8.服务器→a：{| G k（2），send（2）}|中国（3）9.一→所有：{| {}{}|G k（2）10.间谍→伺服器： {| {\fn黑体\fs19\bord1\shad1\1cHD8AFAF\4cHC08000\b0}|（1）11.服务器→间谍：{| ackleave}|（1）12.一→伺服器： {| sendd（2）}|中国（3）13.间谍→a：{| G k（2），send（2）}|中国（3）14.一→所有：{| （14）}|G k（2）图二.第一次攻击田中-佐藤/塔赫迪里-杰克逊议定书由此，间谍可以从组外部发送消息，并使其被组内部的代理接受，从而破坏了多播组真实性属性，即我们给了CORAL一个适当的猜想以供证实，它发现了图3中的反例。与之前的攻击一样，这也是一次重放攻138G. Steel，A.Bundy/Electronic Notes in Theoretical Computer Science 125（2005）125击，在这种情况下，间谍重放消息13中的消息8，欺骗代理a认为消息11来自该组的合法成员。重放攻击通常在组密钥管理协议的上下文中更为严重。对标准单播协议的重放攻击通常假设间谍可以通过密码分析或其他方式获得短期密钥，因此如果他能够迫使代理接受旧密钥，则会构成对协议的攻击。在上述两种攻击中，由于间谍可以通过合法加入组来获得一些旧密钥，然后在实施攻击之前离开，因此不需要进行密码分析。然而，即使我们假设间谍无法访问有效的长期密钥，因此无法加入组，这些重放攻击仍然是危险的。如果间谍通过密码分析获得短期组密钥，他可以在不加入组的情况下进行攻击G. Steel，A.Bundy/Electronic Notes in Theoretical Computer Science 125（2005）1251391.一→伺服器： {| a}|longtermK（a）2.服务器→a：{| ik（1），Gk（1）}|longtermK（a）3.间谍→伺服器： {| 间谍|longtermK（spy）4.服务器→间谍：{| ik（3），Gk（2）}|longtermK（spy）5.间谍→伺服器： {| read}|中国（3）6.服务器→间谍：{| G k（2）}|中国（3）7.一→伺服器： {| read}|（1）8.服务器→a：{| G k（2）}|（1）9.间谍→伺服器： {| {\fn黑体\fs19\bord1\shad1\1cHD8AFAF\4cHC08000\b0}|中国（3）10.服务器→间谍：{| ackleave}|中国（3）11.间谍→所有：{| （12）}|G k（2）12.一→伺服器： {| read}|（1）13.间谍→a：{| G k（2）}|（1）图三.对《田中-佐藤/塔赫迪里-杰克逊议定书》的第二次攻击也可以通过向密钥请求添加新的nonce来防止，这次是用于读取消息，并将其包含在来自服务器的协议模型文件的完整列表可在http://homepages.inf.ed.ac.uk/s9808756/tanaka-sato/网站。4Iolus协议Iolus协议与Tanaka-Sato协议的Taghdiri-Jackson版本之间的主要区别在于Iolus急切地分发新密钥，而Tanaka-Sato仅按需分发密钥，即，当组的用140G. Steel，A.Bundy/Electronic Notes in Theoretical Computer Science 125（2005）125户想要发送或读取消息时。加入本集团1.Mi→S： {|加入我们|KMi2.S→Mi： {|IkMi，GknJ}|KMi3.S→ALL： {|GknJ}|GKN成员以与Tanaka-Sato相同的方式加入Iolus协议，即通过使用成对认证协议，我们使用G. Steel，A.Bundy/Electronic Notes in Theoretical Computer Science 125（2005）125141J长期钥匙服务器生成新的个体密钥IkM i和具有IDn的新的组密钥GknJ。在消息2中，组密钥被发送给新成员，并且在消息3中，组密钥被发送给在旧组密钥Gkn下的组的旧成员。离开本集团1.Mi→S： {|{\fn黑体\fs19\bord1\shad1\1cHD8AFAF\4cHC08000\b0}|IkM2.S→ALL： [{|Gk nJ}|IkMi，Mj∈群. . . ]j/=当成员Mi离开时，生成新的密钥GknJ，并以广播列表的形式发送给每个成员。该列表包含新的组密钥，该新的组密钥是在仍在组中的每个成员的成对会话密钥下加密的（该密钥不能在旧的组密钥下广播，因为这会将其泄露给离开的成员）。发送消息1.Mi→ALL： {|我的年龄}|G k（n）消息只是在当前组密钥下广播。4.1造型Iolus不需要改变C口服模型的框架来正式确定Iolus方案。虽然该协议分发新的密钥急切，而不是懒惰，操作是类似的Tanaka-Sato协议中使用的。模型中最复杂的部分涉及“leave”子协议的第二条消息。在这里，我们必须为任意组生成适当的密钥更新列表建模。 在我们的一阶模型中，这是一个简单的任务。我们定义了一个递归函数rekey，它为给定的组和给定的新组密钥生成适当的密钥更新消息。这个函数在所有的实例化模式下都能正常工作，也就是说，给定一个rekeying消息，它将返回一个合适的组和键。 这在我们的反向搜索过程中很重要。辅助rekey函数的使用类似于我们在Asokan-Ginzboorg协议模型中使用的allmsg 2s received函数，[ 24 ]。 能够进行这种递归计算似乎（也许并不令人惊讶）在建模组协议时很重要，我们的一阶逻辑模型非常适合它们。我J142G. Steel，A.Bundy/Electronic Notes in Theoretical Computer Science 125（2005）1254.2攻击Iolus在为上述Tanaka-Sato/Taghdiri-Jackson协议提出了安全性假设之后，为Iolus协议制定一个适当的猜想就更容易了。同样，我们正在研究多播组的真实性，即组外的人不能成功地冒充组内的人，无论是通过发送或接收消息。然而，由于密钥是容易提供的，因此我们没有将此属性划分为“外部无法读取”和“外部无法发送”。相反，我们必须考虑更新密钥的可能方法。期望的属性是：当组的成员接受对密钥Gk的密钥更新时，并且该组不包含间谍，则间谍不应该知道密钥Gk。我们针对组成员离开后发送的更新来制定此属性，如下所示：%对于诚实的代理Mjeqagent（Mj，spy）=false ∧%Mj接受密钥Gkm（cons（sent（X，all，cons（encr（Gk，Ikey），Rest），cons（triple（Mj，Ikey，OldGk），Restgp）），Trace），Group，Xk，Tick）=true%间谍不在组ingroup（triple（principal（spy），Y，Z），Restgp，Newgp）=false∧%但是他知道钥匙in（Gk，analz（Trace））=true→同样，这是一个否定的猜想，表明为了使协议安全，当间谍在组外时，不应该存在间谍知道组成员Mj接受的密钥Gk的CORAL在图4-4中找到了反例。这又是一次重放攻击。在消息14中，间谍重放最初在消息11中发送的密钥更新，而他仍然在组中。因此，间谍知道组密钥Gk（4），即使他不再是组成员。 注意，要使这种攻击起作用，需要两个诚实的代理人在此之前的几次攻击中，只需要一个人就可以加入该组织和间谍，并进一步注意到，CORAL自己已经发现了这一点-没有预先设置特工的数量。防止这种攻击并不像Tanaka-Sato/Taghdiri-Jackson协议那样简单，因为密钥更新是主动提供的，因此代理和服务器没有机会交换随机数。防止重放的唯一方法似乎是在加密包中包含时间戳[4]在CORALG. Steel，A.Bundy/Electronic Notes in Theoretical Computer Science 125（2005）1251431.一→伺服器： {| a}|longtermK（a）2.服务器→所有：{| G k（1）|G k（X8）3.服务器→a：{| ik（2），Gk（1）}|longtermK（a）4.间谍→伺服器： {| 间谍|longtermK（spy）5.服务器→所有：{| G k（2）}|G k（1）6.服务器→间谍：{| ik（5），Gk（2）}|longtermK（spy）7.s（a）→伺服器： {| s（a）}|longtermK（s（a））8.服务器→所有：{| G k（3）}|G k（2）9.服务器→s（a）： {| ik（8），Gk（3）}|longtermK（s（a））10.一→伺服器： {| {\fn黑体\fs19\bord1\shad1\1cHD8AFAF\4cHC08000\b0}|中国（2）11.服务器→所有：[英|G k（4）|i k（8），{|G k（4）|（5）]12.间谍→伺服器： {| {\fn黑体\fs19\bord1\shad1\1cHD8AFAF\4cHC08000\b0}|中国（5）13.服务器→所有：[英|（5）|（八）]14.间谍→所有：[英|G k（4）|i k（8），{|G k（4）|（5）]见图4。 对Iolus协议的在代理加入和离开组时发送密钥更新。这将要求所有组成员具有至少松散同步的时钟，并且还需要提前决定组密钥的寿命和网络中的预期延迟144G. Steel，A.Bundy/Electronic Notes in Theoretical Computer Science 125（2005）125量。然而，这种限制似乎是不可避免的，这样的协议。例如，在Dolev-Yao间谍存在的情况下，将密钥更新消息中的最后一个密钥作为新鲜度信息是不足够的，因为间谍可能会阻止该消息被接收，然后一旦他离开组就重新发送该消息Iolus协议模型文件的完整列表可在http://homepages.inf.ed.ac.uk/s9808756/iolus/网站。5案例研究在这些案例研究中，我们看到了第一个安全协议的设计者在新协议中重新出现的过度关注。 正如我们在§3.2，像我们发现的重放攻击在多播密钥管理协议的上下文，甚至不需要