公钥加密在密码协议分析中的重要性及扩展性研究

理论计算机科学电子笔记125（2005）43-54www.elsevier.com/locate/entcs公钥加密克里斯托弗·林奇1，2克拉克森大学数学与计算机科学系邮编：13699-5815凯瑟琳·梅多斯3海军研究实验室高保证计算机系统中心代码5543华盛顿特区，邮编20375摘要用于密码协议分析的形式系统通常根据自由代数来建模密码系统然而，根据重写规则对密码系统的行为进行建模更具表达性，并且有一些攻击只有在使用重写规则时才能被发现。 但是自由代数更有效，并且似乎对“大多数”协议都是合理的。在[9]中，Millen将这种直觉形式化为共享密钥密码学，并提供了它成立的条件;也就是说，协议的自由代数版本的安全性意味着使用重写规则的版本的安全性的条件此外，这些条件与协议设计的公认最佳实践非常吻合。然而，他留下了公钥密码学作为一个开放的问题。在本文中，我们将展示如何米伦的方法可以扩展到公钥密码学，给出条件下，安全的自由代数模型意味着在共享密钥加密的情况下，我们的条件对应于协议设计的标准最佳实践保留字：加密协议验证。1这项工作是在作者访问海军研究实验室2 电子邮件地址：clynch@clarkson.edu3 电子邮件地址：meadows@itd.nrl.navy.mil1571-0661 © 2005由Elsevier B. V.出版，CC BY-NC-ND许可下开放获取。doi：10.1016/j.entcs.2004.05.01844C. 林奇角，澳-地Meadows/Electronic Notes in Theoretical Computer Science 1251介绍在大多数用于密码协议分析的形式化系统中，通常用自由代数来表示加密操作。例如，加密可以表示为e（K，X），其中K是密钥，X是明文。然而，解密是隐式表示的。例如，可以包括这样的规则：如果主体知道共享/对称密钥K和e（K，X），则它也可以学习X。另一种方法是显式地表示加密和解密加密用e（K，X）表示，而解密用d（K，X）表示.解密撤销加密的事实可以由取消规则d（K，e（K，X））=X表示。由于解密运算符也可以用于未加密的数据，并且当反向应用时，这些运算也可以抵消，因此我们还可以包括规则e（K，d（K，X））=X。这种明确性导致了更大的表现力，无论是在协议表示和构造攻击。例如，在[5]中，Meadows分析了一个在自由代数模型中无法指定的协议，因为它需要将解密运算符应用于未加密的数据。即使协议不需要以这种方式显式表示解密运算符，它们仍然可能受到需要使用它的攻击。例如，在[9]中，Millen给出了一个在自由代数模型中安全但在解密扩展模型中不安全的协议的例子。然而，取消的明确表示，虽然更有表现力，但可能导致效率较低的分析。此外，许多实际的协议似乎是免疫基于取消的攻击。诸如可识别格式、概率加密等技术似乎使取消规则的意外应用变得不太可能。因此，大多数用于密码协议分析的形式化系统都使用自由代数模型，尽管它们对这种方法提供了很少的形式化证明在[9]中，Millen通过给出使用对称加密的协议的必要和充分条件来解决这个问题，在该条件下，如果保密性对于自由代数模型中的协议成立，则它在解密扩展模型中也成立。该条件在基于参数串空间和模式匹配的模型中编写的协议上指定它有两个子条件。第一个，称为纯度，说明解密操作符不应该出现在协议规范中。第二种称为EV-freeness，即不能将加密运算符应用于规范中的变量。EV-free属性本质上说，主体不应该将加密运算符应用于术语，除非它能够验证C. 林奇角，澳-地Meadows/Electronic Notes in Theoretical Computer Science 12545该项具有某种结构，使得它不会不知不觉地将加密运算符应用于应用解密运算符的结果。由于通常认为只对已知的数据进行加密是一种良好的做法（例如，它是满足某些格式约定的数据，或者是自己创建的数据），因此可以合理地期望大多数加密协议都能满足EV自由性。虽然米伦承认类似的结果可能适用于公钥密码学，但他将其作为一个开放的问题。在共享密钥加密中，有可能构建容易受到依赖于取消规则的攻击的协议例如，考虑诸如RSA的密码系统，其中签名和解密是相同的操作。在这种情况下，我们有身份pke（privkey （U ），pke（pubkey（U），X））=X，其中pke是公共加密，pubkey（U）是U的现在考虑一个简单的公证协议，其中服务器愿意签署它收到的任何消息假设有人用服务器的公钥加密消息m这种攻击依赖于公钥加密的取消属性，没有它就无法表示。但大多数使用公钥加密的实际协议也不受这种类型的影响的攻击。通常，用于签名的公钥对与用于加密的公钥对不同，并且数字签名应用于消息的单向散列，而不是消息本身。最后，从不签署完全由另一方提供的消息被认为是合理的程序。相反，委托人通常被要求在签署之前添加一些自己的材料。这样的观察使我们相信，应该有可能将Millen的结果扩展到公钥密码学，基于我们对上述普遍接受的设计原则的限制。我们的第一个公钥纯度，类似于Millen其中第二个，类似于EV自由，称为PEV自由，是加密或签名运算符的出现不包含变量作为参数。我们还介绍了第三个条件，称为结构，这是足够的，没有其他两个，这意味着没有出现的加密或签名操作符包含作为参数的变量或一个以公钥操作符为根的术语。请注意，对于不同类型的操作使用不同密钥对的要求假定：46C. 林奇角，澳-地Meadows/Electronic Notes in Theoretical Computer Science 125CIPAL知道哪些密钥对用于什么，因此排除了包括公钥分发的协议。然而，当我们只需要结构时，情况并非如此本文的其余部分组织如下。在第二节中，我们介绍了模型。在第三节中，我们证明了公钥纯、无PEV协议的可靠性结果在第4节中，我们描述了我们的计划，进一步的工作，并作出一些说明。由于篇幅限制，我们无法在本文件中列入许多技术材料所有的证明都被遗漏了，所有关于结构化协议的材料都被遗漏了。包含所有这些材料的完整论文可以在www.clarkson.edu/~clynch/papers/pubfree.ps/2协议模型2.1Millen和Shmatikov像Millen一样，我们使用基于Cervesato等人[1]和Song等人[12]中使用的参数链的模型，以及Millen和Shmatikov在[10]中开发的约束求解。关于串空间的定义，我们请读者参考[3]。在参数串中，消息项可以包含变量。 变量对应于出现在负节点的消息项的子项，接收者无法验证其属性;因此任何项都可以用来替代它。变量也可以出现在链的正节点中，但前提是它们之前出现在负节点中。定义2.1约束是一对m：T，其中m是项，T是项集。如果对所有m：T∈C，入侵者可以从T σ导出mσ，则通过替换σ满足一组约束C。约束和项集的集合可以从半丛B中的正节点和负节点的序列构造，该半丛B与由丛排序施加的偏序每一个积极的节点都会扩大每个负节点创建一个约束m：T，其中m是节点中的消息，T是最后一个项集，第一个项集是入侵者最初已知的项集。这样一个约束集被一个替换σ满足，当且仅当，对于紧挨在负节点m之前的约束的每个初始序列s，入侵者可以从sσ中的正节点生成mσ。换句话说，σ满足约束集，当且仅当入侵者可以从诚实主体发送的所有先前消息和入侵者最初已知的所有信息中生成诚实主体所期望的消息。当然，这正是我们如何使用串空间来构造对C. 林奇角，澳-地Meadows/Electronic Notes in Theoretical Computer Science 12547一个协议。这使得在与约束相容的意义上定义丛成为可能。定义2.2半丛是参数链的集合。半丛中节点的全序与半丛相容，如果在串上，只要N1在N2之前，则N1N2。<<定义2.3丛是一个半丛B，使得在与B相容的节点上存在一个全序，使得由导出的节点序列产生的约束集满足。<<一个半丛是可解的，如果存在某个丛，其中嵌入了该半丛的某个基实例。在[9]中，Millen描述了两个约束系统。一种是基于一个自由的代数，与入侵者运营商组成的级联，解级联，加密和加密的逆转。另一种是基于一个代数（称为解密扩展代数），其中包括取消规则描述的加密和解密的相互影响，和渗透运营商组成的级联，解级联，加密，加密的逆转，和解密运营商的应用。这篇论文的主要定理是，在一定条件下，任何在第二个系统中可解的丛在第一个系统中也可解。这归结为显示- ing在什么条件下，约束m：T从自由代数是可解的取消代数也可解的自由代数。在[9]中，这些条件是从中导出约束的协议不应包含任何显式使用的解密运算符（纯度），并且它不应包含应用于变量的加密运算符（EV-freeness）。注意，自由代数中的可解性总是给我们解密扩展代数中的可解性，因此结果是一个如果且仅如果。此外，由自由代数的解导出的解密扩展代数的解不引入属于诚实主体的链。这对我们可以证明的定理的类型有一个结果，正如我们将在下面看到的。Millen在[9]中描述了如何使用这个结果来证明自由代数相对于解密扩展代数的保密性质是合理的。人们可以创建一个特殊的链，描述入侵者学习特定的秘密，例如密钥。人们可以用他的定理来证明，纯粹性和EV-自由性意味着入侵链在消去代数中是可解的，当且仅当它在自由代数中是可解的。Millen还提到，这个结果可以用来证明某些身份验证属性的可靠性，尽管他没有详细说明这一点。48C. 林奇角，澳-地Meadows/Electronic Notes in Theoretical Computer Science 125我们想描述的攻击类型，米伦为此，我们在下面定义了一种攻击定义2.4我们将攻击规范定义为两组参数链，称为正集和负集。地面攻击规范是所有术语都是地面的攻击规范简单地说，攻击规范的正集合给出了应该在束中的链，负集合给出了不应该在束中的链。因此，对发起者接受的密钥的秘密性的攻击的具体化可以用包含两个链的正集合来给出：一个是发起者链，其中密钥由变量K表示，另一个是米伦描述的特殊入侵者链，其中入侵者学习的数据也由K表示。负集将是空的。然而，认证协议的规范将包括正集合中的认证链和负集合中的认证链。攻击规范的概念在[10]中没有明确阐述，但我们的定义抓住了Millen和Shmatikov在其约束系统中处理的攻击类型的本质。然而，我们注意到，米伦和什马蒂科夫将自己限制在地面攻击规范上，或者至少是正集中的所有项都是地面的攻击规范。我们认为，应该直截了当地将他们的攻击概念扩展到非地面攻击规范。这将使我们能够以某种更普遍的方式来描述攻击。然而，当重写规则被用来描述密码系统的属性时，问题变得稍微复杂一些，因为我们需要跟踪攻击规范中的哪些项被假设为不可约，哪些项可以被允许为可约。虽然这并不一定很难做到（类似的事情已经在NRL协议分析器中用于指定不安全状态），但它可能是乏味的，并且有点偏离本文的主要目标。 因此，我们将其视为超出本文的范围，并将其留给进一步的工作。Millen的结果，以及我们的结果，很容易扩展到任何具有空负集的接地攻击规范。它可能并不总是延伸然而，对于非空负集的情况，因为将消去代数映射到自由代数的变换不一定是恒等式，并且在自由代数中的攻击中出现的串可能通过变换被发送到负集中C. 林奇角，澳-地Meadows/Electronic Notes in Theoretical Computer Science 125492.2公钥密码学中的自由代数和扩展代数在米伦的情况下，我们的结果是在两项代数。其定义如下：定义2.5自由代数FA包含(i) 常量pub、priv、enc和sig。它还包含一组名称、一组消息和一组随机数。(ii) 配对运算符[X，Y]和公钥加密运算符pe（X，Y）。pe的第一个参数是key，我们表示为pk（N，P，S），其中• N是密钥的名称（通常是使用该密钥的主体），• P可以是 pub或 priv，表示这是公钥还是私钥，• S可以是enc或sig，表示密钥是用于加密还是用于签名。pe的第二个参数是消息。例如，项pe（pk（A，pub，enc），pe（pk（B，priv，sig），m））表示消息m，用B我们使用这种符号来强制执行这样的假设，即在协议中没有密钥同时用于签名和加密我们只考虑pk运算符的第二个和第三个参数不是变量的协议。这反映了密钥具有固定目的的假设，不可能改变该目的，并且所有主体都将识别密钥的目的是什么例如，在公钥和私钥事先由某个可信协议分发的情况下，这将是有效的由于这是一个假设，许多密码协议分析都是在这个假设下进行的，我们认为这是合理的，至少作为第一个近似值。定义2.6扩展代数EFA，除了上面的，还包括下面的方程组E：E1pe（pk（K，pub，enc），pe（pk（K，priv，enc），X））=XE2pe（pk（K，priv，enc），pe（pk（K，pub，enc），X））=XE3pe（pk（K，pub，sig），pe（pk（K，priv，sig），X））=XE4pe（pk（K，priv，sig），pe（pk（K，pub，sig），X））=X该集合E对加密和签名操作的属性进行建模。设R为重写系统，其结果是将这些方程从左向右定向为重写规则。这可以被证明是一个表示E的连续和终止重写系统，使用类似于那些的技术50C. 林奇角，澳-地Meadows/Electronic Notes in Theoretical Computer Science 125在[5]中。这意味着两项模E等价当且仅当它们具有相同的模R唯一范式。我们定义t↓R为t模R的标准形式。设D为以下推导规则：D1（X，Y）D2（X，Y）D3X，Y（X，Y）D4pe（pk（K，pub，enc），X），pk（K，priv，enc）XD5pe（pk（K，priv，sig），X），pk（K，pub，sig）XD6X，pk（K，pub，enc）压缩（pk（K，pub，enc），X）D7X，pk（K，priv，sig）重复（pk（K，priv，sig），X）列表D表示入侵者可以在自由代数FA中获得信息的方式接下来，我们构建了一组推导规则DE，它表达了入侵者可以在自由代数的方程扩展EFA中学习到什么。我们让DE是包含D的导出规则的集合，不包括规则D4和D5，加上附加规则DE1X，pk（K，priv，enc）压缩（pk（K，priv，enc），X）DE2X，pk（K，pub，sig）压缩（pk（K，pub，sig），X）如果T是一个项的集合，那么我们将DerivD（T）定义为可以使用D的推导规则从T导出的项的集合。我们将DerivDE（T）定义为可以使用导出规则DE从T导出的项的集合。DerivDE的推导以方程理论E为模进行。换句话说，给定一个求导规则t1···tn<$t和一组项s1···sn，那么我们可以导出一个新的项s，如果s=tσ且si=Etiσ，对于所有i，其中1≤i≤n。我们假设在一个导子中使用的代换σ是R不可约的。(If它不是，它总是可以用它的简化形式来代替。在每个推导规则之后，我们将新的项s减少R。注意，这些推导规则类似于Millen[9]为他的秘密密钥结果给出的推导规则。我们只是在这方面与他们不同在DE中，我们没有显式地添加这样的规则：如果秘密加密的消息是已知的，并且如果对应的密钥是已知的，则该消息是已知的。我们不加这个，因为它是一个推导规则和一个归约规则的结果。公开签名的消息也是如此任何可以由D导出的项也可以由DE导出。唯一不明显的是D的规则4和5在DE中不存在。 但这些规则是通过DE的推导加上R的约简来模拟的。C. 林奇角，澳-地Meadows/Electronic Notes in Theoretical Computer Science 125512.3协议规范的语法属性我们现在定义一些基本的协议的语法属性，我们将使用它们来证明我们的结果。定义2.7我们称项t是结构化的，如果每当运算符pe出现在t中时，pe的第二个参数不是变量或以运算符pe为根。结构化术语的一个例子是[4]中的标记消息，其中每个术语前面都有一个描述其类型的标记。另一个例子是一对术语。定义2.8如果一个项t不包含任何项pk（k，priv，enc）或pk（k，pub，sig），其中k可以是任何项，我们称之为公钥纯一组项是pk纯的，如果它的所有元素都是pk纯的。如果协议中出现的所有项都是pk纯的，则该协议被认为是注意所有的pk-纯项都是R不可约的。定义2.9如果没有发生以下情况，则认为方案不含PEV：pe包含一个变量作为参数。3pk-纯度和PEV-游离意味着可靠性在本节中，我们将只考虑pk-pure协议，因为我们希望对解密是隐式的真实协议同样，对签名的承认也是隐含的。我们将证明，如果一个协议是pk-纯的，没有PEV，并且如果T是pk-纯的，那么我们将证明DerivDE（T）≠DerivD（T），这意味着DerivDE（T）=DerivD（T）。这将意味着自由代数模型可以找到扩展模型所做的所有攻击。首先，我们需要一个引理，说明如果一个pk-纯不可约项是PEV-自由的，那么它在应用不可约子项后仍然是不可约的。引理3.1设t是pk-纯PEV-自由项，σ是一个置换，使得σ不可由R约。则tσ不可由R约。我们证明了DE中的所有导子都保持一定的性质。为了做到这一点，我们定义了一个新的重写系统P，它将所有项都减少到一个pk-纯项。(i) pe（ pk（ K，priv，enc），X）→ X(ii) pe（ pk（ K，pub，sig），X）→ X52C. 林奇角，澳-地Meadows/Electronic Notes in Theoretical Computer Science 125我们定义t↓P为t模P的标准形式。注意每个pk-纯项都是模P不可约的。引理3.2设t是pk-纯项，σ是置换项。若σ不可由P约，则tσ不可由P约.这意味着，如果t是pk纯的，则（tσ）↓P=t（σ↓P）定理3.3设s1，···，sn为R不可约项，使得s可由DE中的s1，···，sn一步导出.则要么s↓P可以从D中的s1↓P，···，sn↓P一步导出，并且s不可由R约，要么存在i使得s↓P= si↓P。定理3.4设T是R不可约项的集合。让t成为一个术语。如果t∈DerivDE（T），则t↓P∈DerivD（T↓P）。另外，存在一个s∈DerivDE（T），使得s不可由R约且t↓P= s↓P.推论3.5假设T是一组PEV-自由pk-纯项。 设t是一个pk-纯无PEV基项。设σ是R不可约的代换。如果tσ ∈ DerivDE（T σ），则t（σ ↓P）∈DerivD（T（σ ↓P））。推论3.6设Pr是一个pk-pure-pev-free协议。设B是Pr的半丛。如果B是EFA中的丛，则它是FA中的丛。4结论本文将Millen关于共享密钥加密的自由加密模型的可靠性的结果推广到公钥加密。虽然证明在一些重要的方面不同于米伦的，但我们发现他的一般方法可以很好地扩展到公钥密码学。此外，我们发现，我们的结果，类似于米伦除了我们在前一节中提到的利用非空负集攻击规范之外，最明显的是包括其他最佳实践（例如，使用概率加密），或者将我们的结果扩展到同时使用公钥和单密钥加密的模型，因为今天使用的大多数协议都使用这两种方法。此外，密码算法还有许多其他的特殊性质，如果能够以安全的方式抽象出来，将是有用的。例如，Di Joule-Hellman的交换性质可以大大增加密码协议分析的费用。在[7]中，使用了Di Bie-Hellman的一个规范，它抽象了交换属性，但它的缺点是，由发起者和响应者计算的相同密钥片段将具有C. 林奇角，澳-地Meadows/Electronic Notes in Theoretical Computer Science 12553不同的陈述。如果我们能够保证发起者计算的密钥片段不会与响应者计算的密钥片段混淆，这就不应该是一个问题。我们在这个方向上有一些初步的结果，使用类似于本文中使用的技术其他可能适用于[9]和这里使用的技术的感兴趣的代数事实上，Even等人的早期论文[2]表明，对于一类非常有限的协议（称为乒乓协议），忽略RSA的同态性质是安全的，因此我们知道对于该性质，结果至少在有限的情况下是正确的。将这些结果扩展到已经使用取消规则的系统（例如NRL协议分析器[6]）也是有用的。这将允许我们在必要时使用消去规则，而在不必要时使用更有效的自由代数Millen和我们的论文中所采用的方法一般的目标是有一个层次的协议模型，每个包含不同数量的细节。在给定协议的某些条件下，可以证明较不详细的模型相对于较详细的模型是合理的，并使用较有效但较不详细的模型执行分析。如果条件不满足，则使用更详细的模型。这种方法并不局限于密码系统的更多代数属性;[8]中详细描述的其他可能性包括类型的攻击（由Heather等人在[4]中处理），密钥泄露的可能性和密码模型。我们认为本文中的结果是一个潜在的构建块在这方面。5致谢这项工作得到了海军研究办公室的支持。引用[1] I. Cervesato，N.Durgin，P.Lincoln，J.Mitchell和A.谢德罗夫安全协议分析中的关联链与多重集重写 在proc 第13届IEEE计算机安全基础研讨会。IEEE Computer Society Press，2000.[2] S.甚至，O。Goldreich和A.沙米尔关于使用RSA实现的乒乓协议的安全性。在密码学的进展：密码'85的程序Springer-Verlag，1985.[3] F. Thhaye r F'abrega ， J. .赫 尔 佐 格 和 J.我也 是 。STRANDSPACES ： Whyisasecurityprotocolcorrect ？在 Proc.1998 IEEE Symposium on Security and Privacy ，第 160-171 页中。IEEE Computer Society Press，May 1998.54C. 林奇角，澳-地Meadows/Electronic Notes in Theoretical Computer Science 125[4] J. Heather，S. Schneider和G.洛 如何防止对安全协议的攻击。 在proc 第13届IEEE计算机安全基础研讨会。IEEE Computer Society Press，2000.[5] C.梅多斯应用形式化方法分析一个密钥管理协议。 计算机安全杂志，1（1），1月。一九九二年[6] C.梅多斯NRL协议分析器：概述。Journal of Logic Programming，26（2）：113[7] C.梅多斯使用NRL协议分析器分析Internet密钥交换协议。1999 IEEE Symposium on Securityand Privacy. IEEE Computer Society Press，June 1999.[8] C.梅多斯迈向加密协议规范的层次结构。 FMSE 2003：安全工程中的形式方法。ACM Press，2003.[9] J. Millen关于解密的自由。Information Processing Letters，86（6）：329-333，June 2003.[10] J. Millen和V. Shmatikov。有界进程密码协议分析的约束求解。在Proc.8th ACM Conference onComputer and Communications Security（CCSACM Press，2001.[11] L.保尔森验证密码协议的归纳方法。Journal of Computer Security，6（1）：85[12] D.宋，S. Berizin和A.佩里格雅典娜：一种高效自动证券分析的新方法。计算机安全杂志，9（1）：47