缺陷安全协议的修补方法及测试研究

理论计算机科学电子笔记174（2007）117-130www.elsevier.com/locate/entcs一种在缺陷安全协议中修补交错重放攻击的方法1.胡安·卡洛斯·洛佩兹·皮门特尔和劳尔·蒙罗伊计算机科学系TecnolgicodeMonterrey，CampusEstadodeMexicoC ar reteraallagodeGuadalupe，Km3. 5，Atizapan，52926，Mexico{juan.pimentel，raulm}@ itesm.mx迪特尔·哈特DFKI，SaarbruckenUniversityStuhlsatzenhausweg3，D-66123Saarbrucken，Germanyhutter@dfki.de摘要式安全协议的验证在形式方法界引起了很大的兴趣，产生了两种主要的验证方法：i）状态探索，例如PDR [8]和OFMC [2]; ii）理论证明，例如Isabelle归纳法[12]和CORAL[13]。 Abadi和Needham的原则是对正式方法的补充我们感兴趣的是一个与验证有关但尚未探讨的问题：错误安全协议的纠正。经验表明，对反例的分析或失败的证明尝试往往掌握着完成证明和纠正错误模型的关键...... 在本文中，我们介绍了一种修补易受攻击的缺陷安全协议的方法。这是一个交错重播的攻击。我们的方法使用了Abadi和Needham的密码协议的谨慎工程实践原则，以指导协议中错误的位置，以及候选补丁的建议。[10]我们已经对我们的方法进行了测试，结果令人鼓舞。测试集包括从Clark-Jacob库借用的21个故障安全协议[5]。关键词：故障定位、修补、重放攻击、安全协议、验证......1介绍性计算机安全是IT部门最关心的问题用户不愿意在不安全的、敌对的网络上传递他们的机密信息。[10]计算机犯罪已经造成了无法计算的损失。为了确保安全性，用户使用协议。安全协议是一组规则和惯例，其中一个或多个代理人相互之间存在分歧1我们感谢Alan Bundy、Graham Steel和审稿人对本文早期草稿的有用评论。本文报告的研究得到了ITESMCCEM-0302-05的支持。1571-0661 © 2007由Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2006.12.034118J.C.L. Pimentel等人。理论计算机科学电子笔记174（2007）117身份，通常以拥有一个或多个秘密而告终[12]。安全协议只包含几个消息，但令人惊 讶 的 是 ， 它 们 很 难 正 确 。 例 如 ， 在 3-message Needham-Schroeder 公 钥（NSPK）协议中检测到漏洞需要17年[7]。安全协议的验证在正式方法界引起了很大的兴趣，产生了两种主要的验证方法：（i）状态探索，（ii）状态探索，（iii）状态探索。例如 罗斯福[8] 和OFMC [2];以及 ii） 定理 证明，例 如伊莎 贝尔归 纳法[12] 和CORAL[13]。模型检查工具能够确定一个协议（一个协议的有限抽象）是否是有效的。验证过程通常需要几秒钟的时间，在不可靠的情况下，会输出一个反示例（协议攻击）。定理证明可能是缓慢的，但有一个广泛的应用范围，如[13]所示。作为对正式方法的补充，阿巴迪和李约瑟的Abadi和Needham通过通知一些难以在协议中分析的共同特征来达到他们的原则。如果避免了这些功能，协议往往会变得更容易阅读，更重要的是，更正确。我们感兴趣的是一个与验证有关但尚未探讨的问题：错误安全协议的纠正。一个有缺陷的协议是一个错误的表述。错误的表述是理论重构的核心。他们经常通过一个失败的证明尝试的出现而变得明显，可能会产生一个反例。对这一证据的分析往往掌握着完成证明和纠正错误模型的关键......故障安全协议的纠正需要开发一套能够处理一般类型的故障的修补方法，这是一个很好的解决方案。在本文中，我们介绍了一种修补有趣的一类故障安全协议的方法，我们已经利用了这种方法进行了交错-重放攻击。重放攻击是网络攻击的一种形式，其中有效的数据传输被恶意地或欺骗性地重放或延迟。[2]根据Paul Syverson的粗略地说，为了导出我们的修补方法，有必要遵循完整的验证周期（第2节）。此循环主要涉及三个阶段：i）验证故障安全协议并获取其反例; ii）通过修补框架修补故障安全协议;以及iii）验证最新版本的协议。我们修补方法的关键在于第二阶段），这取决于阿巴迪和李约瑟关于这些原则被应用于指导协议中缺陷的位置，就像候选补丁程序的 建议 为了自动修补缺陷安全协议，我们的方法首先按 照toidntifytheroleplayedbyalcomponetsofeachmessage的顺序分析协议描述（第4节）。Then，它分析了在阶段i）中获得的协议反例，以便识别2http://en.wikipedia.org/wiki/Replay攻击J.C.L. Pimentel等人。理论计算机科学电子笔记174（2007）117119在其运行中共享的非平凡消息部分，并使用启发式，它分析这些观察结果，以便诊断可能的故障并建议候选修补程序（第5节）。我们还介绍了在我们的修补方法的发明中使用的方法（第6节）。最后，我们对我们的方法进行了测试，结果令人鼓舞（第7节）。测试集包括从Clark-Jacob库借用的21个故障安全协议[5]。此外，我们还报告了使用AVISPA工具验证第iii）阶段的大量结果。2一个完整的验证周期一个完整的验证周期将有助于安全协议设计人员创建最佳的安全协议，从而降低实施后的风险。[10][11]该循环由三个阶段组成。在第一阶段，我们将使用模型检查器或定理提供程序来检查反测试示例，以说明安全协议是错误的。 结果，我们得到了（一般来说）几个协议运行的交织，这些协议运行违反了在模型检查器或理论提供程序的规范中建模的安全要求。在第二阶段，我们必须通过一个修补框架来修补缺陷安全协议此修补框架是一组能够处理一般类型的错误的修补方法。[10]每个修补方法都具有图1中所示的形式（名称、输入、前提条件、流等）。打补丁的方法可以分为两个步骤。第一个步骤是找出那些会导致协议失败的协议消息，这是一个很好的解决方案。我们的修补方法，对于实例，对thecounterexample，usingtheroleplayedbyalcomponentsofeachmessage进行了有趣的观察。我们分析了针对这些情况的各种协议，并将其形式化为所谓问题位置的前提条件。在第5节中，我们将重点介绍一个特殊的例子（NSPK协议），其中委托人的身份对于协议的安全性至关重要。违反这一原则的行为可以在协议跟踪的技术层面上观察到，事实上，在一个协议运行中（在某种意义上）保密的消息部分在一秒钟内就被重复使用了。在修补框架的第二步中，我们必须更改协议，以便避免特定的错误。因此，我们将使用问题位置的这种技术描述作为解决这种冲突的特定规则的先决条件。在这些前提条件下，该方法具有一个缺陷部分，该缺陷部分由对其试图修复的缺陷的详细描述组成，以及一个将要对协议进行的更改形式化的部分（补丁）。变化，在错误的信息，仍然在阿巴迪和李约瑟的在我们的修补方法中，对于实例，原则3建议了解决方案：我们在错误消息部分中引入代理名，以消除消息部分可能发生的上下文的歧义。其结果是，在两个协议运行中都不能再使用已修改的消息。在完整验证周期的第三阶段，我们必须验证协议的新版本，以便了解安全协议在哪些方面是无漏洞的，或者在哪些方面是无漏洞的。120J.C.L. Pimentel等人。理论计算机科学电子笔记174（2007）117在最坏的情况下，不再容易受到同样的反例。对于这一点，我们必须再次使用模型检查器或定理证明。在本文中，我们特别使用了AVISPA工具（一种模型检查器）来处理完整验证周期的第一阶段和第三阶段。在下面的章节中，我们将更详细地解释一种修补交错-重放攻击的方法。3阿巴迪和李约瑟Abadi和Needham的它们涉及两个主要问题：（i）协议中涉及的消息及其内容;以及（ii）由参与者维持的信任关系。原则1：处理协议消息及其内容：每个消息都应该说它的意思，对消息的解释应该完全取决于它的内容。它包含原则3-10。原则3，命名，规定与消息相关的代理名称都应该可以从已经应用的加密密钥或其他数据中推导出来，包括代理名称的明确提及，或者可以从已经应用的加密密钥或其他数据中推导出来。原则4，加密，是正确使用加密的指导方针;它规定了为什么加密被破解是明确的（它是为了提供真实性而完成的吗？）还是保密性？）。原则5，签名（加密）数据，规定签名的外观并不一定意味着签名代理知道消息的内容，这是一个很好的解决方案，也是一个很好的解决方案。原则10，编码，规定对消息格式要谨慎：委托人应该能够从消息内容中关联，消息的步骤对应于他们正在运行的任何协议的步骤。[10]原则6-8是建立消息新鲜度和消息关联的指导原则。原则6规定要清楚地了解关于随机数所假定的属性;原则7规定要谨慎地使用可预测的随机数;原则8是对时间戳使用中谨慎实践最后，原则9规定要确定使用钥匙的可接受性反过来说，与参与者的信任关系的两个原则交易：应该明确地设置要执行的消息的条件，以便审查设计的人可以看到它们是否可以接受。 它包括原则11。信任关系引入了依赖性，例如，谁对会话密钥的生成是可信的？无论这些依赖关系是可接受的，都应该建立在政策而不是逻辑的基础上。34安全性协议正 如 [1] 所 指 出 的 ， 安 全 协 议 中 的 大 多 数 漏 洞 都 源 于 不 正 确 的useofcryptographicprimitives。 Aprotocoldesignermaymisstheroleplayed由消息组件或高估由加密消息提供的安全保证。我们目前正在发展一个理论，将允许我们identifytheoneortheseveralrolesplayedbyeachmessagecomponent。3因此，原则2和11在我们的机制中没有被用于纠正错误安全协议的目的。J.C.L. Pimentel等人。理论计算机科学电子笔记174（2007）117121Def=4.1基本成分：我们的方法使用了Paulson对代理人口和消息结构的形式化有三类代理：服务器代理、S代理、绝对可信的代理、友好的代理（A、B、......）。。和一个Dolev-Yao间谍，间谍。消息包括代理名、随机数、时间戳、共享密钥（在对称加密中使用）、公钥或私钥（在对称加密中使用）、公钥或私钥（在对称加密中使用）、公钥或私钥（在对称加密中使用）。和会话键。 符号{|X1，... ，Xn−1，Xn|}用于缩写com-pound消息MPairX1...（MPairXn−1Xn）。 符号Kab、Kas和Kbs表示特定的共享密钥;K+、K+和K+表示特定的公钥;K−表示特定的公钥。ABS AKb-和Ks-表示相应的私钥。符号Na、Nb和Nc表示随机数;Ta、Ib和Ts表示时间戳。 我们写了{|M|K表示您的在密钥K下对消息M进行加密。与Paulson不同的是，我们将协议指定为一系列步骤，每个步骤的形式为：n。A→B：M，意思是在步骤n中，A向B发送消息M，B接收到消息M。请注意，每个步骤都涉及两个通信事件：发送和接收关联消息的过程中的一个步骤。由多个并行协议运行组成的协议反例被指定为一系列会话步骤，其中每个步骤的形式都是S：n。[10] A→B：M，表示第n个会话S的步骤。4.2MessagePartsandtheirRolesAnagentmayplayoneoftworolesina protocol：initiato r orr是ponder。发起者是在协议中请求会话的代理，响应者是对该请求作出响应的任何代理。通常，启动器启动协议中的运行，因此：definitiator（P）发送方（P，1）Def响应（P）={r：Agent}|r/=发起人（P）？rS？r？参与者（P）其中参与者（P）（分别为发送者（P，n））返回协议P中的所有参与代理（分别为第n步的发送者）。我在一个protocol，eachmessagecomponetcar rriesouta specificicrole。有时候，通过合成分析可以找到一个消息组件，这是一个很好的例子。以下是[11]：Secret Distributor是一个带有秘密的加密消息。一个秘密是一个月的圣人，在协议执行期间从来没有明确地发送函数符号secretDist（P）用于表示协议P中所有秘密的集合;在符号中：secretDist（P）={{|M|K.|{|M|{K她家}{\displaystyleK}{\displaystylep}{\displaystyleP}在rts M中，m ≥p。 M1她家她家 有一个msgOf（P）。m她家g2set（M1）}122J.C.L. Pimentel等人。理论计算机科学电子笔记174（2007）117其中parts是Paulson对身份验证器是一个加密的消息组件，用于提供消息发送者的身份的J.C.L. Pimentel等人。理论计算机科学电子笔记174（2007）117123BABBA间谍AB间谍A正如下面所示，这些简单的概念允许我们对一个协议和它的一个反例进行有趣的观察。5一种用于修补交错-重放攻击的为了解释我们的修补机制背后的原因，我们将展示一个错误安全协议（称为NSPK协议）的示例修复程序：1 A→B：{|A、A|K+2B→A：{|NA，NB|K+3A→B：{|NB|K+NSPK协议乍看起来是对的，但这是错误的。 Lowe发现入侵者可以模仿一个代理同时与另一个代理进行会话[7]：1：1。A：间谍 ：{|A、A|K+s2：1。 间谍（A）→B：{|A、A|K+2：2。B→Sp和（A） ：{|NA，NB|K+：{|NA，NB|K+：{|NB|K+s2：3。 Spy（A）→B：{|NB|K+5.1故障检测系统;InLowe被欺骗的代理A是第一个跟踪的发起者，是消息2的两个实例的预期接收者，但是她不能区分是谁构建了它还是发送了它。因此，虽然B知道A最近在协议的某个运行中进行了部分启动，但他不能告诉A是否与他无关地运行它。在这次攻击中，间谍参与了一次交错重放攻击：在监视了一个协议的一个（可能是部分）运行后，他在另一个不同的协议运行中重放了一个或多个消息，模仿了一个友好的代理。正如我们所看到的，Interleave协议在执行中运行。如果通信代理不具有任何机制来区分谁发起了传入消息，或者该消息是针对谁的，或者不能将该消息与时间线相关联，则该消息将被拒绝。通常，间谍选择重播的消息包含一个或多个秘密分发者。因此，重播故障安全协议违反了阿巴迪和李约瑟的第三个打印机，S1：2。间谍→→AS1：3。A→→间谍124J.C.L. Pimentel等人。理论计算机科学电子笔记174（2007）117BAB输入：协议P，反例C前提条件（问题位置：）{|M |K她家（P）↑tr1Dreams（C）↑tr2Dreams（C）↑tr1/=tr22：n2. AJ→BJ：m2她家她家2|M|{K她家}{\displaystyleK}{\displaystyle K}{\displaystyle K}{{\displaystyle K}}T1：N1。 A→B：m1她家她家3|M|K她家rtsmsg2set（m1）缺陷：协议可能违反了阿巴迪·李约瑟的在M中省略了发起人或响应者电子邮件（Patch：）对于协议中的每一步，n。A→ B：m，（initiator（P）她家/msg2set（M）她家/msg2Set（M））在哪里{|M |{K}部分msg 2set（m），如第5.2节A和B中所述，将M相加形成MJ，然后用m中的MJ替换M。原则3：如果委托人的身份对消息的含义至关重要，那么在消息中明确提及委托人的姓名是明智的。通过添加发送消息2的代理的名称来修补协议，在本例中为B，如第三个原则所建议的，我们得到了Lowe已经找到的修复[8]：1 A→B：{|A、A|K+2B→A：{|B、 NA、 NB|K+3A→B：{|NB|K+我们修补重放错误安全协议的方法如图1所示。[10]它是一个4-元组，由输入信息、前提条件、流和函数组成。该方法是可应用的，如果该方法的前提条件成立，考虑输入协议和它的一个反例。前提条件指定了协议或反例中任一项的属性。它们以元逻辑的形式表达，涉及第4节中介绍的符号。该漏洞包括对设计原则的非正式描述，该协议被认为违反了该原则。E-ECTS规定了修改协议的具体方式，具体如下：在最坏的情况下，期望协议的较新版本不再易受交错重放攻击的影响，并且在理想的情况下，期望协议的较新版本健壮地足以在任何攻击中生存。图1。一种交错-重放修补方法。5.2斑块形成[编辑]在我们的方法中，修补交错重放错误协议导致将代理名添加到一组秘密分发程序中。然而，这一增加的过程试图避免冗余的引入和混乱的引入......J.C.L. Pimentel等人。理论计算机科学电子笔记174（2007）117125A有时，参与者代理的名称可以在加密消息中从加密因此，为了避免引入冗余，我们应用了加密技术的以下众所周知的结果：[10][11]不对称密码学中的真实性：在Kb下加密的任何消息-最初来自B，只要B不被泄露。不对称加密中的机密性：在K+下加密的任何消息只能由A使用他的私有ke和Ka−解密（只要A不被泄露）。对称加密中的真实性：A在与可信服务器K共享的长期密钥下接收到的任何加密内容，最初来自服务器，只要A没有发送它。这类似地适用于A和交换的服务器。为了避免消息混淆，我们将返回到协议描述中。我们需要确保新的消息组件，或者甚至整个新消息都没有与协议中的另一个组件类似的结构。如果出现潜在的消息混淆，我们将使用一些顺序输入所有名称，例如：发送方优先，然后响应，参见表2中的CCITT X.509（3）协议。6发展方法学我们现在概述了在我们的修补方法的发明中使用的方法。首先，我们区分了两组故障安全协议：......开发：这个类由几个协议示例组成，这些协议示例将用于设计修补方法。为了使这一点有意义，开发错误协议必须具有相似的缺陷（至少受到相同类型的攻击），并且它们应该在大小、使用的加密类型、参与者（是否涉及可信服务器）等方面有所不同。该方法在实现之前在开发集上进行了手动测试;测试：这个类包含用于测试方法的鲁棒性的示例协议，并且仅在开发完成时才考虑这些协议。测试集包括开发集，但也包含在开发过程中未使用的测试集的示例。其次，我们试图使开发协议示例尽可能地保持不相似性。第三，我们从不同的来源收集了一些例子，例如，书籍、研究报告等...和克拉克-雅各布图书馆，这已经成为最后的来源。[10]对于交错-重放修补机制，开发集仅包括四个协议，即：NSPK协议、宽嘴青蛙（WMF）协议、Denning-Sacco PK协议以及Otway-Rees协议的Abadi和Needham版本。126J.C.L. Pimentel等人。理论计算机科学电子笔记174（2007）117ID协议名称密码学类型攻击类型已修复1Andrew Secure RPC对称的CR2BAN混凝土ASRPC对称的IR√3CCITT X.509（1）（+）不对称的IR√4CCITT X.509（3）（+）不对称的IR√5Denning-Sacco SK对称的CR6Denning-Sacco PK不对称的IR√7Kao Chow Auth-V.1对称的CR8KSL对称的IR√9诺依曼·斯塔布尔宾对称的TF10NSPK（+）不对称的IR√11李约瑟·施罗德SK对称的CR12奥特威-里斯对称的TF13O R BAN版本对称的IR√14Splice/AS不对称的IR√15Hwang-Chen Splice/AS不对称的IR√16C-J改良Splice/AS不对称的CR17TMN对称的CR18WMF协议对称的IR√19Woo和Lam Mutual对称的IR√20Woo和Lam Pi（+）对称的TF21BAN Modified Yahalom对称的IR√表1验证测试集7结果一旦我们的方法修补了一个协议，它就需要知道协议的新版本在什么时候是无漏洞的，在最坏的情况下，它不再容易受到相同的交错重放攻击（完整验证周期的第三阶段）。为此，我们使用了AVISPA工具v.1.0（互联网安全协议和应用程序的自动验证）。4要在此工具中验证协议，必须用高级协议规范语言（HLPSL）来制定协议和要验证的属性（例如，保密性或/和身份验证）。然后，我们必须在四个后端搜索引擎之一上测试协议：飞行模型检查器（OFMC）、基于约束逻辑的攻击搜索器（CL-AtSe）、基于SAT的模型检查器（SATMC）和基于自动近似的安全协议分析树自动（TA 4SP）。前两个后端，OFMC [3]和CL-AtSe [15]，用于与完整验证周期的第一阶段和第三阶段相对应的实验性表1-5总结了我们的结果。表1包含我们的验证测试集。它由21个错误协议组成，借用自克拉克-雅各布图书馆。克拉克-雅各布图书馆包括50个协议，其中26个是已知的错误。因此，我们的验证测试集包含除五个已知故障安全协议外的所有协议。从我们的验证测试中遗留下来的错误协议中的漏洞与重放攻击没有任何关系。[10]4可通过http://www.avispa-project.org/J.C.L. Pimentel等人。理论计算机科学电子笔记174（2007）117127{||}||}在表1中，用（+）表示的协议旨在提供身份验证;保留的协议旨在实现身份验证和会话密钥分发两种功能。攻击类型用"IR"、"TF"和"CR"表示。 "IR"缩写词交错重播， 标记有√的协议已打补丁。 的修补版本的方案如表2-3所示。方案名称新的描述评论BAN混凝土ASRPC1.A→B：A、NaB =A：{|A、B、NA、KPAB|KabA →B：{|Na|KPAB4、B→A：Nb此补丁类似于Lowe在[9]中提出的补丁。CCITT X.509（1）1.A → B：A，{|T、N、A、B、Nxa、{|AN和A|K+|K-B A此修补程序类似于这是由Abadi和Needham在[1]中提出的。CCITT X.509（3）1.A → B：A，{|T、N、A、B、Nxa、{|AN和A|K+|K-B AB =A：B，{|T b、Nb、A、Na、Nxb、在这里，两个实验中的一个-这样的补丁被呈现。此修补程序类似于这是Burrows提出的，阿巴迪和李约瑟在[4]。{|A → B：A，{|A、B N和B|K + |K-A BBN B|K- ADenning-SaccoPK1.A→S：A，B+2.S→A：{|A、K、A、 T|K−，S+{|B、K、B、 T|K-S+A→B：{|A、K、A、 T|K−，S+{|B、K、B、 T|K −，S此修补程序与建议的修补程序相同Abadi-Needham在[1]。{|{|B、K AB， TA|K-|K+A B表2已修补协议描述，第一部分我们的方法能够在21个错误协议中的12个错误协议中识别出一个交错重放攻击和一个有趣的是，我们的实验表明，即使我们的修补方法在为相同的错误协议输入两个不同的计数器示例时建议了一个不同的候选修补程序，AVISPA工具中的验证在两个候选修补程序（协议4、13、18和19）中都成功完成。不能在我们的方法范围之外打补丁的协议;也就是说，它们不是交错重放错误的协 议 （ 见 下 文 ） 。 例 如 ， 根 据 Lowe 的 层 次 结 构 ， 协 议 5 和 16 缺 乏 响 应 者 的AlivenessLowe类型错误攻击是指代理没有机制来识别最初打算具有一种类型的字段，而该字段随后被解释为具有另一种类型的字段。例如，等待接收形式为A，Kab，TB KB的消息的代理接收消息A，Na，TBKB，在这种情况下，它通过密钥Kab天真地接受NonceNa。[6]根据Paul Syverson的分类法[ 14 ]，经典重播是一种攻击，不需要当代运行。经典的重播已经被识别出来，没有一个时间参考。128J.C.L. Pimentel等人。理论计算机科学电子笔记174（2007）117方案名称新的描述评论KSL1.A→B：Na，AB→S：Na、A、Nb、B此修补程序类似于Lowe在中提出的修补程序3.S→B：{|B、 N b、A、 Kab|KB，[9]。 而不是添加到{|Na、B、 Kab|}KAB→A：{|Na、B、 Kab|KA，{|B、A、Kab|KBB，Nc，{|Na|KabA →B：{|NC|KabA→ B：Nma，{|B、A、Kab| KBB的A：Nmb，{|NMA|Kab8.A→B：{|NMB|Kab响应name B，在这样一个秘密分发者中，Lowe将顺序更改为f或ll或w s：{|A、N、B、K、B|KB.这是同样的事情，第三步的秘密发行商。再给一个。NSPKA →B：{|Na，A|K+此补丁程序相同。B=A：{|BN A， N B|K+如所提议的那样A→B：{|NB|K+B在[7]中。O R BAN版本A→B：M，A，B，{|N A、M、A、B|卡B → S：M，A，B，{|N A、M、A、B|KA，NB，{|M、A、B|KB3.S→B：M，{|Na，K ab|卡，类似于CCITTX.509(3)协议我们的方法提出了两个不同的补丁在两个不同的补丁{|A、NB、K ab|KB反例（此处，A：M，{A：M}|Na，K ab|卡仅提供一个）。表3已修补的协议描述，第二部分它通过添加随机数握手来扩展协议。表2-4显示了我们的修补方法的输出。对于每个协议，它们都描述了新的规范。更改包括代理名，这些代理名包含在协议新描述中的框中。表5显示了用于验证新协议描述的总延迟验证时间（TEVT）和后端（OFMC或CL-Atse）。实验在配备1.6 GHz奔腾IV处理器和512 Mb RAM的PC上进行。8结论和进一步工作在本文中，我们提出了一种修补易受交错重放攻击影响的错误安全协议的方法。使用Abadi和Needham关于代理命名的指导，我们的机制通过将必要的名称添加到协议消息中来修补协议，这样它们就不能在没有通知的情况下再被重放。我们的机制提出的补丁是自然的，使错误识别和纠正过程看起来很漂亮，微不足道。然而，事实并非如此，因为这种类型的设计错误已经系统地出现在整个文献中，如表2最近易受交错重放攻击的错误协议的一个例子是Asokan-Ginzboorg协议，如[13]所示。我们已经进行了大量的实验来验证我们的方法。 例如，它已经在21个故障安全协议上进行了测试（从J.C.L. Pimentel等人。理论计算机科学电子笔记174（2007）117129方案名称新的描述评论Splice/ASC→Sa：C、S、N1C：Sa，{{}|S、Sa、C、N 1、K+|}SK-SaC→S：C，S，{|C，Tc，Lc，{|N2|K+|K-S C4.S→Sa：S、C、N35. S：S，{|C、Sa、S、N、3、K+|}CK−SaC：S，C，{{}|S，f 2（N 2）|K+C此修补程序成为Hwang-Chen版本Splice/as协议。虽然这个版本是Faulty，我们的方法也是修补它。请参阅以下内容行。Hwang-ChenSplice/ASC→Sa：C、S、N1C：Sa，{{}|Sa、C、N 1、S、K+|}SK-SaC→S：C，S，{|C，Tc，Lc，{|CN2|K+|K-S C4.S→Sa：S、C、N35. S：S，{|Sa、S、N、3、C、K+|}CK−SaC：S，C，{{}|S，f 2（N 2）|K+CWMF议定书1.A→S：A，{|B、Ta、K ab|卡请参阅下面的行评论。2.S→ B：{|BA、T、K、ab|KBWoo和Lam相互认证。1.P→Q：P，N1Q→P：Q，N2P → Q：{|P、Q、N1、N2 |KpQ→ S：{|P、Q、N1、N2 |Kp，{|P、Q、N1、N2|>KQ类似于WMF协议，我们提出的方法是在两个数据表中使用两个数据表补丁。5.S→Q：{|P、Q、N1、N2、Kpq|Kp，示例（仅限此处）{|P、N1、N2、Kpq|>KQ一个是存在的）。Q →P：{|P、Q、N1、N2、Kpq|Kp，{|N 1，N 2 |KpqQ = Q：{|N 2 |Kpq班亚哈隆1.A→B：A、NaB → S：B，Nb，{|A、Na|KB该补丁程序类似于建议的补丁程序3.S→A：Nb，{|A、B、Kab、 Na|KA，保罗在[12]。{|A、Kab、Nb|KBA→B：{|A、Kab、N b|KB，{|NB|Kab表4已修补的协议描述，第三部分克拉克-雅各布图书馆）和25个反例。我们的方法已经成功地处理了16个计数示例，并且已经显示出能够成功地修补这些协议中的12个。我们的方法通常可以修补一个违反Abadi和Needham原则3的交错-重放错误协议。但是，它不能总是处理违反时间线参考（经典重播）或运行内部攻击的重播错误协议。"[10]例如，它在修补Andrew Secure RPC协议方面没有取得成功：(i) A→ B：A，{|N A|Kab130J.C.L. Pimentel等人。理论计算机科学电子笔记174（2007）117协议名称工具TEVT（秒）BAN混凝土ASRPCOFMC34.34CCITT X.509（1）OFMC0.10CCITT X.509（3）OFMC2.27Denning-Sacco PKOFMC0.33KSLOFMC17.26NSPKCL-Atse28.8O R BAN版本OFMC4.15Splice/ASCL-Atse8.43Hwang-Chen Splice/ASCL-Atse35.15WMF协议CL-Atse0.70Woo和Lam MutualOFMC0.35BAN Modified YahalomOFMC0.74表5总延迟的验证时间（S）(ii) B→ A：{|Na +1，N b|Kab(iii) A→B：{|NB +1 |Kab(iv) B→ A：{|KBP，NBP|Kab在这里，错误的起源与代理命名无关，而是与时间引用有关。特别是，请注意，随机数NBP被用作确认，但NBP的我们计划进一步用其他故障协议来验证我们的方法。此外，我们将分析如上所述的其他缺陷协议，以便提出新的修补方法。[10]参考文献[1] M.阿巴迪和R.李约瑟。密码学协议的谨慎工程实践（Prudent Engineering Practice）。 IEEE软件工程学报，22（1）：6[2] A.D.Ba s in ， S.Moder s heim ， andL.VIGan'o 。Aon-the-flymodel-checkerforsecurityprotocolanalysi s。在D。戈尔曼和E. Snekkenes，编辑，ESORICSSpringer-Verlag。[3] D. Ba s i n，S. Moder s heim，andL. VIGan'o。 OFMC：as ymbol icmodel-checkerfors ecurityprotocols。TechnicalReport450，ET H Zurich，ComputerScie nce，2004年6月。[4] M. Burrows，M.阿巴迪和R. M.李约瑟。身份验证的一个逻辑。伦敦皇家学会学报，426（1）：233[5] J·克拉克和J·雅各布。身份验证协议文献调查：版本1.0（2010年）。技术报告，约克大学计算机科学系 ， 1997 年 11关 于 CAPSL 中 克 拉 克 - 雅 各 布 图 书 馆 的 完 整 说 明 ， 请 访 问http://www.cs.sri.com/millen/capsl/。[6] D. Dolev和A. C.姚明。关于公钥协议的安全性。技术报告2，斯坦福大学，美国加利福尼亚州斯坦福，1983年。[7] 加文·洛。对Needham-Schroeder公钥身份验证协议的攻击。《信息处理快报》，56（3）：131[8] 加文·洛。使用PDR破坏并修复Needham-Schroeder公钥协议。 TACASpringer-Verlag。[9] 加文·洛。对安全协议的一些新攻击在CSFWIEEE计算机学会出版社。J.C.L. Pimentel等人。理论计算机科学电子笔记174（2007）117131[10] 加文·洛。这是身份验证规范的层次结构之一。在CSFWIEEE计算机协会。[11]R.蒙罗伊和M.卡里略。论归纳法下安全目标制定的自动化[编辑]在M.H. Hamza，编辑，IASTEDActa出版社[12] 劳伦斯C.保尔森。验证密码学协议的归纳法[编辑] 计算机安全杂志，6（1-2）：85[13] G.钢铁 ，A.邦迪 和M. Maidl。 攻击 asokan-ginzboorg协议 的密 钥分发 在a nad-hocbluetoothnetworkusingcoral。 InH. Kni g，M. H einer，andA。Wolisz，editors，IFIPTC6工作组6.1：第23届IFIP网络和通信正式技术国际会议论文集分布式系统，第2767卷，第1-10页，柏林，德国，2003年。FORTE 2003（正在进行的工作文件）。[14] 保罗·西弗森。重播攻击的分类法。在CSFWIEEE计算机学会出版社。[15] M athieTur uani。Sec uri tedesProtocolesCryptographiques：Deci dabi litetComplexite。P hDthesis，U ni versi t e H inriPoincare，December2003.