--→理论计算机科学电子笔记36（2000）网址：http://www.elsevier.nl/locate/entcs/volume36.html6页项重写在密码协议分析中的应用（特邀演讲概述）J. Millen计算机科学实验室Menlo Park，CA94025 USA电子邮件：millen@csl.sri.com摘要用于密钥分配和认证的密码协议在互联网安全中起着重要的作用。这些协议中的某些漏洞可以使用术语重写模型来表达协议、恶意网络环境和漏洞搜索策略来发现。1密码协议安全密码协议是简短的消息交换，其目的是向通信方分发密钥。这些密钥可用于传输机密信息或验证消息。例如，考虑以下协议：A -> B：{A，Na}pk（B）B -> A：{Na，Nb}pk（A）A-> B：{Nb}pk（B）形式A的每一行B：M，意味着A将消息M发送给B，结果每个都改变了状态。表达式A，Na pk（B）表示用B的公钥对级联字段A和Na进行加密。 Na和Nb是特定于会话的值，称为“随机数”，该协议被保密，并且可以在以后用作会话密钥。这种类型的规范被称为但是，请注意，实际的协议用户（如Alice）可以启动任何1由DARPA通过SPAWAR合同N66001-00-C-8014提供部分支持。2000年由ElsevierScienceB出版。 诉 操作访问和C CB Y-NC-ND许可证。MILLEN2许多进程，其中一些可以扮演A角色，而另一些则扮演B的角色。这个协议是1978年发表的一个更长的协议的一部分;它在1996年被发现是不安全的[8]。第三方（“Mallory”）可以该漏洞可以从上面的抽象表示中发现，仅给出理想化的加密概念和简单的攻击者模型，并且所有这些都可以使用术语重写规则来表示。密码协议最常陈述和分析的安全属性是保密性和认证性。会话密钥和用户数据应该保密，会话密钥或重要数据（例如合同）的接收者应该能够确认发送者的身份。这些是安全属性，即，状态不变量一些协议具有更复杂的安全目标，但在如何声明它们方面没有达成共识。活性属性通常被认为是性能而不是安全属性。2协议建模Dolev和Yao [7]提出的一类密码协议的最早数学模型是重写规则模型。那篇论文研究了例如，状态转换规则可以将接收到的消息x重写为EB（DA（x）），其中EA表示用A有像Dx（Ex（y））→y这样的归约规则。诚实方必须遵守协议，而恶意方Z可以拦截任何消息，对任何x应用Ex和恶意方的解密运算符D Z的任何组合，并将结果转发给任何会话中的攻击的目的是暴露在第一条消息中加密发送的秘密安全问题是决定这个非常有限的模型，也为它的小扩展。术语“Dolev-Yao”模型现在通常用于指攻击者可以拦截和重定向消息的任何协议模型，并使用公理定义的操作和攻击者可用的数据修改其内容。为了使密码协议问题不可判定，我们只需要假设，首先，两个项可以连接成一个更长的消息，其次，存在某种类型的无界项集，通常称为“nonce”。随机数作为唯一的标识符来区分不同的会话[3]。已经有一些方法来识别受限的协议类别，对于这些协议，检查有限数量的会话是足够的。例如，有LoweMILLEN3--这一点，足以说明，有可能是一个“伪君子”。但这一结果的条件是非常严格的。状态探索方法通常执行有界的迭代扩展搜索。Mitchell最近的多集重写规则（MSR）模型[3]受到线性逻辑的启发，既简单又通用，足以扩展到实际协议。在MSR模型中，系统状态是“事实”的有限集合0的a和b之间的协议）;传输到网络的消息，例如作为N（a，b）;以及攻击者记忆的消息组件，例如M（a）.例如，协议规则显示如何更新状态和生成消息A0（A，B）→（K）A1（A，B，K）， N（{A}K），其中量化器具有特殊的含义，即关键变量K是使用nonce实例化。系统状态多集中与左侧匹配的状态事实被移除，并由类似实例化的右侧替换。(The系统状态是多重集，因为某些规则，如会话初始化或消息创建规则，允许生成某些项的任何数量的副本。该模型还包括攻击者规则，例如，攻击者可以通过这些规则解密加密项并将结果添加到其内存中，例如M（{A}K），M（K）→ M（{A}K），M（K），M（A）。请注意，攻击者模型是固定的和通用的，给定协议使用的加密和其他计算函数还有其他的模型，如专门的认知认证逻辑[2][15，1]，但他们有一个长期重写的代数表示。3协议分析存在用于证明密码协议满足安全性的技术。Paulson的一篇重要论文展示了一种归纳技术来证明保密或认证不变量[14]，还有其他人，使用与MSR模型精神相似的模型。使用认证逻辑的证明对于理解协议是有用的，但是它们通过以一种非算法的方式将协议“理想化”为逻辑语句来工作，当协议实际上是安全的时，证明协议安全性是最有用的如果协议存在漏洞（大多数协议都存在漏洞，至少在其初始版本中是这样），则实现某种形式的状态搜索是有效的MILLEN4→3.1Using Prolog最古老的密码协议分析方法使用Prolog。很容易将协议方的状态表示为Prolog术语，消息也是术语，因此环境的全局状态就是这样的状态和消息的列表。全局状态转换更新某方Interrogator是一个用于协议分析的Prolog程序[12]，它是一组Prolog规则，表达了一个关系可达（H，Q），这意味着全局状态Q可以通过消息序列H到达。在一个典型的可达性查询中，Q被部分实例化为不安全状态，H是一个变量，将被成功的Prolog搜索实例化以进行攻击。Prolog的内置解析算法执行从不安全目标状态到初始状态的反向搜索。 这种方法的挑战是终止，而不是这只是因为固有的不可判定性，而是因为需要控制Prolog的深度优先搜索。部分答案是使程序具有交互性，以利用用户指导。Meadows的NRL Protocol Ana- lyzer [11]（也是一个Prolog程序）引入的改进之一窄- ing解决方程模重写规则的规范集;并且用于减少符号加密的规则，例如dec（K，enc（K，X））=X，是规范的。使用窄化的一种方法，也在后来的Interroga- tor版本中采用，是查找前驱状态。假设协议包括转换规则Q，M QJ，意味着当接收到消息M时，可以存在从Q到Q j的网络状态转换;并且攻击者的目标是部分实例化的状态Qa。现在假设窄化成功地解决了QJ= Q a与替代σ。然后攻击者的工作被减少到到达状态σQ并生成消息σM。窄化的使用揭示了另一个挑战，当协议使用非规范操作时，例如交换和关联操作。例如，逐位模2加法（异或）在许多协议中用作加密运算符。3.2模型检查工具已有的模型检验工具，如用于处理器“硬件”设计的模型检验工具，在密码协议分析中的应用已取得了许多成功。刺激是Roscoe关于FDR使用的论文[15]，其次是Lowe关于Needham-Schroeder协议的结果[8]。其他研究人员意识到，类似的技术可以与他们自己的工具一起使用[10，13]。现代计算能力、模型检查的进步（如BDD）和一些特定于协议的优化相结合，使得在合理的执行时间内发现以前未发现的漏洞成为可能，在初始编码和设置之后没有用户交互。MILLEN5关于建模和搜索优化的经验教训可以以其他方式应用。一个显着的结果是Maude的能力，重写逻辑系统，而不是一个模型检查器，成为一个模型检查器。使用元级执行策略，它执行迭代广度优先状态搜索，并利用适合于协议问题的状态约简优化。通过这种方式，它实现了与模型检查工具相当的性能[5，4]。也可以为协议问题定制一个新的模型检查器。Athena [16]采用了一种不寻常的方法，使用链空间模型[17]。在这个模型中，网络的状态是一个被称为束的单一结构，由部分按因果关系排序的节点组成。串是由来自同一进程的执行序列排序的相邻节点组成的字符串。协议用参数化链指定可能的合法链，即，带有可变参数的串表达式，这些表达式可以通过连接发送和接收的消息连接成半束Athena试图将一个包含安全违规的小半丛扩展为一个完整的丛。它是有效的，因为它使用了偏序，因为状态扩展引入了整个链一次。一个半丛可以看作是一个大的复数项。如果一个通用的术语重写系统能够适应这种方法，那将是很有趣的。4结论将项重写的概念和工具应用于密码协议的安全性分析有着自然和实用的方法。除了上面提到的特定方式外，术语重写也可以以其他方式应用于该领域，例如实现从高级协议语言到规则表示的翻译器的一部分，就像在CAPSL翻译器中使用Maude所做的那样[6]。我们也可以期待从相关领域的进步中获益，比如缩小算法，也许还可以从图重写等扩展中获益引用[1] M. Abadi和A.戈登密码协议的演算：Spi演算。技术报告SRC-149，数字系统研究中心，1998年。[2] M. Burrows ， M. Abadi 和 R. 李 约 瑟 认 证 的 逻 辑 。 ACM Transactions onComputer Systems，8（1）：18[3] I. Cervesato，N. Durgin，P. Lincoln，J.Mitchell，and A.谢德罗夫协议分析的Meta符号.第12届IEEE计算机安全基础研讨会，第55IEEE计算机学会，1999年。MILLEN6[4] G.丹可CIL连接器到Maude的设计。In H. V.和N. Heintze和E.Clarke，编辑，正式方法和计算机安全研讨会。卡内基梅隆大学，2000年7月。[5] G. Denker，J.Meseguer，and C.塔尔科特Maude中的协议规范和分析。形式方法和安全协议，1998年。LICS[6] G. Denker 和 J.Millen 。 CAPSL 集 成 协 议 环 境 。 DARPA InformationSurvivability Conference（DISCEX 2000），第207-221页。IEEE计算机学会，2000年。[7] D. Dolev 和 A. 耀 公 钥 协 议 的 安 全 性 。 IEEE Transactions on InformationTheory，IT-29：198-208，1983。另见STAN-CS- 81-854，1981年5月，斯坦福大学。[8] G.洛使用FDR破坏和修复Needham-Schroeder公钥协议。在TACAS会议录中，计算机科学讲义第1055卷，第147-166页。Springer-Verlag，1996.[9] G. 洛 安 全 协 议 模 型 检 验 的 完 备 性 结 果 。 Journal of Computer Security ， 7（2/3）：89[10] W. Marrero，E. Clarke和S. Jha.安全协议的模型检查。在DIMACS安全协议的设计和验证研讨会上。罗格斯大学，一九九七年。[11] C. 梅多斯一种用于规范和验证密钥管理协议的系统IEEESymposium onSecurity and Privacy，第182-195页。IEEE计算机学会，1991年。[12] J. Millen，S. Clark和S.弗里德曼The Interrogator：协议安全分析。IEEE软件工程学报，SE-13（2）：274[13] J. Mitchell，M.米切尔和U。胸骨切开术组使用Murφ进行密码协议的自动分析。IEEESymposium on Security and Privacy，第141-154页。IEEE计算机学会，1997年。[14] L. 保尔森验证密码协议的归纳方法Journal of Computer Security，6（1）：85[15] A. W.罗斯科使用CSP和FDR建模和验证密钥交换协议。第八届IEEE计算机安全基础研讨会，第98-107页。IEEE计算机学会，1995年。[16] D.歌Athena：一种新的高效安全协议自动检验器。在第12届IEEE计算机安全基础研讨会上，第192202. IEEE计算机学会，1999年。[17] J. Thayer，J. Herzog和J. 古特曼串空间上的诚实理想 第11届IEEE计算机安全基础研讨会，第66-78页。IEEE计算机学会，1998年。
