反潜战议定书再探：统一观点下的合同签署协议分析

理论计算机科学电子笔记125（2005）145-161www.elsevier.com/locate/entcs《反潜战议定书》再探：统一观点1PaulHankesDrielsma2SebastianMödersheim3瑞士苏黎世联邦理工学院计算机科学系摘要我们重新分析屈臣氏集团合约签署协议，并以协议的整体统一观点作为基础，对协议及其目标进行 这条推理路线产生了一个更简单和更清晰的代理模型和协议目标，标准的安全分析方法，因为它不需要公平性约束，只使用标准的认证和保密属性。我们还使用自动化分析工具OFMC及其扩展OFMC-FP分析了该模型的有限和无限多个协议会话关键词：合同签署，公平交换，自动协议分析1介绍合同签署协议，如[1]中提出的ASW协议，允许其用户数字签署合同，而不必见面并签署文档或通过标准邮件交换文档，这在商业世界的日常通信中非常有用。当考虑对这些协议进行形式化分析时，困难在于它们超出了许多现有协议分析方法的范围：尽管签名和交换消息的行为是这些方法的标准1这项工作得到了FET开放项目IST-2001-39252和BBW项目02.04312电子邮件地址：drielsma@inf.ethz.ch3电子邮件地址：moedersheim@inf.ethz.ch1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2004.05.024146P. Hankes Drielsma，S.Mödersheim/Electron.注意Theor。Comput. Sci. 125（2005）145然而，在合同签署过程中，很难将合同签署协议旨在实现的目标与它们所依赖的特殊假设我们提出了一个统一的视图的ASW协议，其中的子协议被视为一个单一的协议与不同的可能的执行路径。虽然这种观点隐含在建立的协议模型中，例如，在[5，14]中，我们明确地描述和推理协议及其目标，这是基于这种高层次的观点，它产生了对ASW合同签署协议的更简单，更直观的理解。特别是，我们的模型在两个方面比其他方法更简单。首先，作为我们的观点的结果，人们不必区分入侵者和不诚实和腐败的参与者（甚至是不同程度的腐败），因为这在其他几个模型中是必要的第二，采纳这一观点使我们能够以简单而有力的方式对这样一项议定书的目标进行推理。例如，我们演示了协议设计者确定的几个安全目标实际上可以表示为标准的保密和身份验证属性，从而然后，我们具体地应用我们的统一视图，构建ASW协议的模型，并使用我们在我们的团队中开发的工具进行形式化分析，即On-the-Fly Model-OFMC 及 其 基 于 抽 象 的 扩 展 OFMC-FP 。 两 者 都 是 在AVISPA项目（http://www.avispa-project.org）的背景下开发的，该项目提供了一个用于自动分析安全协议和应用程序的工具集。使用OFMC，我们可以对有限多个会话（即协议的执行）验证协议除此之外，我们还使用OFMC-FP进行了分析，验证了无限多会话的协议。在分析中，这些工具报告了对ASW协议的攻击，这是由于目标的指定非常微妙。调整这些，我们能够验证该协议确实确保了一个稍微弱的目标，仍然意味着主要的公平交换目标。我们观察到，即使我们的方法是简单的理解协议，自动分析的正式模型的设计提出了几个挑战。在介绍这些之后，我们简要地讨论了我们对有限和无限多协议会话的自动分析2背景ASW协议由Asokan，Shoup和Waidner在[1]中提出，是一种乐观的公平交换协议，用于合同签署，旨在使两个P. Hankes Drielsma，S.Mödersheim/Electron.注意Theor。Comput. Sci. 125（2005）145147交换子协议：1.O →R：me1=SigO（VO，VR，T，text，h（NO））2.R →O：me2=SigR（me1，h（NR））3.O →R：NO4.R →O：NR中止子方案：1.O →T：ma1=SigO（中止，me1）2.T →O：ma2=如果已解决（me1），则SigT（me1，me2）elseSigT（aborted，ma1）;aborted（ma1）=true解决子协议：1.O →T：mr1=me1，me22.T →O：mr2=如果中止（me1），则SigT（中止，me1）elseSigT（me1，me2）;resolved（me1）=trueFig. 1. 反潜战的子协议各方承诺遵守事先商定的合同文本。只有在需要争议解决时，才涉及可信第三方（T3P）（因此，术语乐观，这将这种方法与其他方法区分开来其中在线受信方参与每个交换）。在解决争议时，T3P要么发布一份替代合同，声称他承认所讨论的合同有效，要么发布一个中止令牌，声称他从未发布过，也永远不会发布替代合同。该协议的一个重要要求是入侵者不能永远阻塞诚实代理和T3P之间的消息。2.1方案目的这样一项议定书应该实现的目标是多方面的。我们在这里讨论设计者确定的安全目标，并在稍后讨论我们的验证时参考这些非正式描述注意[1]中的“公平性”是指虽然[1]提出了一个任意项目公平交换的框架，但我们只考虑这个框架在合同签订中的应用我们148P. Hankes Drielsma，S.Mödersheim/Electron.注意Theor。Comput. Sci. 125（2005）145§因此，以专门针对我们目的的方式描述随后的目标。1. 首先，也可能是最重要的是公平交换的概念，这意味着，在协议执行结束时，要么双方都拥有有效的合同，要么双方都没有特别是，我们要求如果一个agent最终只得到一个abort token，那么另一个agent就不能拥有有效的合约。2. 有效性意味着，如果两个诚实的代理人P和Q完成了协议，并且从未选择放弃当前的协议运行，那么每个人都确实有一个有效的合同。3. 该协议还提供了及时完成的保证：更具体地说，协议运行的发起者和响应者可以确保在有限的时间内完成。4. 在签订合同的情况下，不可否认性的目标5. 第三方可验证性规定，如果受信任的第三方应该是腐败的，并且以损害协议参与者之一的交换公平性的方式行事，那么这种腐败行为可以向外部验证者证明。公平交换的要求通常是以活性性质的形式来表述的：“如果一个代理人有一个有效的合同，那么另一个代理人要么也有一个合同，要么最终能够获得一个合同”。一般来说，活性属性对于各种验证方法都是有问题的，特别是那些涉及有限状态空间的方法。在这种情况下，通常通过安全属性来近似活性属性，即，如果协议满足安全属性，那么它也满足近似的活性属性，例如[14]中所做在第3章中，我们同样确定了要检查的适当的安全属性;然而，正如我们将展示的那样，从我们对协议的统一视图中，2.2方案说明该协议，如图所示1，由三个子协议组成：交换，中止和解决。前者仅涉及两个协议参与者，发起者O和响应者R，而后两者仅在可信第三方T被要求解决争议时执行。我们的符号约定如下：SigO（M）表示消息M由代理O执行，其用于签名验证的公钥是VO。合约P. Hankes Drielsma，S.Mödersheim/Electron.注意Theor。Comput. Sci. 125（2005）145149我们称之为文本。在协议中，每一方都生成一个随机数，我们分别为发起方和响应方写NO和NR最后，函数h是假设为抗冲突的密码散列函数。我们注意到，该协议定义了两种有效合约：由交换子协议获得的标准合约，或由T3P发布的替代合约，两者具有相同的有效性。交换子协议：如果两个参与者都是诚实的，并且没有网络故障或入侵者干预，在执行交换子协议后，双方都将拥有有效的标准合同。发起方和响应方都生成随机数NO和NR，它们被称为各自对合同的秘密承诺给定这些，它们通过对这些值进行散列来计算它们所谓的公共承诺，分别产生h（NO）和h（NR然后，协议进行两轮：第一轮，每一方都公开表示对商定的合同的承诺，但不透露他的秘密承诺。在第二回合中，他们交换了各自的秘密承诺。然后，每一方都可以对后者进行散列，从而验证他收到的所谓秘密承诺确实对应于第一个协议阶段的公开承诺在这种交换结束时，每一方都拥有一份有效的标准合同，格式为me1，me2，no，NR。中止子协议：如果O在可接受的时间范围内没有收到R的回复me 2（其中“可接受”的定义完全由O决定），他可以通过调用可信第三方来他发送一个签名的中止请求ma1，表明他希望中止交换。T3P被假定维持一个永久性的合同数据库，其中记录了他被要求进行仲裁的合同。如果他已经声明了合同的有效性（由resolved（me1）表示），那么他向发起者发送一个形式为SigT（me1，me2）的替换合同否则，他会回复一个所谓的中止令牌，签署发起者这样的令牌不会使现有的合同无效，而只是作为T3P的承诺，他以前没有解决有问题的合同，将来也不会这样做解决子协议：解决子协议类似于中止，但可以由任何参与者调用。如果双方在合理的时间内没有收到另一方的秘密承诺随机数，他们将请求T3P解决合同解析请求包括来自交换子协议第一阶段的两个消息，me1和me2。如果T3P已经发出了用于合同的问题（表示为中止（我1）），他以实物答复，150P. Hankes Drielsma，S.Mödersheim/Electron.注意Theor。Comput. Sci. 125（2005）145§交易所1. O→R：我1如果超时，则中止1。O→T：ma1中止2. T→O：ma2（中止令牌或替换合约）其他交换2. R→O：me2交换3。O→R：NO如果超时，则解析1。O→T：mr1决心2. T→O：mr2（中止令牌或替换合约）其他交换4. R→O：NR图二. 我们对协议的统一观点下的发起人角色。中止令牌。否则，他发出一份替换合同，并在他的数据库中表明他已经解决了该合同。2.3入侵者模型我们采用Dolev和Yao [8]的标准入侵者模型，其中入侵者完全控制网络，但无法破解密码。此外，入侵者可以作为一个正常的协议参与者，作为发起者或响应者，但不能作为T3P。正如我们将在3中更详细地讨论的那样，这样的入侵者模型已经包含了与入侵者合作的妥协或不诚实的代理的可能性，并且我们希望表明，即使在与入侵者一起运行的协议中，诚实代理的利益也总是得到保证3统一的观点本文背后的关键思想是查看和推理，ASW这种观点隐含在协议的构建中，因此也隐含在[5，14]构建的协议模型我们明确地利用这一观点的原因有关的协议的属性。更具体地说，我们认为中止和解决子协议是主交换协议的一部分例如，发起人角色P. Hankes Drielsma，S.Mödersheim/Electron.注意Theor。Comput. Sci. 125（2005）145151发送初始消息给响应者交易所1. O→R：我1来自响应器交换器2的回复。R→O：ma2交换3.O→R：NO超时中止1. O→T：ma1要求可信第三方中止从响应者收到回复将自己的随机数发送给响应者响应者的回复交换4. O→R：NR超时决心1. O→T：mr1已要求可信第三方解决T→O：解析令牌T→O：中止令牌由可信的第三方解决图三.发起者角色的状态转换视图。虚线表示如果可信服务器是诚实的，则永远不会发生的转换，正如我们将在下面的分析中显示的那样。然后看起来如图2所示（响应者角色是类似的），其中超时表示代理人在合理的时间内没有收到对他的最后一条消息的回复。我们避免指定超时发生的具体时间：它可能只是几秒钟或整整一个小时-对于协议的安全性来说，重要的只是有这样一个超时，所以代理不会永远等待答案。图3示出了扮演发起者角色的代理的内部状态：在发送他的初始消息之后，他处于等待回复直到超时的状态如果发生超时，则他尝试中止协议，并因此等待可信第三方（其可以是替换合同或签名的中止令牌）。 否则（如果他及时收到回复），他继续执行常规协议并发送他的随机数，到达与发送第一条消息后类似的状态：要么在分配的时间内收到回复，要么他联系可信的第三方。这个模型虽然是抽象的，但它是协议的真实实现的忠实代表，因为代理确实用这种内部超时来保护自己请注意，这与本合同签署协议中的滥用可能性有关：当发起者迈出第一步时，响应者可以自由地通过发送第二个消息来接受合同，或者通过忽略它来拒绝它。特别是，不诚实的响应者可以在与其他代理人的谈判中滥用合同中发起者签署的部分（例如，通过向竞争对手争取更有利的合同）。请注意，与例如类似的GJM[9]协议不同，ASW协议没有通过特殊的加密技术来防止这种滥用的手段。持有有效的标准合同中止152P. Hankes Drielsma，S.Mödersheim/Electron.注意Theor。Comput. Sci. 125（2005）145比如私有合同签名。因此，超时是缩小发起者对滥用攻击的脆弱性窗口的唯一方法，虽然我们假设入侵者可以根据Dolev-Yao模型控制整个网络，但协议要求他不能永远阻止诚实代理和T3 P之间的消息。人们可以直观地想象这种情况如下：所有网络连接都可能崩溃，但诚实的代理仍然可以通过其他媒体（例如普通邮件）向T3P发送必要的消息，并且这个过程不会永远持续下去可以说，我们因此有两种公平假设：第一，一个诚实的代理人不会永远等待另一方的回答，第二，与T3P的“紧急”协议最终会成功。再看一下图3，我们可以将这种公平性约束的组合解释为保证扮演发起者角色的诚实代理（以及响应者角色的类似保证）不会永远停留在任何中间状态（图中带有向外箭头的状态），但最终会到达三个最终状态之一，（i）他收到响应者因此，两个公平性约束（超时和来自T3P的保证回复）足以得出结论，每个扮演发起者或响应者角色的诚实代理最终将以有效（标准或替换）合同或中止令牌结束。粗略地说，如果代理人收到一个有效的合同，那么他的利益就得到了保证，但是如果他收到一个中止令牌，那么它仍然表明没有其他人可以获得有效的合同。这给了我们一个关于协议的新观点，因为通过一个简单的元论证，我们现在可以从一个有公平约束的模型转到一个没有公平约束的无限状态转换系统中的状态可达性。这个思想本质上是，我们只需要检查，如果一个诚实的代理人到达了协议执行的最终状态，那么他应该通过协议获得的保证确实得到了满足。换句话说，我们不需要考虑处于中间状态的代理人的保证，因为他们最终会达到最终状态，因此我们不必考虑“如果代理人最终能够达到某个状态”的形式4.如果响应者发送了一个秘密承诺，当被散列时，它与公共承诺不对应，那么这将被视为他根本没有发送任何消息（这可能会导致超时）。P. Hankes Drielsma，S.Mödersheim/Electron.注意Theor。Comput. Sci. 125（2005）145153§我们检查的属性。将目标编码为安全属性是部署用于无限状态分析的自动和半自动方法的基础。同样在有限状态分析中，对安全属性的限制通常是必不可少的，例如。[14]使用类似的论证，即检查具有公平性条件的协议4目标编码我们现在要对比两个模型：一方面，具有上述公平性约束的模型（即代理最终将从可信第三方获得超时和回复），另一方面是没有公平性约束的模型。在无公平模型中，诚实代理人的状态转移如图3所示，被解释如下：没有超时，也没有保证的应答，因此代理可以永远保持在任何中间状态。因此，代理的局部状态转换系统是非确定性的，因为在诚实代理等待另一方回复的状态中，他可以在任何时候（即，没有超时）开始中止或解决协议，如果合适的话。由此可以直接得出，如果在具有公平性的模型中存在对安全属性的违反，那么在不具有公平性的模型中也存在违反。这表明我们的方法是合理的，如果我们可以证明模型中没有公平约束的属性，那么它们也必须在有公平约束的模型中成立。挑战在于找到适当的安全属性，这些属性在没有公平性约束的情况下确实成立，并且隐含着我们希望检查的§2.1的安全性和活性属性我们现在回顾2.1中在协议的新视图下列出的目标，并展示如何将我们希望检查的目标编码为安全性能。让我们从目标（3.）开始，及时完成，这意味着诚实的代理最终总是会达到有效的标准或替换合同或中止令牌。该目标是具有公平性约束的模型的直接结果，如所讨论的，并且因此不需要显式地检查。目的（1.），公平交换是该协议的主要目标，即要么双方都获得合同，要么双方都不获得合同。我们将此目标分解为以下两个：154P. Hankes Drielsma，S.Mödersheim/Electron.注意Theor。Comput. Sci. 125（2005）1451a.如果一个诚实的代理收到一个中止令牌，那么没有人（除了可信的第三方）可以获得一个有效的标准或替换合同。1b.如果一个代理人A（不一定是诚实的）已经获得了一个由诚实的代理人B签署的有效的标准或替代合同，那么B也拥有一个有效的合同，或者可以从可信的第三方获得一个合同。目标（1a.）是我们分析的主要目标，因为它反映了与中止令牌相关的基本保证。这个目标的好处在于，它指的是一个诚实的代理人的最终状态（随后不会改变），而不是中间状态。因此，可以在没有公平性的情况下检查模型，即在代理已经到达具有中止令牌的最终状态的所有状态中，除了T3P之外没有人可以生成有效的标准或替换合约匹配该中止令牌。无法生成这些消息可以用标准协议分析方法通过保密属性来表示。因此，我们可以将协议的主要目标简化为协议分析中的标准属性（尽管在直接应用工具时存在技术困难，我们将在下面讨论目标（1b.）是目标（1A）的结果。（3）：如果代理人A拥有由诚实代理人B签署的有效合同，则通过（3.）B也将最终到达中止令牌或有效合约，并且通过（1a.），如果他得到中止令牌，则A不能拥有有效合同，这是矛盾。B最终会得到一份有效的合同。请注意，入侵者或扮演发起者角色的不诚实代理可以获得有效合约和中止令牌（通过与诚实代理执行正常运行并向T3P请求中止）的情况并不违反上述目标：中止令牌仅保证T3P从未且永远不会解决此合约，但不会使现有合约无效。我们现在转向目标（2.），e.可靠性。在我们的模型中，每个诚实的代理人最终都会达到最终状态，有效性意味着当诚实的代理人A收到与诚实的代理人B的会话的中止令牌时，A或B必须选择中止合同。由于来自T3P的中止令牌包含根据协议的代理A或B的签名，因此它包含A或B确实想要中止协议运行的隐式证明。因此，由于中止令牌的形式，有效性是一种隐含的保证，因此在后面的分析中将不考虑。目的（4.），不可否认性也可以被看作是消息格式的结果，因为在有效的标准或替换合同中，P. Hankes Drielsma，S.Mödersheim/Electron.注意Theor。Comput. Sci. 125（2005）145155双方的签名都包含在内，因此我们可以假定他们同意合同文本。然而，我们也对进一步的分析感兴趣，即对ASW的认证属性（或[10]中的协议属性）的分析。我们的分析将包括检查重放和随机数的混淆。这样的标准认证属性不依赖于公平性，因此可以直接进行检查。最后，目标（5.），第三方可核查性在我们的环境中不相关，因为我们假设T3P始终是诚实的。总之，我们已经表明，协议的几个目标是其结构，假设和消息格式的直接后果。从本质上讲，诚实的代理将收到中止令牌或有效合同。在后一种情况下，他的利益得到了保证，但仍需表明，在中止令牌的情况下，他的利益也得到了保证。 这相当于如果诚实的代理获得中止令牌，则有效合同保持秘密。因此，由于我们的观点和元推理的协议，我们已经得到了一个模型，属于标准的自动化协议分析方法（通常只支持保密和认证属性）的领域，我们已经完全避免了公平性问题正如我们将在下一节中看到的，即使是对这个简化模型的分析也是具有挑战性的。让我们以入侵者模型的评论来结束这一节。有几种方法可以区分入侵者和不诚实或腐败的代理（腐败程度不同）。这种区别的原因之一是协议的安全属性通常只适用于诚实代理之间的会话特别是，入侵者可以在与诚实代理的会话中扮演发起者或响应者的角色;在这样的会话中，该诚实代理没有安全属性，而该会话不应危及诚实代理之间的其他会话的安全。由于我们的简化视图，我们必须检查屈臣氏集团的主要安全属性，即（1a.）一旦一个诚实的代理人收到一个中止令牌，有效合同的保密性在另一个代理人不诚实的情况下也应该保持。(But不一定确保该不诚实的代理也具有相同的安全保证。这意味着我们不需要区分不诚实代理人的各种腐败行为。5结果在上一节中，我们已对ASW协议及安全属性的公式形成统一的看法我们现在具体地应用这些思想，156P. Hankes Drielsma，S.Mödersheim/Electron.注意Theor。Comput. Sci. 125（2005）145使用我们小组开发的两个第一个工具是On-the-Fly Model-Stimulator（OFMC），它基于入侵者的符号表示，称为懒惰入侵者[4]。对于终端，它需要对可以执行的会话的数量进行限制，但不需要其他限制，例如对消息的复杂性的这与[14]的有限状态分析相似第二个工具OFMC-FP是OFMC的扩展，当可以执行的协议运行次数没有限制时，它具有可达状态的抽象定点计算，但是消息的复杂性在该方法中是有界的。在撰写本文时，OFMC-FP仍处于初步状态：特别是，用户必须手动设计所采用的抽象。OFMC和OFMC-FP都是在AVISPA项目的背景下开发的用户使用高级协议规范语言（HLPSL [2]）指定协议;然后这些规范自动转换为低级中间格式（IF [3]），后者是自动分析工具的输入语言。因此，第一项任务是说明我们对HLPSL中ASW协议的看法。5.1质量标准建立反潜战的正式模型面临三大挑战：首先，协议的一个方面是难以建模的是由T3P维护的中止和解决的合同的数据库。许多现有的协议规范语言无法表达这一点，但HLPSL和IF包含了必要的构造（即有限消息集）来建模这样的数据库。此外，数据库不能直接集成到使用抽象的无限状态验证方法中。其次，当使用OFMC时，我们约束诚实代理的会话数量以获得有限的状态空间。然而，T3P可以执行的步骤数量没有先验限制：特别是，入侵者可以与T3P交换无限数量的消息。因此，在OFMC的有限会话分析中，我们也限制了T3P可以处理的来自入侵者的请求最后，虽然我们已经把我们分析的主要问题简化为一个秘密问题，但还有一个更微妙的问题。当发出包含初始消息me1的中止令牌时，我们必须检查包含me1的任何有效合约的保密性。因此，我们不只是一个国家的秘密，P. Hankes Drielsma，S.Mödersheim/Electron.注意Theor。Comput. Sci. 125（2005）145157e1. I→R：me1e2. R→I：me2e3. I→R：NIe4. R→I：NR的1. I→T：ma1一台2. T→I：中止令牌e1J。I→R：me1e2J。R→I：me2J入侵者停止通信R1. R→T：{me1，me2J}r2。T→R：中止令牌见图4。OFMC返回的攻击：入侵者（表示为I）中止已经交换的合约。在使用相同响应者的后续运行中，响应者则无法解析协议。一个典型的信息，而是一种信息的模式。目前HLPSL和IF（或大多数其他协议规范语言）不支持这种特性。作为解决这个问题的一种简单方法，我们指定一个诚实的代理，它充当观察者，并适当地标记错误状态5.2基于OFMC的通过限制T3P处理的会话数量和来自入侵者的请求数量，我们现在可以直接检查referee的transition是否被触发，以及检查身份验证属性。OFMC发现了几个在[14]中已经确定的认证问题。首先，该协议不提供强认证（Lowe在[10]中定义的单对象协议），因为它没有明确的重放保护：如果入侵者监听两个诚实代理的会话，他可以与响应者重放交换协议任意次数，并获得有效的合同，每个合同都有一个新的响应者随机数。然而，我们认为应将隐含的重放保护作为合同的一部分，例如，交易通常由唯一的交易编号标识。在这种情况下，我们因此检查协议提供弱认证（也称为非单射协议，[10]）。关于合同文本和随机数N0和NR的弱认证也被违反，OFMC返回由[14]中报告的相同认证问题引起的攻击跟踪。最后，OFMC针对各种有限测试场景验证了仅针对合同文本的当转向我们已经公式化的保密属性时，OFMC报告了图4中显示的攻击。假设充当协议发起者的入侵者I和诚实的响应者R已经完成了交换子协议的运行，而不涉及T3P（步骤e1到e4）。每一个都生成了一个秘密承诺（分别为NI和NR），并以158P. Hankes Drielsma，S.Mödersheim/Electron.注意Theor。Comput. Sci. 125（2005）145标准格式的有效合同。 现在假设入侵者向T3P发出针对该相同合约的中止请求。后者以前从未解决过有问题的合约，将以有效的中止令牌进行响应入侵者现在开始与R的第二个会话，重放前一个会话的第一个消息me1R生成一个新的随机数NRJ，并真诚地用第二条消息me2J回复，包括这个新的随机数的散列然而，入侵者并没有回复他的随机数，而是忽略了R。 反过来，R将超时并向T3P请求合约的解析因为所讨论的始发者消息ME1已经被I中止，所以I将用中止令牌进行响应。因此，在完成第二个协议会话时，R有一个中止令牌，而I有一个有效的合约其对应于该中止令牌（在其包含相同的初始消息ME1的意义上）。当然，R自己也拥有这个契约，在第一个协议会话中与I形式上，这违反了目标（1a.）：一个诚实的代理有一个中止令牌，而另一个人（入侵者）有一个有效的合同。这实际上不是一个问题，因为诚实的代理人本身也有这个有效的合同。特别是，原始目标（1.）没有违反，因为两个代理人确实拥有同一合同文本的有效合同这有点令人惊讶，因为我们现在看到，在某些情况下，诚实的代理确实拥有有效的合同和中止令牌。注意目标（1a.）也被[14]考虑过，他报告了nonce和契约关系中的问题，但没有发现（1a.）可以被侵犯。同一作者在[13]中报告了对GJM的类似攻击，GJM是一个类似的合同签署协议[9]。我们还注意到，他们为解决上述认证问题而建议的协议改进并不能防止这种情况。因此，我们放宽了目标（1a）。以下是较弱的目标（1aJ.）：“if anhonest agent has an abort token, then he also possesses a valid 请注意，此属性与（1b.）公平交易（1）。对于这个被削弱的目标，OFMC没有发现进一步的攻击。我们还希望指出，在响应方对公共承诺的重放进行额外检查将防止这种攻击。5.3OFMC-FP的无界会话分析我们还使用OFMC-FP分析了该协议，该协议采用了一种新的基于抽象的固定点计算。有必要扩展现有的OFMC-FP技术，以便能够整合服务器及其合同数据库。该技术不是完全自动的，因为用户P. Hankes Drielsma，S.Mödersheim/Electron.注意Theor。Comput. Sci. 125（2005）145159必须自己指定一个适当的抽象。OFMC-FP也可以检测攻击，但由于抽象性，它们在我们最初的具体模型中可能是不可能的;然而，如果抽象模型的安全性得到这与其他基于抽象的验证方法类似[7]。使用OFMC-FP技术，我们已经建立了OFMC的验证结果的参与者，会话和转换的T3 P的数量无限;只有消息的复杂性是有界的，在这种方法中。特别是，我们首次证明了仅对合同文本的弱认证此外，OFMC-FP揭示了不诚实的发起者可以获得也已被服务器中止的有效的标准合同，这包含违反（1a.）上面已经报道此外，我们确定，在所有这些情况下，另一方也获得了有效的标准合同，从而验证了弱化的财产（1aJ.）。然而，我们注意到，作为分析的一部分，我们发现，对于性质（1aJ.）为了保持，一个重要的先决条件是这样的事实，即扮演发起者角色的诚实代理3 .第三章。6相关工作和结论大量的文献存在于合同签署协议的分析，特别是ASW和类似的GJM协议。Shmatikov和Mitchell使用有限状态模型检查器Mur [12，13，14]对ASW和GJM协议进行了分析（具有有限数量的会话）。他们的方法与我们的方法最接近，即他们也遵循减少公平性问题的主要思想安全属性。虽然他们也隐含地使用了协议的统一视图，但他们并没有明确地使用它来执行关于协议的元推理。另一个不同之处是，它们还将入侵者与不诚实的代理人（腐败程度不同）区分开来。此外，他们检查GJM协议的无滥用性（而ASW的设计并不是为了确保无滥用性）。Das和Dill [7]是第一个描述使用抽象和模型检查器Mur为无限数量的会话自动分析合同签署协议GJM的人。与我们的分析类似，他们关注公平交换的属性。Kremer和Raskin [11]专注于无滥用，并认为在某些假设下，即使ASW协议也是无滥用的（尽管这不是协议设计者的原始目标适当地模拟160P. Hankes Drielsma，S.Mödersheim/Electron.注意Theor。Comput. Sci. 125（2005）145§恶意代理的策略和策略优势，他们使用博弈论的方法和交替过渡系统。他们使用模型检查器MOCHA进行自动分析;注意，他们没有考虑协议的并行多次运行，而是采用强类型假设。5有几个作品（不专注于自动化分析）对这些协议及其保证的推理，特别是乐观和公平[5，6]。所采用的模型比我们的模型更详细，因为它们明确地使用超时并区分入侵者和（不同种类的）不诚实的代理人。此外，在这方面也经常采取与我们类似的观点，尽管据我们所知，没有人用它来推理议定书及其目标。我们采纳此统一观点，并明确地使用其来推理协议然而，如5.1中所述，即使在统一视图下，使用现有协议分析工具的规范和分析也是具有挑战性的，特别是对于维护数据库的可信第三方的建模，中止和解决的合同。我们的分析证明了与[14] 还表明，人们可能直觉上期望《议定书》的目标（1a.）事实上是被我们提出的攻击所侵犯的。然而，我们可以证明，除了这些问题之外，该协议是安全的。虽然我们至今的工作一直以屈臣氏集团为重点，但我们乐观地认为，采纳此统一观点所带来的裨益亦将适用于类似的协议一般来说，我们对安全目标进行的元推理不仅有助于更好地理解给定协议的目标，而且正如我们所看到的，还可以识别潜在的方法，将看似复杂的目标简化为更标准的概念，如认证和保密。通过这种方式，我们希望扩展现有方法的安全协议的形式化分析的适用性。引用[1] N. Asokan，V. Shoup，and M.韦德纳异步乐观公平交换协议。在1998年IEEE安全和隐私研究研讨会论文集，第86-99页。5强类型假设是比OFMC-FP所做的消息大小限制更强的限制;OFMC不需要类似的限制。P. Hankes Drielsma，S.Mödersheim/Electron.注意Theor。Comput. Sci. 125（2005）145161[2] 阿维斯帕。可扩展2.1：高级协议规范语言。见www. avispa-project.org/delivs/2.1/，2003年。[3] 阿维斯帕。第2.3章：中间体见www.avispa-project.org/delivs/2.3，2003年。[4] D. Basin，S. Müodersheim和L. 维甘奥。一种用于安全协议分析的动态模型在大肠Snekkenes和 D.Gollmann ， editors ， Proceedings of ESORICS'03 ， LNCS 2808 ， pages 253-270.Springer-Verlag，2003.可在www.avispa-project.org上获得。[5] R. Chadha，M. Kanovich和A.谢德罗夫归纳方法和合同签署协议。在p. Samarati，编辑，Proceedings，8 th ACM Conference on Computer and Communications Security，第176-185页，纽约，2001年11月。Press.[6] R. Chadha，J. C.米切尔，A. Scedrov和V. Shmatikov。签约，乐观，和优势。CONCUR：第14届并发理论国际会议。LNCS，Springer-Verlag，2003年。[7] S. Das 和 D.L. 迪 尔 抽 象 转 移 关 系 的 逐 次 逼 近 在 Proceedings of the 16 th Annual IEEESymposium on Logic in Computer Science（LICS-01），第51-60页IEEE计算机协会。[8] D. Dolev和A.耀公钥协议的安全性。IEEE Transactions on Information Theory，2（29），1983.[9] J. A. Garay，M.Jakobsson和P.麦肯齐无滥用乐观签约。在Proc.19th International Advancesin Cryptology Conference[10] G.洛身份验证规范的层次结构。在第10届IEEE计算机安全基础研讨会（CSFW'97）IEEEComputer Society Press，1997.[11] J. Raskin和S.克莱默无滥用合同签订的博弈分析第15届IEEE计算机安全基础研讨会，第206IEEE Computer Society Press，June 2002.[12] V.Shmatikov和J.C.米切尔公平交换协议的分析。1999年FLoC正式方法和安全协议研讨会论文集，意大利特伦托，1999年。[13] V.Shmatikov 和 J.C. 米 切 尔 无 滥 用 合 同 签 订 分 析 。 第 四 届 金 融 密 码 学 国 际 会 议 论 文 集（FinCrypto'00），2001年[14] 诉Shmatikov和J.C. 米切尔两个合同签署协议的安全状态分析理论计算机科学，283（2）：419