块链接技术及已知对和选择文本攻击的协议分析：安全性加强和明文攻击防范

理论计算机科学电子札记128（2005）87-104www.elsevier.com/locate/entcs协议产生已知对攻击和选择文本攻击史蒂夫·克雷默1英国伯明翰大学计算机科学学院Mark D.瑞恩2英国伯明翰大学计算机科学学院摘要在本文中，我们报告了在协议中发现已知对和选择文本攻击的分析由于这些攻击是在块的水平，我们扩展了攻击者的特殊功能相关的块链接技术。分析是自动使用Blanchet在第一个协议中，我们展示了与链接相关的特殊入侵者能力如何可能危及随机数的保密性，并且选择密文攻击是可能的。我们提出了两个修改版本的协议，加强其安全性。然后，我们说明了已知对和选择明文攻击的第二个协议。关键词：安全协议的形式化分析，已知对和选择文本攻击，块链接。1介绍随着互联网和电子商务的迅猛发展，计算机安全变得越来越重要。然而，历史表明，1电子邮件：S. cs.bham.ac.uk2 电子邮件：M.D. cs.bham.ac.uk1571-0661 © 2005由Elsevier B. V.出版，CC BY-NC-ND许可下开放获取。doi：10.1016/j.entcs.2004.11.04388S. Kremer，医学博士Ryan/Electronic Notes in Theoretical Computer Science 128（2005）12安全协议非常容易出错，并且将形式化方法应用于安全系统的需要已被广泛接受。最著名的例子之一是在17年前提出的Needham-Schroeder公钥协议[15]中发现的Rewaw Lowe [9]。该协议被认为，甚至证明是正确的之前（虽然人们不得不承认，洛改变了一些，可能是不切实际的，假设）。1983年，Dolev和Yao [6]通过定义自那时以来被称为Dolev-Yao模型，为将形式化方法应用于安全协议奠定了基础。该模型基于以下两个假设：• 入侵者完全了解并可访问通信网络：他可以删除任何发送的消息并插入他可以构建的任何消息;• 密码学是完美的，例如，除非你知道密钥，否则不可能解密加密的消息。在过去的二十年里，这个模型得到了很好的研究。在一个方向上，已经建立了许多与验证的可判定性和复杂性有关的理论结果，例如[24，7]。在另一个方向上，已经使用和开发了大量的方法和（部分或完全自动化）工具，例如[1，8，9，12，16，19]。虽然该模型的第一个假设被广泛接受，但完美加密假设被认为过于强大。例如，许多加密方案呈现攻击者可能利用的代数性质。例子包括RSA en的乘法性质，加密方案，即（memodn）×（memodn）=（m1×m2）emodn，事实上，迪-赫尔曼密钥协议是基于交换性的前，假设，即gab=gba，或者基于“异或”的加密抵消了a=a.最近的许多论文旨在扩展Dolev-Yao模型与这些额外的属性[2，3，14，17]。另一种在标准Dolev-Yao模型中无法捕获的攻击是猜测攻击[4，5，10]。 在猜测攻击中，入侵者试图通过猜测来破解弱密码。只要协议允许验证先前的猜测是正确的，猜测攻击就可能发生。类似的密码分析，虽然不限于弱数据，但可以在协议允许获得已知对或选择文本的可能性时执行。在已知对攻击中，攻击者既知道明文又知道相应的密文。然后，当密码分析员试图获得关于密钥的一些信息时，该信息可能是有用的。更强大的攻击是选择明文攻击和选择密文攻击，其中攻击者可以选择明文进行S. Kremer，医学博士Ryan/Electronic Notes in Theoretical Computer Science 128（2005）89他就能知道密码反之亦然已知的明文攻击例如在第二次世界大战中被用来破解恩尼格玛密码.密码分析家利用天气预报通常包含“潮湿3”这个词的事实。易受已知明文攻击的密码系统的另一个示例是当异或被用作加密运算符时。知识一个已知对的密钥就足以恢复密钥（尽管在这个密码系统中不应该使用同一个密钥两次）。大多数现代密码都能抵抗这种攻击.然而，Shoup在[18]中指出，OAEP抵抗选择密文攻击的证明是令人敬畏的。已知密文和选择密文也可以用于发起（非线性）字典攻击。给定在弱加密密钥（例如密码）下加密的已知对，攻击者可以尝试用来自列表或字典的密钥加密明文并比较结果。当给定一个选择文本时，攻击者准备（一劳永逸地）一个用可能的密钥列表加密（或解密）的文本列表。然后，攻击者可以选择获取此文本的加密（或解密），并尝试在其列表中找到结果以恢复密钥。这是一种特殊的猜测攻击。我们认为，重要的是要明确对协议中使用的密码系统所做的假设，而不是将其视为黑箱。如果攻击者可以使用协议作为加密（解密）预言，则协议使选择明文（密文）攻击成为可能。即使这可能不总是导致攻击，也应该分析这样一个神谕的存在：攻击者可以例如通过使用相同的密钥混合两个不同的协议来发起攻击，其中每个协议可以是独立安全的。在本文中，我们的目标是开发一个自动化的方法，以确定是否一个协议的可能性，安装已知对或选择的文本攻击的底层加密方案。我们在分组密码的框架中这样做。在这种密码中，加密是在块的级别上执行的，我们需要考虑使用什么技术来链接不同的块。这些技术提供了一些额外的攻击能力，“相关工作与我们最接近的工作是Stubblebine和Meadows他们使用NRL协议分析器来自动进行分析，并展示如何在IP封装安全协议的早期版本中自动发现已知的攻击。与我们工作的一个主要区别是Stubblebine和Meadows模型密码块3德语天气90S. Kremer，医学博士Ryan/Electronic Notes in Theoretical Computer Science 128（2005）在低级别上链接，对异或操作进行建模然而，由于NRL协议分析器的限制，关联交换属性不包括在内。在本文中，我们给出了一个更抽象的链接模式，与链接的入侵者的特殊能力表示为演绎规则。此外，我们使用一个自由项代数反对的重写系统所使用的协议分析器。这导致了一些技术 上 的 困 难 ， 我 们 将 在 解 释 我 们 的 模 型 时 讨 论 。 据 我 们 所 知 ，Stubblebine和Meadows还有其他一些作品，如[11，20]，强调了在没有附加完整性机制的情况下使用链接模式时可能出现的问题。然而，这些作品并没有使用自动化工具来发现此类攻击。纲要第二节给出了已知对攻击和选择对攻击的基本概念，包括符号、定义等。我们还解释了块链接技术，并显示攻击者如何使用这些技术的特殊属性。在第3节中，我们简要介绍了Blanchet的协议验证器，我们使用它来自动化我们的分析。我们将已知对和选择文本攻击定义为向工具提供的查询，并在协议验证器中编码与块链接相关的特殊攻击者功能。在第4节中，我们将介绍我们在两个著名的协议上所做的工作，即Needham-Schroeder-Lowe公钥协议和Needham-Schroeder公钥协议。我们演示了该工具查找已知对和选择文本攻击以及与扩展攻击者功能相关的保密攻击的能力。为了方便其他人复制我们的工作并可能进一步发展，我们将我们的分析以电子方式提供4。最后，在第5节中，我们结束。2已知对、选择文本攻击和块链接在本节中，我们给出基本的符号，并介绍已知对和选择文本攻击。我们讨论他们的分组密码，这可以是对称或公钥密码系统的框架。当使用分组密码时，明文被分成不同的块，这些块被逐个加密这些加密块使用特殊技术组合或链接由于已知的对或选择的文本必须在块的级别上找到，我们讨论了其中的一些，并展示了攻击者如何利用这些链接技术的一些属性。4http://www.ulb。AC. b e/di/sc si/sk rem er/P air s/S. Kremer，医学博士Ryan/Electronic Notes in Theoretical Computer Science 128（2005）912.1符号在本文的其余部分，我们使用以下符号。第一，第二，我代表实体爱丽丝，鲍勃和入侵者.表达式pk（k）表示对应于秘密密钥k的公共密钥;sEk（m）和sDk（c）分别是对称加密和解密。m使用密钥k。使用密钥k及其公共对应物pk（k）的m的公共密钥解密和加密被写为pDk（c）和pEpk（k）（m）。我们写h（m）用于加密消息m的散列。2.2已知对和选择文本攻击通常，密码的安全性是根据密码分析师提供的信息来评估的（我们假设根据Kerkho然后，存在不同类别的攻击：• 仅密文：攻击者完全没有关于明文的信息;• known-plaintext：攻击者知道明文和密文;• 选择明文：攻击者可以选择他想知道密码的明文;• 选择密文：攻击者可以选择他想要知道明文的密码。请注意，当考虑公钥加密时，加密方案应该始终至少能够抵抗已知和选择的明文攻击，因为这些攻击可以很容易地实现，因为加密密钥是公共知识。选择文本攻击的一种变体是自适应选择文本攻击。不同之处在于，当选择文本时，它可能取决于先前的选择。当一个协议可以被执行多次时，只要选择文本攻击是可能的，它就增加了自适应选择文本攻击的可能性。在协议分析的上下文中，我们要检查协议设计者必须对加密函数的使用做出的确切假设是什么。我们不只是将加密函数视为黑盒，而是希望量化所使用的密码应该抵抗上述攻击中的哪一种。因此，我们想验证给定的协议是否允许发动上述攻击之一。请注意，我们并不假装存在已知对或选择文本攻击会破坏协议。如果协议允许这种可能性，则应明确说明所使用的加密函数以抵抗此类攻击。92S. Kremer，医学博士Ryan/Electronic Notes in Theoretical Computer Science 128（2005）2.3块链接技术电子代码簿（ECB）、密码块链接（CBC）、密码反馈（CFB）和输出反馈（OFB）。当使用块密码时（无论是对称密码还是公钥密码），明文首先被分成固定大小的块，对应于加密函数的块大小。 然后将这些块一个接一个地进行拼接。经典的分组链接机制有ECB（电子码本）、CBC（密码分组链接）、OFB（输出反馈）和CFB（密码反馈）。然而，如[13]第285页所述，OFB和CFB不能应用于公钥加密。因此，我们关注ECB和CBC。我们在对称密钥加密上说明了块链接，但这些技术也直接适用于公钥加密。 最简单的链接是ECB。对于明文P1.大小为n× blocksize的P n，对应的密文C1...在密钥k下的C n通过设置Ci= sEk（Pi） （1 ≤ i ≤ n）.CBC代表了一种更精细的链接方式。在CBC中，每个块的大小取决于前一个块的密码，计算如下：Ci=sEk（Pi<$Ci−1）（1≤i≤n）其中C0=IV，初始化向量。为了解密这样的消息，我们计算Pi=sDk（Ci）<$Ci−1其中，n表示逐位异或，其自身抵消。根据[13]，IV的保密性不是安全性所必需的，尽管保密性可能被用来确保IV在下文中，我们假设，不是秘密的，并且不使用附加的机制来确保其完整性或保密消息的完整性。我们支持这样的观点，即如果需要额外的机制来确保消息的完整性，例如加密哈希，那么它应该在协议描述中明确说明。我们现在解释攻击者如何篡改使用ECB或CBC的密码消息很容易看出，如果使用ECB，攻击者可以提取任何密码块并组成一个新的序列。 给定一个密文C1...例如他可以提取密码C i Cj（1 ≤i≤j≤n）对应于Pi... P j。 以类似的方式，攻击者可以删除一些块并获得C1. Ci Cj.C n（1 ≤i< j ≤n），对应于P1. Pi Pj. P n. 攻击者可以甚至重新组合不同信息的一部分，S. Kremer，医学博士Ryan/Electronic Notes in Theoretical Computer Science 128（2005）93我钥匙此外，当Ci和Pi都已知时，我们立即有一对Pi，sEm（Pi），这在使用CBC时由于异或运算而不是这种情况。当使用CBC时，改变消息和获得配对可能看起来更困难。然而，正如我们现在将要展示的，有几个属性可以利用。一个已经被注意到并自动化的属性，[23]是一个有效密码的任何前缀也是一个有效密码：给定C1. Cn，C1... C i（1 ≤i≤n）是对应于第i个块的加密的有效密码。可能不太明显的是，人们也可以重用一个有效的密码我们所需要做的就是将IV设为C i，我们就得到了一个有效的密码C i+1. C n对应于最后n-i个明文块的加密。当使用公钥加密方案时，还有一个额外的属性可以被利用。 给定任何密码C1... C i的明文P1.我们可以得到一个有效的密码C1Cn对应于明文P1.其中最后n-i个明文块是自由选择的。这样做会产生一个我们不知道开头的有效密文即第i个块。请注意，这是唯一可能的，因为加密密钥是已知的。当使用对称加密时，它将不起作用，除非我们在不感兴趣的情况下，因此解密密钥也是已知的。然而，存在一个类似的性质，它也适用于对称的情况。给定C1，... C n和CJ...攻击者可以将这两个密码连接起来。 解密重新-1nJ J J导致P1... Pn，X，P2... PnJ，其中X = sDk（C1）<$C n是一个随机外观块，因为它没有被正确解密。在[11]中，这个属性被用来寻找新的随机数，因为X可以被接受为一个新的随机数或密钥。除了使用CBC为攻击者提供了新的功能之外，我们还将展示如何在以下情况下发现已知对或选择文本攻击：CBC使用。由于CisEk（Pi），获得一个对不是直接的。 但如果我们已知Pi，Ci和Ci−1，我们可以计算Ci的解密为：sDk（Ci）=Pi<$Ci−1并获得已知对。这种相同的技术可以用于选择密文攻击以恢复块的解密。在选择明文攻击中，我们希望获得给定块Pi的加密。 为了做到这一点，插入PJ=Pi<$Ci−。实际上，当应用加密算法时，1对于块PJ的CBC，我们得到sE（PJC）= sE（P）.kii−1k i上面描述的在下文中，我94S. Kremer，医学博士Ryan/Electronic Notes in Theoretical Computer Science 128（2005）我们假设所有字段的大小都是块大小的倍数。这意味着我们可以随时在正确的位置“剪切”消息，需要填充以实现正确的块大小。虽然这个假设可能是不切实际的，但我们希望验证协议的安全性在最坏情况下的行为，并且不依赖于未声明的实现假设。还请注意，当使用公钥加密时，1024位RSA块不太可能与随机数大小相同。然而，基于椭圆曲线的公钥加密使用更小的密钥和块大小，使得大小匹配更加真实。在这些假设下，我们得出结论，当知道密文和相应的明文时，总是可以得到每个块的明文和相应的加密。此外，给定一个选定的密码块，我们知道如何将其正确地集成到消息中，以便在获得消息的解密时，我们可以提取选定块的解密。在第3节中，我们展示了如何以抽象的方式扩展攻击者3协议验证工具和我们的模型在本节中，我们简要介绍了我们用来自动化分析的工具。我们使用Blanchet尽管我们相信许多其他工具可以很容易地扩展到执行类似的分析，但我们的选择是基于以下论点：协议验证器不限制会话的数量，非常有效，最重要的是允许我们对攻击者的能力进行编码，而无需修改工具本身。3.1协议描述每个协议都由一组Prolog规则描述，其中协议消息由术语组成。对于详细的语法，我们请读者参考[1]。加密原语由函数表示。作为示例，加密被建模为具有两个参数（明文和密钥）的函数。密码系统是根据自由项代数建模的，这意味着我们不显式地对解密建模。只有显式加密的项才能被解密。密钥是名称，而随机数是由给定协议会话中先前接收到的消息参数化的名称，以便模拟新名称的生成（即使这比真正创建新名称稍微弱S. Kremer，医学博士Ryan/Electronic Notes in Theoretical Computer Science 128（2005）95公钥由一个函数表示，该函数将私钥映射到相应的公钥，即只要知道秘密密钥，就可以推导出还有一个特殊的谓词att（m），它被解释为协议消息本身被编码为Prolog规则，每个消息一个直觉是入侵者完全控制了网络，每个消息都被发送给他。因此，协议预见的每个消息允许攻击者增加他的知识，只要攻击者知道该实体在协议中应该接收的所有先前消息。这是为了确保诚实的协议实体不能无序地执行协议所必需的。作为一个例子，考虑由Lowe [9]固定的经典Needham-Schroeder公钥协议，在其三个消息版本中，如协议1所述。方案1Needham-Schroeder-Lowe公钥协议1. A→ B：pEpk（B）（NA， pk（A））2. B→ A：pEpk（A）（NA，NB， pk（B））3. A→B：pEpk（B）（NB）这个协议描述为我们提供了以下一组规则，对应于三个消息中的每一个。att（pk（x））att（pEpk（sB[]）（NA[pk（x）]，pk（sA[]）att（pEpk（sB[]）（x，y））att（pEy（x，NB[x，y]，pk（sB[]）att（pk（x））attatt（pEpk（sA[]）（NA[pk（x）]，y，pk（x）att（ pEpk（x）（y））在第一条规则中，对应于第一条消息，我们要求攻击者知道实体x的某个公钥。这反映了Alice愿意与任何其他实体进行会话的事实因此，我们允许攻击者触发Alice的协议执行，选择她与谁一起当这样做时，攻击者学习协议的第一条消息我们分别用sA []（sB []）来表示Alice注意，随机数NA由pk（x）参数化以确保不同的随机数用于每个会话。还要注意的是，我们通过公钥对实体名称进行建模，这是协议的一种第二条规则是，每当入侵者可以提供一个用Bob的公钥加密的对（x，y第三条规则的解释也是类似的。96S. Kremer，医学博士Ryan/Electronic Notes in Theoretical Computer Science 128（2005）att（m）att（h（m））att（m）att（k）att（sEkatt（sEk（m））att（k）att（m）att（x）att（pk（x））att（m）att（pk（k））att（pEpk（k）（m））att（pEpk（k）（m））att（k）att（m）图1：标准攻击者能力3.2攻击者能力我们现在定义攻击者以Dolev-Yao风格构造和分解消息入侵者的能力以类似于协议消息本身的方式编码为Prolog规则在图1中，我们展示了与标准攻击者能力相对应的攻击者规则。 第一条规则对应于攻击者的能力散列一个消息。第二和第三规则表示对称密钥加密和解密。其余的规则对应于公钥操作，应该是明确的。攻击者还可以执行我们没有明确提到的基本操作，例如串联，生成新项等。此外，我们还可以向攻击者提供初始知识添加消息m到攻击者在图2中，我们描述了额外的功能，当我们假设加密使用CBC模式或ECB模式5时，我们授予攻击者这些功能。当使用CBC时，我们允许攻击者在给定消息加密的情况下，分别提取这条信息我们在第2节中解释了这是如何实现的。在这个抽象模型中，我们假设所有的消息要么是原子的，要么是原子消息的串联。即使在现实生活中，这可能是可行的，并且可以用于发动微妙的攻击，也不可能剪切原子消息。如第2节所述，当使用公钥加密时，如果加密密钥已知，则还可以扩展加密消息这是由第三条规则反映的。在第四条和第五条规则中，我们模拟了这样一个事实，即通过引入一个新名称rnd来产生一个随机外观的块，这取决于解密时错误合并的两个块。当ECB用作链接技术时，我们添加了类似的功能。5如图所示，对这些攻击者模型进行编码稍微复杂一些，因为我们必须在函数内部使用配对运算符，而不是在元组上进行运算S. Kremer，医学博士Ryan/Electronic Notes in Theoretical Computer Science 128（2005）97密码块链接：att（sEk（m，n））att（sEk（m））att（pEpk（x）（m，n））att（pEpk（x）（m））att（pEpk（x）（n））att（pEpk（x）（m））att（n）att（pk（x））att（pEpk（x）（m，n））attt（sEk（m，n））attt（sEk（mJ，nJ））att（sEk（m，n，rnd[n，att（pE（m，n））att（pEpk（x）pk（x）（mJ，att（pE（m，n，rnd[n，mJ]，nJ））pk（x）电子码本：att（sEk（m，n））att（sEk（m））att（sEk（n））attt（sEk（m））attt（sEk（n））att（pEpk（x）（m，n））att（pEpk（x）（m））att（pEpk（x）（n））att（pEpk（x）（m））att（pEpk（x）（n））att（pEpk（x）（m，n））图2：由于块链接而3.3物业规格Blanchet人们可以验证的最直接的属性是保密属性。如果我们想知道一个协议是否保证秘密s，我们验证att（s）不能被推导出来。此外，只要s可以从规则中导出，该工具就会显示导出跟踪。我们感兴趣的是验证协议是否存在已知对或选择文本攻击的可能性，以确定对原语需要什么样的假设。现在我们将证明这些不同的攻击可以被形式化为保密属性。已知对攻击记住，为了发起已知对攻击，我们需要知道密文和相应的明文。因此，我们说协议允许关于密钥k的已知对攻击，如果对于某个x可以推导出att（sEk（x），x）。98S. Kremer，医学博士Ryan/Electronic Notes in Theoretical Computer Science 128（2005）选择明文攻击为了让攻击者能够发起选择明文攻击，攻击者应该能够将协议用作预言机，并选择要加密的任何明文。我们通过给攻击者一个挑战来建模，也就是说，我们给他的知识添加一个特殊的名称，称为挑战，这是一个从未被任何协议参与者使用的明文。如果攻击者成功地加密了这个挑战，我们可以得出结论，他可以对他选择的任何明文这样做。我们说一 个 协 议 允 许 对 密 钥 k 进 行 选 择 明 文 攻 击 ， 如 果 给 定 att（challenge[]），则可以推导出att（sEk（challenge[]））。选择密文攻击选择密文攻击的形式与选择明文攻击类似这个想法是，我们给攻击者的挑战是一个密文，他不知道明文。由于我们在自由项代数中，我们不能表示挑战是密文;相反，我们给攻击者加密的挑战，并要求他恢复挑战本身。我们说一个协议允许对密钥k的选择密文攻击，如果给定att（sEk（challenge[]）），则可以推导出att（challenge[]）。公钥加密函数的查询与此类似。我们现在可以简单地将我们的定义与Stubblebine和Meadows的定义进行首先， 我们 使用挑战的 想法来建模 选择文本 攻击。 Meadows 和Stubblebine使用了一个特殊的函数not sent，使攻击者能够选择一个值。然而，这个函数的定义相当棘手。其次，我们不需要解密来定义选择密文攻击。让攻击者知道挑战的加密，并要求他产生挑战本身，这就抓住了选择密码攻击的概念。4分析在这一节中，我们举例分析了两个著名的协议：Needham-Schroeder-Lowe公钥协议和Needham-Schroeder公钥协议。4.1Needham-Schroeder-Lowe公钥协议方案描述见方案1。我们认为读者熟悉它的主要思想。我们的分析揭示了两件事。一方面，我们表明，给予攻击者与块链接相关的额外功能，S. Kremer，医学博士Ryan/Electronic Notes in Theoretical Computer Science 128（2005）99攻击者危及协议中使用的随机数的保密性。另一方面，该协议允许攻击者进行选择密文攻击。然后，我们展示了协议的一个轻微变化，它只需要改变第一条消息中字段的顺序来防止这两种攻击。一种危及随机数我们首先展示攻击者如何学习Alice的nonce。该攻击基于攻击者从密文中提取前缀并将后缀添加到现有密文的能力。攻击在攻击1中呈现，其中I表示攻击者或入侵者。攻击者开始观察Alice和Bob之间协议会话中的第一条消息。然后，攻击者从该消息中提取pEpk（B）（NA）。 为此，他采取了前缀的密文由于攻击者知道Bob消息pEpk（B）（NA，I）。记住，这是可能的，通过加密他的身份，并考虑pEpk（B）（NA）的最后一块作为IV。现在，攻击者可以自己与Bob开始会话，Bob解密未知内容然后用攻击者的公钥将其加密后发送回去攻击1一次危及爱丽丝随机数秘密的攻击1. A→B：pEpk（B）（NA，B）2. 从pEpk（B）（NA，B）中提取pEpk（B）（NA），构建pEpk（B）（NA，I）3. I→ B：pEpk（B）（NA，I）4. B→I：pEpk（I）（NA，NB，pk（B））一个更简单的攻击可以用来学习鲍勃在这里，在-tacker观察协议的第三个消息，即pEpk（B）（NB）。从这个消息中，攻击者构造pEpk（B）（NB，I），开始与Bob的新会话，并完全按照前一次攻击进行注意，在这次袭击中，我们甚至不需要从消息中提取前缀。我们描述了攻击2中的场景。选择密文攻击我们现在展示如何对Bob的密钥发起选择密文攻击攻击再次基于对现有密文进行后修复的想法假设我们给入侵者密文pEpk（B）（挑战）。为了成功，攻击者只需要能够恢复平原-短信挑战攻击者可以通过以下方式实现这一点。首先，他构造消息pEpk（B）（challenge，I），然后启动与Bob的协议会话。Bob将接受加密的质询作为攻击者100S. Kremer，医学博士Ryan/Electronic Notes in Theoretical Computer Science 128（2005）B攻击2一次破坏鲍勃随机数秘密的攻击1. A→ B：pEpk（B）（NA，B）2. B→ A：pEpk（A）（NA，NB， pk（B））3. A→ B：pEpk（B）（NB）4. 从pEpk（B）（NB）构建 pEpk（B）（N B，I）5. I→B：pEpk（B）（NB，I）6. B→ I：pEpk（I）（NB），NJ，pk（B））nonce并将发送回其解密，用入侵者的私钥加密。这种情况出现在攻击3中。注意，没有针对Alice的私钥的选择密文攻击（即针对充当协议发起者的人的私钥）。入侵者当然可以与Alice开始一个会话，其中Alice扮演Bob攻击3对Bob私钥的选择密文攻击1. 从pEpk（B）（激发）构建pEpk（B）（激发，I）2. I→ B：pEpk（B）（攻毒，I）3. B→I：pEpk（I）（攻毒，NB，pk（B））更健壮的协议在使用CBC的情况下，存在避免上述潜在攻击的简单方法。如果我们仔细观察它们，我们会发现它们都是基于这样一个事实，即第一条消息可以通过将攻击者的身份附加到未知随机数的加密中来伪造。一个简单的变化包括在第一个领域反转随机数和身份，这给了我们消息pEpk（B）（B，NA），而不是pEpk（B）（NA，B）。由于消息的未知部分，即随机数，是最后一个字段，因此我们不能使用相同的“技巧”CBC就像以前一样。不可能在加密文本中添加前缀，因为IV将不再匹配。但是请注意，当ECB用作块链接模式时，我们的fix没有帮助。如果我们使用从右到左而不是通常的从左到右CBC，也没有帮助。事实上，改变场的顺序可以避免上述攻击，这是一种好奇心，而不是真正的固定。更好的协议做法是通过消息的加密散列来确保消息的完整性，该散列可以包括在密码中。我们通过添加这个额外的完整性机制来改变协议，即我们系统地用pEpk（x）（m，h（m））替换pEpk（x）（m此修改版本可抵抗上述所有攻击。S. Kremer，医学博士Ryan/Electronic Notes in Theoretical Computer Science 128（2005）1014.2Needham-Schroeder对称密钥协议让我们首先简要描述经典的Needham-Schroeder对称密钥协议[15]，我们将其用作第二个案例研究，说明已知对和选择明文攻击的分析Needham-Schroeder对称密钥协议1. A→ S：A，B，NA2. S→ A：sEKAS（NA，B，KAB， sEKBS（KAB，A））3. A→ B：sEKBS（KAB，A）4. B→ A：sEKAB（NB）5. A→B：sEKAB（NB−1）该方案在方案2中描述。 它使用可信密钥服务器S在Alice和Bob之间建立共享密钥KAB。 假设服务器与每个实体共享长期密钥。在第一条消息中，Alice请求服务器生成一个密钥，供Bob和她自己共享。服务器通过发送回密钥以及为Bob加密的密钥来回答。此外，使用随机数NA来确保新鲜度。然后Alice在消息3中将加密的密钥发送给Bob。消息4和消息5是一个挑战-响应握手，以确保Alice知道密钥并且密钥是新的。注意通过声明一个函数decrease（）来模拟NB−已知对攻击对长期密钥KAS和KBS的已知对攻击是简单的。为了找到这样的配对，攻击者甚至不需要任何特殊的能力。当Alice开始与攻击者的会话时，发现关于KAS的已知对。当交换了第一个消息后，攻击者就知道了在第二个消息中加密的所有元素，因为第三个消息直接发送给攻击者，他可以提取共享密钥KAI。为了学习关于Bob的长期密钥K BS的已知对服务器当分析协议对会话密钥KAB的已知对攻击时，该工具提出了错误攻击。这意味着我们既不能断定存在攻击，也不能断定协议是安全的。然而，当我们禁用攻击者连接两个密文的能力，生成一个随机块，没有已知对攻击是可能的，对建立的会话密钥KAB。令人惊讶的是，该协议提供了更多的攻击长102S. Kremer，医学博士Ryan/Electronic Notes in Theoretical Computer Science 128（2005）术语密钥比会话密钥更安全，会话密钥的安全级别应被认为更低。选择明文攻击当我们不添加额外的攻击能力时，选择明文攻击是不可行的。然而，当我们允许入侵者从sEk（m，n）推导出sEk（m）和sEk（n）时，这两个长期密钥可以再次被攻击。我们首先描述对KAS的攻击，其中攻击者必须学习该密钥下的挑战的加密。该攻击在攻击4中呈现，其中符号A（I）表示攻击者伪装成Alice。请注意，这种攻击只涉及服务器的存在，而不是Alice或Bob的存在。因此，同样的攻击可以直接重复使用，对Bob的长共享密钥发起攻击攻击4对Alice长期密钥的选择明文攻击1. A（I）→S：A，B，挑战2. S →A（I）：sEKAS（攻毒，B，KAB，sEKBS（KAB，A））3. I提取sEKAS（激发）5结论在本文中，我们报告了已知对和选择文本攻击的自动分析。为此，我们给出了这些攻击的可达性的定义。特别是，我们在定义选择文本攻击时使用了挑战的概念。由于已知对攻击和选择文本攻击是在块级别上进行的，我们对两种块链接技术ECB和CBC进行了建模。这些块链接技术以抽象的方式建模，而不需要使用演绎规则实际建模CBC的异或操作。我们的方法是自动使用Blanchet的协议验证器，并说明了两个著名的例子，Needham-Schroeder-Lowe公钥协议和Needham-Schroeder公钥协议。在第一个协议中，我们展示了与链接相关的特殊入侵者能力如何可能危及随机数的保密性，并且选择密文攻击是可能的。我们提出了两个修改版本的协议，加强其安全性。然后，我们说明了已知对和选择明文攻击的Needham-Schroeder对称密钥协议。作为未来的工作，我们预计将这些技术应用到现实生活中的协议，这精确的链接技术的使用。一个有趣的案例研究将是，因为它是基于这里研究的李约瑟-施罗德S. Kremer，医学博士Ryan/Electronic Notes in Theoretical Computer Science 128（2005）103对称密钥协议此外，我们相信，额外的攻击能力，使我们能够发现新的猜测攻击。考虑使用（确定性）公钥加密来加密弱数据w的协议，即pEpk（x）（w）。一个简单的猜测攻击是猜测wJ，并通过以下方式验证该猜测：J重新加密w 并与原始密码进行比对 在添加一个加密内的新随机数，即pEpk（x）（N，w），这将使这种猜测攻击在标准模型中是不可能的，我们的额外攻击能力会让攻击变得可行确认作者希望感谢匿名评论者提供的有用评论，以及Bruno Blanchet在使用他的工具时提供的宝贵建议。我们非常感谢EPSRC的资助编号GR/R02214/01，引用[1] Blanchet，B.，一个基于Prolog规则的高效密码协议验证器，S.Schneider，editor，14th IEEEComputer Security Foundations Workshop（2001），pp. 82-96.[2] Chevalier，Y.，R. Kuester，M. Rusinowitch和M. Turuani，一种基于异或的协议不安全性的，在：P。G. Kolaitis，编辑，Symposium on Logic in Computer Science（LICS261-270。[3] Comon-Lundh，H.和V.Shmatikov，在存在异或的情况下的入侵者扣除，约束求解和不安全决策，在：P.G. Kolaitis，编辑，Symposium on Logic in Computer Science（LICS第271-280页。[4] 科林河，S. Malladi，J.Alves-Foss和S.Etalle，猜猜怎么着？ 这是一个新的工具，发现了一些新的猜 测 攻 击 （ 扩 展 抽 象 ） ， 在 ： R 。 Gorrieri 和 R.Lucchi ， editors ， In Proceedings of theWorkshop on Issues in the Theory of Security（WITS62-71.[5] Delaune，S.和F.Jacquemard，字典攻击及其复杂性的理论，在：R. Focardi，editor，17th IEEE Computer Security Foundations Workshop（2004），pp. 2比15[6] Dolev ， D. 和 A. C. Yao ， On the Security of Public Key Protocols ， IEEE Transactions onInformation Theory 29（1983），pp. 198-208.[7] Durgin ， N. 一 、 P. D. 林 肯 ， J.C. Mitchell 和 A. Scedrov ， Multiset Rewriting and theComplexity of Bounded Security Protocols，Journal of Computer Security（2002）。[8] Guttman，J.D.，“安全分析和设计的基础”，计算机科学讲义2171，Springer-Verlag，2001年，第101页。197-261[9] Lowe，G.，对Needham-Schroeder公钥认证协议的攻击，信息处理快报56（1995），pp.131比133[10] Lowe，G.， 分析遭受猜测攻击的协议。，in：J.Guttman，editor，In Proceedings of theWorkshop on Issues in the Theory of Security（WITS[11] 毛，W。和C. Boyd，关于加密协议中加密的使用，在：第四届IMA密码学和编码会议论文集，Cirencester，英格兰，1995，pp. 251-262.104S. Kremer，医学博士Ryan/Electronic Notes in Theoretical Computer Science