理论计算机科学电子笔记128（2005）55-63www.elsevier.com/locate/entcs多协议身份验证Matteo Ma Jingei马泰奥1，2意大利威尼斯Ca'Foscari大学信息学系摘要形式化方法在分析不同类型的安全协议方面已被证明是成功的。他们通常形式化和研究由加密协议提供的安全保证，当由（可能无限）数量的不同参与者执行时。将形式化方法应用于密码协议的一个关键问题是研究多协议系统，其中不同的协议被并发执行。这种情况在全球计算环境中特别有趣，在这种环境中，几种不同的安全服务共存，并且可能组合在一起。 在本文中，我们讨论了[4，5]中提出的标记机制如何解决这个问题。关键词：安全，进程演算，静态分析1介绍安全协议被设计为在可能的敌对环境中提供各种安全保证：典型的保证包括两个可信实体之间的消息交换的保密性，消息的新鲜性和真实性，声明身份的真实性，...... 和更多. 敌对实体的存在使得协议设计复杂并且经常容易出错，如文献中报道的对长期协议的许多攻击所示（参见，例如，[6、7、13、18、19]）。在大多数情况下，这种攻击都集中在协议逻辑中的漏洞上，而不是底层密码系统中的漏洞。事实上，即使密码学被假定为完全可靠的构建块，1部分由欧盟合同IST-2001-32617“移动分布式系统安全性的模型和类型”（MyThS）支持的工作2 电子邮件地址：maffei@dsi.unive.it1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2004.11.04256M. Maffei/Electronic Notes in Theoretical Computer Science 128（2005）55入侵者可以进行许多潜在的危险动作，特别是截取/重放/伪造消息，以破坏预期的协议变体。形式化方法作为协议设计和验证的工具已经被证明是非常成功的。一方面，几种模型检查技术已经被应用于分析安全协议（参见，例如，[17，19]），导致发现了几次攻击。然而，他们的精度是平衡的必要性，以explore所有可能的消息序列，在协议的执行过程中产生的因此，分析无限数量的参与者，可能运行不同的和未知的协议，证明是不可行的。另一方面，静态分析技术，例如，类型系统[1，9，10]和控制流[2，3]，旨在通过只检查源代码来证明程序（在我们的情况下是协议）的属性。它们很吸引人，因为（i）只检查代码，不需要生成和探索所有可能的执行序列;（ii）通过利用组合性，可以（甚至自动）证明具有无限数量会话和参与者的协议的正确性组合性对于研究多协议系统也很有吸引力，因为它可以在不分析整个系统的情况下给出正确性的局部保证。这些优点是通过近似感兴趣的属性而获得的，因此失去了精度：静态分析通常是合理的（不正确的协议从未被验证），但不完整，因为可能存在假阴性，即，无法验证的正确协议。通常，上面提到的方法研究在不受信任的环境中运行相同协议的主体之间的交互。不同协议之间的交互（可能执行一些共同的子任务）被认为是一个开放的问题[16]，并且在全球计算环境中特别有趣，其中多个安全服务共存并可能组合在一起。事实上，这种互动可能是棘手的。作为一个例子，让我们考虑以下两个简单协议：α。1）B→A：nα。2）A→B：{B，M，n}kABβ。1）A→B：A，Mβ。2）B→A：{B，n，M}kABβ。3）A→B：n第一个协议是众所周知的ISO两次通过认证协议：B发送一个随机数，即随机挑战，由A加密，以及B的身份标签和她愿意认证的消息。加密密钥kAB是在A和B之间共享的密钥。当M. Maffei/Electronic Notes in Theoretical Computer Science 128（2005）5557B接收到该消息，并通过验证随机数的相等性来检查其新鲜度，他保证M是来自A的真实性。在协议β中，A以明文形式发送消息M（例如广播消息）和她的身份标签。在第二条消息中，B要求A通过发送密文来认证该消息，该密文用与A共享的长期密钥加密，包含身份标签B、新的随机数n和消息M。A可以通过发布n来确认。这两个协议在使用不同密钥时是安全的然而，当同一密钥被利用来执行两个协议时，它们α。1）B→I（A）：nβ。1）I（A）→B：A，nβ。2）B→I（A）：{B，nA，n}kABα。2）I（A）→B：{B，nA，n}kABB启动协议α，发送一个新的随机数用于认证A，敌人截获并将其与身份标签A一起接收到运行协议β的B的另一个实例。 B将随机数误认为是协议β的广播消息，并要求A验证该消息。敌人将第三条消息发送给B，B将该消息误认为是第二个协议的密文，因此认证A。不幸的是，A不存在于身份验证任务中！该攻击利用了两个密文之间的结构相等性。在[4，5]中，我们提出了一种基于ρ- spi演算的身份验证静态分析。分析是组合的：每个主体都是单独的类型检查.主要定理保证了正确主体的并行合成是安全的。我们的安全概念形式化了Lowe [14]提出的协议属性：“无论何时Bob完成发起者角色，显然是与Alice一起完成的，那么Alice之前已经在同一个认证任务中运行了响应者角色，与Bob一起完成。此外，Alice和Bob同意要认证的消息m组合性是通过利用标记机制来实现的。这种方法用于表达每个密文所执行的认证保证，而不管产生它的特定认证协议。在本文中，我们讨论了标记机制如何应用于多协议系统。58M. Maffei/Electronic Notes in Theoretical Computer Science 128（2005）552用于身份验证的表1标记方案POSHB→A：nA→B：{Id（I），Auth（M），R（n）}kB→A：{Id（I），Auth？（M），R public？（n）}kSophA→B：n索斯B→A：{Id（I），Auth？（M B），Rsecret？（n）}kAA→B：{R secret（n），Auth（M A）}kB身份验证协议中使用的消息通常是不明确的。例如，让我们考虑下面的简单密文：{A，n，m}kAB。第一个歧义是关于每个消息组件的角色：n可能是一个随机数，m是一个要验证的消息，但反过来也可能是正确的。即使在执行单个协议时，这种模糊性也经常导致攻击，称为类型攻击。此外，第二个更棘手的模糊性是可能的：密文可能从A发送到B，以验证M（如在协议α中）或询问B是否同意M（例如，M可能是A创建的新会话密钥）;但是，它也可能从B发送到A，目的相同。当执行单个协议的多个会话时，这种模糊性通常会导致攻击，I RKA索赔键（A，B）BVerifkey（A，B）B Verifkeypriv（A）I RKA索赔键（A，B）BVerifkey（A，B）B Verifkeypub（A）I R索赔B验证B验证kI（I=A，B）键（A，B）key（A，B）keypubM. Maffei/Electronic Notes in Theoretical Computer Science 128（2005）5559一B当然，在多协议系统中，情况甚至更糟：如Syverson和Meadows在[15]中所讨论的，我们提出了一种标记机制，统一适用于不同的认证协议，防止这两种形式的歧义。密文可能包含一个身份标签，它可以指定认证任务的请求者或验证者。随机数通常用于保证密文的新鲜度。密文还可以包含要认证的消息。协议通常分为三类，根据nonce握手[10，12]：在公开出秘密归属（POSH）中，nonce作为明文发送并接收到密文，在秘密出公开归属（SOPH）中相反，而在秘密出秘密归属（SOSH）中，nonce被发送并接收回（不同的）密文。 §1中的协议α使用POSH随机数握手，而协议β基于 SOPH。作为SOSH随机数握手的示例，让我们考虑以下协议：γ。1）B→A：{n，B，MB}k+γ。2）A→B：{n，MA}k+第一个消息用A的公钥加密。通过该密文，B询问A她是否同意MB，并且她是否愿意向B认证自己，B是认证会话的验证者。随机数握手的这一部分与SOPH随机数握手完全相同然而，第二个消息是不同的，因为随机数是保密的（它是用B的公钥加密的，敌人无法读取）。通过发送回该随机数，A确认从B接收到的请求，如在SOPH随机数握手中，但也认证由A发起并与秘密随机数一起加密发送的MA。在这个意义上，第二个消息结合了POSH和SOPH一次性握手的属性。表1总结了三种一次性握手，以及如何根据一次性握手对它们进行分类。POSH密文可以用A和B之间共享的密钥加密，也可以用A的私钥加密。在前一种情况下，必须出现一个身份标签，以消除密文3的始发者和预期接收者的歧义。如果身份标签是A，则随机数由Claim标记，因为A是认证会话的声明者。 如果它是B，则随机数由Verif标记，因为B是验证者。在后一种情况下，3身份标签和随机数是必要的，以防止反射和重放攻击，分别（详细信息见[6，8]）。60M. Maffei/Electronic Notes in Theoretical Computer Science 128（2005）55需要身份标签来指定认证会话的预期验证者。因此，nonce由Verif标记。SOPH密文可以用A和B之间共享的密钥加密，也可以用A4的公钥加密。消息组件的标记类似于前一种情况;标记是疑问的，因为B询问A她是否同意M并愿意接受B作为认证任务的验证者。下标public指定在确认的情况下，nonce应该以明文形式发送。SOSH这个一次性握手结合了前两个握手。随机数是保密的，所以只有A可以发送回那个随机数：这激发了下标秘密。当加密第二密文内的随机数时，A还可以认证由Auth标记的新消息。这些模式可以组合在一起，因为密文可能包含例如在不同种类的随机数握手中使用的两个随机数此外，如[4]中所示，对于POSH一次性握手，当协议中涉及可信第三方（TTP）以及会话密钥用于实现认证时，这种标记方案会扩展。3标签和多协议系统这里提出的标记机制解决了§2中讨论的两种歧义：随机数、消息和身份标签被明确地确定。此外，标签显示谁是密文的发起者和预期的接收者，以及它在认证任务中是代表挑战还是回答。此外，标记明确地指示由密文传达的认证保证。事实上，它们不依赖于产生它们的协议：假设所有参与者都同意这种标记机制，标记允许本地推理。例如，如果A接收到一个密文，该密文是对先前发送给B的质询的回答，则A可以独立于正在运行的特定协议B来认证B。该协议的唯一假设是它尊重我们的标记机制。这种形式的组合性，在[4，5]中形式化，允许我们在多协议系统上进行推理，其中主体对周围的世界一无所知。作为一个例子，让我们回到§1中的两个协议：我们认为，[4] A的私钥不能使用，因为随机数应该只在A确认的情况下才被发送回来：用A的私钥加密的密文将被敌人读取，敌人可能会发送回随机数。M. Maffei/Electronic Notes in Theoretical Computer Science 128（2005）5561协议α中的密文可以标记为{Id（B），Auth（M），Verif（n）}kAB，因为A指定B作为认证任务的验证者。在协议β中，密文可以被标记为{Id（B），Verifpublic？（n），Auth？（M）}kAB，因为B询问A她是否愿意向B（即认证任务的验证者）认证M。请注意，在协议的标记版本上不可能进行类型重写攻击，因为消息M和随机数n是不同标记的，并且随机数的标记表明，在协议α中，密文表示响应，而在协议β中它表示挑战。一个有趣的观点是，可能有不同的方式来标记协议。例如，让我们考虑§1中协议β的一个简单变体。βJ。1）B→A：nβJ。2）A→B：{A，B，M，n}k密文可以标记为{Id（A），B，Auth（M），Claim（n）}kAB或{A，Id（B），Auth（M），Verif（n）}kAB。注意，标记对于在执行协议βJ的多协议系统中保持安全性与另一种变体同时：βJJ。1）B→A：nβJJ。2）A→B：{B，A，M，n}k事实上，这两个协议的未标记版本受到以下攻击的影响：βJJ。1）B→I（A）：nβJ。1）I（A）→B：nβJ。2）B→I（A）：{B，A，M，n}kβJJ。2）I（A）→B：{B，A，M，n}k4结论和相关工作多协议系统是安全协议分析研究中的一个新兴问题[16]。不可信环境不仅包含Dolev-Yao入侵者，还包含运行不同协议的可信主体。不同协议会话之间的交互可能很棘手，并且难以分析。在[11]中，Guttman和Thayer在Strand Spaces形式主义[12]中证明，如果不同协议处理的加密消息集是不相交的，那么这些协议的并发执行是安全的。换句ABABABAB62M. Maffei/Electronic Notes in Theoretical Computer Science 128（2005）55换句话说，保证安全性的充分条件如下：如果协议使用消息，则没有其它协议应该构造该形式的消息。直觉地，在全球计算环境中，为了安全地实现安全服务，有必要避免不同协议之间的事实上，这个条件可以简单地实现：协议设计者可以同意允许一个独立的机构为他们选择协议特定的标识符。或者，设计者可以随机选择它们，遵循某种通用算法，保证碰撞的概率可以忽略不计。我们从相反的角度来处理这个问题：我们不阻止不同协议之间的交互。相反，我们证明了[4，5]，同意我们的标记方案的不同协议之间的通信结果是安全的。带标记的消息显式地指示它们提供的身份验证保证，因此允许主体接受身份验证，而不管另一方正在运行的协议。此外，标记消息的生成也由本地推理来控制（详情参见[4，5]）。这可以被认为是迈向理想的协议独立通信概念的第一步，其中安全目标通过简单地坚持共享标记方案来实现。致谢感谢匿名推荐人提供了非常有用的意见和建议，并感谢RiccardoFocardi提供了宝贵的反馈。引用[1] M. Abadi和B.布兰切特非对称通信的保密类型。 Theor. Comput. Sci. ，298（3）：387[2] C. Bodei，M. Buchholtz，P. Degano，F. Nielson和H.里斯·尼尔森自动验证协议叙述。在第16届IEEE计算机安全基础研讨会（CSFW'03）的会议记录中IEEE Computer Society Press，June2003.[3] C. Bodei，M. Buchholtz，P. Degano，F. Nielson和H.里斯·尼尔森控制流分析也可以发现新的规律在安全理论问题研讨会（WITS'04）的会议记录中Elsevier，2004年。[4] M.布列西河Focardi和M.妈妈，认证协议的组合分析。在Proceedings of European Symposiumon Programming（ESOP 2004），卷2986的Lecture Notes in Computer Science，第140-154页Springer-Verlag，2004.[5] M. Bugliesi，R.Focardi，and M.Ma Jingei.认证的类型和效果理论。在ACM Proceedings ofFormal Methods for Security Engineering：From Theory to Practice（FMSE2004）中，第1-12页。ACM Press，October 2004.[6] 克 拉 克 和 雅 各 布 。 A survey of authentication protocol literature ： Version 1.0.http://www.cs.york.ac.uk/，1997年11月。M. Maffei/Electronic Notes in Theoretical Computer Science 128（2005）5563[7] R.福卡尔迪河Gorrieri和F.马蒂内利用于密码协议分析的无干扰。在ICALP'00的会议记录Springer LNCS 1853，2000年7月[8] R. Focardi 和 M. 妈妈， 工作中的ρ-spi 演算： 身份验证案例研 究。 在 Mefisto Project 的Proceedings中，第99卷，Electronic Notes in Theoretical Computer Science，第268- 269页293. Elsevier，2004年8月。[9] A. Gordon和A.我是杰弗里。通过键入安全协议进行验证。在第14届IEEE计算机安全基础研讨会（CSFW'01）的会议记录IEEE Computer Society Press，June 2001.[10] A. Gordon和A.我是杰弗里。 非对称密码协议的类型和效应。 在第15届IEEE计算机安全基础研讨会论文集（CSFW91. IEEE计算机协会出版社，2002年6月24-26日[11] 约书亚·D Guttman和F.哈维尔·塞尔通过不相交加密实现协议独立性。 在第13届IEEE计算机安全基础研讨会（CSFW'00）的会议记录IEEE计算机协会出版社，2000年7月。[12] 约书亚·D Guttman和F.哈维尔·塞尔 验证测试和捆绑包的结构。Theoretical Computer Science，283（2）：333[13] J. Heather，G. Lowe和S.施耐德 如何防止对安全协议的攻击。 在第13届IEEE计算机安全基础研讨会（CSFW'00）的会议记录IEEE计算机协会出版社，2000年7月。[14] G. 洛 “A Hierarchy of Authentication Specification”. 在 第 10 届 计 算 机 安 全 基 金 会 研 讨 会（CSFW'97）的会议记录中IEEE Computer Society Press，1997.[15] C. Meadows和P. Syverson。使用npatrl和nrl协议分析器对解释协议的组域进行形式化规范和分析，2003年。发表在Journal of Computer Security上。[16] 凯瑟琳 梅多斯开放 问题 在正式 方法 密码协议 分析.计算机科学讲义，2052：21[17] J. C. 米切尔，M。米切尔和U。胸骨切开术组 使用mur φ进行密码协议的自动分析。 在1997年IEEE安全和隐私研究研讨会论文集，第141-153页。IEEE Computer Society Press，1997.[18] R M Needham和M D Schroeder。重新访问身份验证。ACM SIGOPS Operating SystemsReview，21（1）：7[19] L. C.保尔森秘密之间的关系 ：对yahalom协议的两种形式化分析 。Journal of ComputerSecurity，9（3）：197
我的内容管理
展开
