密码协议中的重放攻击和身份验证测试的机械化模式

141理论计算机科学电子笔记45（2001）网址：http://www.elsevier.nl/locate/entcs/volume45.html21页密钥妥协、串空间和身份验证测试*约书亚·D GuttmanThe MITRE CorporationBedford，MA 01730USAguttman@mitre.org摘要一些加密协议容易受到重放攻击，这是Burroughs-Abadi-Needham逻辑中关注的焦点较新的，更实用的协议分析方法并没有集中在这种类型的攻击。本文填补了串空间理论的空白。主要的技术要点是提供一个近因的定义我们的候选项很方便，因为我们已经有了一种强大的方法来证明最近发生的事件，即传入和传出身份验证测试。本文的第二个目的是说明一种易于机械化的使用身份验证测试的模式。关键词：密码协议，认证，认证测试，串空间，捆绑，密钥泄露1介绍一些加密协议容易受到重放攻击，其中来自合法协议执行的消息稍后被重传，通常是当同一主体执行协议的不同会话时。如果消息包含渗透者已经通过密码分析破解的加密会话密钥，则渗透者可以诱导接收者重新使用受损的会话密钥。虽然Burroughs-Abadi-Needham逻辑[1]在识别这些情况方面特别这些包括串空间[7，19]，CSP模型检查[9]和秩函数[8，18]，而保尔森*2001年5月24日，鲍勃·迪伦60岁生日那天，我发表了MFPS 17演讲。这篇论文是献给他的。2000年1月，出版社dbyElsevierScienceB。 V. 在CC BY-NC-ND许可下开放访问。古特曼142⇒→{||}在本文中，我们填补了这个空白的串空间文献。我们表明如何指定密钥服务器的行为，以使最近的密钥保持不被泄露，而较旧的密钥可能已被泄露。在这个模型中，Needham-Schroeder私钥协议[13]是脆弱的，而Yahalom协议[1]则不是。主要的技术要点是提供一个近因的定义。我们的候选人是方便的，因为串空间方法已经有一个强大的方法来证明一个事件是最近的，即传入和传出的身份验证测试[5，7]。本文的一个补充目的是说明认证测试的力量。 它们提供了协议正确性的简单而直接的解释。我们通过几个例子来说明身份验证测试的用法。这些用法模式都是相当定型的，尽管有几种成分可以有效地结合起来。李约瑟-施罗德对称关键议定书在开创性的论文[13]中，Needham和Schroeder提出了一个使用对称密码学的协议和另一个使用公钥密码学的协议。两人都被吓到了。密钥协议NSSK假设每个主体与密钥服务器共享一个长期密钥。它的目的是在两个主体之间建立一个秘密会话密钥，在每个主体都验证了另一个主体的身份之后。方案的预期执行总结见图1。在这个协议中，发起者A向密钥服务器发送一条消息，其中包含他的名字、他的伙伴的名字B和一个随机数Na。nonce是一个新的随机数，只为一次使用而生成。消息使用A和服务器之间共享的长期密钥进行加密。服务器生成一个新的会话密钥K，并用AB票据包含AA将此票据转发给B，期望接收回一个新的用K加密的随机数Nb。A通过返回1 +Nb来证明接收，也用K加密。图1中的图表形状非常引人注目：它由两个矩形组成，由一个“脖子”连接顶部的矩形只包含A和服务器，而底部的矩形只包含A和B，因此服务器在B开始之前完成Denning和Sunday [2]迅速发现了由此导致的故障。虽然B在接收到A，K，K，B时可以推断它是由服务器生成的，但B无法知道自服务器完成以来已经过去了多少时间。这在图1中是几何上明显的，因为B没有可用的测量A的第二节点和第三节点之间的“颈部”的长度从A 所以B不能限制S生成会话密钥K和B接收到会话密钥K之间的延迟。假设A和B在会话中使用K进行加密通信，古特曼143¨····{||}A S-A ，{|B、Na|{\fn黑体\fs22\bord1\shad0\3aHBE\4aH00\fscx67\fscy66\2cHFFFFFF\3cH808080}¨·✛{|B，Na， K，{|A 、K|}KB|}KA·¨B¨{|A 、K|}KB你好|N b|}K·{|1+ N b|{\fn黑体\fs22\bord1\shad0\3aHBE\4aH00\fscx67\fscy66\2cHFFFFFF\3cH808080}Fig. 1. Needham-Schroeder对称密钥协议（NSSK）也许入侵者会对对话进行密码分析以恢复K。在这种情况下，可以通过重新发送相同的单元来启动会话。|A 、K|}KB，稍后返回1+ N bK。 那么B就已经有了。 当K不再是最近产生的时候，K是好的的假设应该过期我们在本文中的目标是制定一个严格的理论，使我们能够证明，一个协议没有这种类型的锯齿。同样的想法也暗示了在我们无法证明它们不存在的时候，找到这样的规律的方法2串空间串空间理论[7，19]是Dolev-Yao模型[3]的一种特殊形式化方法。它假设密码学是理想的，目的是发现认证和保密属性协议，然后实现。在串空间模型中，主体的行为由一组线串是消息发送和接收事件的序列;例如，图1中的每个垂直列都是一个串（对于参数A、B、Na等的每个特定选择）。 渗透者的行为也由串表示;在这种情况下，串表示基本操作，例如使用已知密钥加密或解密或选择随机数。每条链都是某个特定主体在特定场合的纯粹局部行为。如果链的集合在因果关系上是有根据的，那么它们就形成了一个束，这样，接收到的每一个消息实际上都是由某个链先前发送的，没有一个主体在没有执行第一个事件的情况下参与第二个或第三个事件。2.1背景我们全面总结了串空间模型背后的思想[4，7，19];定义包含在附录A中。古特曼144{||}术语和子术语A是可以在主体之间发送的消息集。它的元素，被称为术语，通过连接和加密从两个不相交的集合T（文本，如随机数或名称）和K（密钥）中自由生成。项g和h的级联表示为g，h，并且使用密钥K对h的加密表示为{|H|K. (See附录A.3.）在NSSK中，发起者A发送形式为A，B，NaKA的项，以启动针对B的交换。这是一个包含A密文是使用A项t是另一项tJ的子项，写作t<$tJ，如果从t开始，我们可以通过重复连接任意项并使用任意密钥加密来达到tJ因此，K/i{|不|}K，除了情况K<$t. t的子项是在发送t时发出的值;在{|不|}K，K没有说出但是没用过。（见定义A.7。例如，A的子项s，{|B、Na|}KA是A，B，Na，连接的消息B，Na，密文t{|B、Na|#21453;，以及整个术语本身。密钥KA不是所表达的内容的一部分;它只是对信息的构建做出了贡献。串和串空间串是一个消息传输和接收的序列，其中项t的传输表示为+t，项t的接收表示为-t。strand元素称为节点。如果s是一个链，则s↓i是s上的第i个节点。节点之间的关系n<$nJn和nJ，如果n=s↓i和nJ=s↓i+1。因此，n+nJ意味着n=s↓i对于某些j> i，nJ=s↓j。关系n→nJ代表链间通讯;它意味着项（n）=+t和节点项（nJ）=−t。继续使用NSSK作为我们的说明，引发剂链引发图1最左边一列所示形式的事件序列。在该串si中，发起者A发送旨在用于服务器S的项，并且 期 望 接 收 针 对 m{|B ， Na ， K ， {|A 、 K|}KB|}KA ， afterwhicitwilllforward{|A 、K|KB，然后继续。第一次接收是si↓2，下一次传输是s i↓ 3。一个NSSK发起者串有五个参数（或自由度），即两个名字A和B，两个随机数Na和Nb，以及会话密钥K。当我们在该图中写为si∈Init[A，B，Na，Nb，K]时，我们将意味着si是使用所示的特定值作为参数的起始链，并且对于ss∈Serv[A，B，Na，K]和sr∈Resp[A，B，Nb，K]也是类似的A是Init[A，B，Na，Nb，K]中作为发起者的主要活动，而B是Resp[A，B，Nb，K]中作为响应者的主要活动。我们通常按照这样的顺序写参数：首先是预期参与者的名字，然后是在运行中看到的任何随机数，最后是会话密钥（如果协议分发了一个）。串表示参与者的本地视图。对于一个合法的参与者，一个串代表参与者将发送或接收的消息，作为他这一边协议的一个特定运行的一部分我们称之为股古特曼145↓↓↓⇒→≤/↓↓→⇒代表一个合法的参与者，一个规则的链。一个链空间是一组链。这两个关系和共同将图结构强加于图的节点上。 这个图的顶点是 节点和边是和→的并集。起源我们说一个项t起源于一个节点n =s i，如果n的符号是正的;t<$term（n）;和t<$term（s iJ）对于每个iJ

下载后可阅读完整内容，剩余1页未读，立即下载