形式化方法在密码协议中的应用

1、形式化方法在密码协议中的应用论文导读：与符号化方法相比拟，我们使用形式化方法对协议进行描述不仅是为了简化描述过程，而是为了进一步利用形式化方法对协议进行验证：证明协议是正确的，即实现了为其制定的各种平安性目标。于是，证明一个协议的平安性问题就转化为证明上述项重写系统中不会产生这样的特定句子。另一种用于分析密码协议的形式化方法是建立在逻辑方法的根底之上。关键词：形式化，密码协议，平安性长期以来，密码学专家一直凭着丰富的经验来指导和设计密码协议，但事实说明这种设计方法很容易忽略掉一些微妙的、直觉难以发现的漏洞。因此，将形式化方法应用到密码协议中是必然的结果。1、形式化方法形式化方法是一种用于描述系

2、统性质的数学方法，它主要用于发现一个系统中的歧义性、不一致性，与不完备性那么这个系统可以大到某个企业级的软件、硬件系统，也可以小到我们讨论范围内的某个协议。与符号化方法相比拟，我们使用形式化方法对协议进行描述不仅是为了简化描述过程，而是为了进一步利用形式化方法对协议进行验证：证明协议是正确的，即实现了为其制定的各种平安性目标；或者分析出协议存在的缺陷。因此，形式化方法在给出描述协议的符号集合根底上，还会在该集合上定义各种关系与运算，以进一步揭示隐藏在协议内部的各种性质。那么如何运用形式化方法证明协议的正确性呢？证明过程通常可以分为三个局部：第一、确定证明的目标，即协议需要实现何种平安目标；第二

3、、建立协议的形式化模型，即给出协议的形式化描述；第三、证明。虽然形式化方法为协议的验证工作提供了强大的证明手段，但是形式化方法并不能为协议的正确性提供百分之百的保证。这是因为：首先，协议正确性的证明总是在证明它的形式化方法所采用的特定假设下进行的，如果违背了这些假设，那么原先的证明结果也就失去了意义。2、密码协议的形式化分析方法目前形式化方法主要用于研究协议的性质，这在很大程度上独立于协议所包含的密码算法的性质，因此下文中我们总是假设协议所使用的密码算法是不可破解的。(1) 基于代数分析的方法在1983年，Dolve与Yao首次提出将协议作为代数系统来研究。它们为密码协议建模的代数系统被称作D

4、olve-Yao模型，对这一模型稍加修改，就是目前大多数形式化方法仍在使用的模型【4】。在Dolve-Yao模型中，协议的交互过程采用代数方法表示：消息的接收与发送分别对应一组代数表达式以及相应的变换规那么;网络被认为是处于入侵者的控制之下：入侵者可以读取所有的信息流，并具有创立、修改与破坏消息的能力；此外，即入侵者还可以执行任何系统合法用户能够执行的操作。但同时假设：在初始阶段，入侵者不知道任何关于系统合法用户的秘密信息。这样，入侵者就可以将协议交互过程看作产生句子(消息)的机器，并且这些句子满足特定的重写(rewrite)规那么，例如：句子中具有相同密钥的加密与解密操作符可以互相抵消。因此

5、，入侵者的目标就是找到一个揭示秘密的特定句子。于是，证明一个协议的平安性问题就转化为证明上述项重写系统中不会产生这样的特定句子。但是Dolve-Yao模型只针对某种特定形式的协议，即，级联协议与名称戳协议。并且后来Even与Goldreich发现，如果对上述协议稍微放宽条件，那么协议的平安性问题就成为数学上不可判定的问题。因此，这方面的理论工作没有进一步拓展。然而稍后，用于分析协议平安性的工具开发得到了人们的重视，并且这些工作大都基于Dolve-Yao模型。这其中包括软件工具Interrogator， N RL协议分析器fill与Longley-Rigby工具。在这些工作的早期阶段，研究人员所

6、开发的工具成功地发现了一些人I分析难以发现的协议漏洞。例如，研究人员利用NRL协议分析器发现了Simmons选择性播送协议中的一个漏洞；利用Longley-Rigby工具发现了一个银行协议中的漏洞。而近年来研究人员主要致力于在Dolve-Yao模型之上实现模型检测技术与定理证明技术。这方面的工作开端于Lowe利用一个具有普遍意义的模型检测器，即FDR，发现了针对Needham-Schroeder公钥协议的中间人攻击。自此，利用模型检测器与定理证明器来分析协议平安性问题的工作得到了人们的普遍重视。(2)基于逻辑推理的方法另一种用于分析密码协议的形式化方法是建立在逻辑方法的根底之上。这种方法中最具

7、影响力的一类就是BAN逻辑，它由Burrows, Abadi和Needham于1989年提出。与上述Dolve-Yao模型不同的是，虽然BAN逻辑考虑到入侵者存在的可能性，但是它不检查未授权情况下的秘密泄漏，而主要研究可信主体(principal)在协议执行过程中所持信念(belief)的演化。BAN逻辑的设计者希望给出每个消息的精确含义，因此它们将一个消息转换为一个逻辑表达式，这个逻辑表达式是原有消息的一个理想化模式。此外，BAN逻辑还给出一套逻辑推理规那么。在利用BAN逻辑对协议进行分析之前，首先需要对协议进行理想化处理，然后还需要给出协议主体具有的初始信念假设。在协议执行过程中，协议主体

8、通过接收消息能够增加较为直观的知识，然后根据上述初始假设的信念与协议执行过程中得到的知识，利用BAN逻辑给出的推理规那么就可以得到此协议步骤下直观上难以得到的深层次的知识与信念。如果在协议执行结束后，通过上述推理所得到的信念能够满足鉴别协议的平安需求，例如共享会话密钥，那么就证明该协议是正确的。如果不能满足，那么说明这个协议可能存在漏洞。利用BAN逻辑，其设计者曾经成功地发现了存在于CCITT X.509标准推荐草案中的一个以前未被发现的漏洞。但是BAN逻辑也存在一些问题，例如：语义模糊、理想化过程局限、初始假设不尽合理、以及推理规那么不够完善，使得利用BAN逻辑己证明为平安的协议，后来却被发

9、现存在漏洞。这样一来，人们只能相信BAN逻辑证明协议的不平安性，而不能相信其证明的协议平安性。为此，研究人员对BAN逻辑进行了改良，这些改良后的逻辑统称作BAN类逻辑。其中，由Gong, Needham和Yahalom提出的GNY逻辑试图消除BAN逻辑中的假设千不合理的初始假设；由Abadi和Tuttle提出的AT逻辑从语义的角度进一步对BAN逻辑进行了修正；Syverson和VanOorschot提出的SVO逻辑吸收TBAN. GNY与AT逻辑的优点，是目前为止最为完善的BAN类逻辑【5】。除了上面介绍的BAN类逻辑，还出现了NCP逻辑、Kailar逻辑以及CS逻辑等等。(3)借助图论的St

10、rand Space方法1998年，Thayer，Herzog和Gutman提出了一种分析密码协议平安性的新方法【6】，即Strand Space。它利用图论方法来建立协议中因果关系的模型，但本质上仍是基于代数的分析方法。它主要用于证明一个协议的正确性。Strand用于描述在协议执行过程中协议主体的一个行为序列，它是一个线性结构。而Strand Space就是关于Strand的集合。各Strand通过消息的发送与接收相钩连，钩连的整体称作Bundle，它是一个用于描述Strand间通信的图结构。该方法根据主体所具有数据组成的模板来判断协议是否正确。并且该方法提出的理想的概念有助于状态可达性的归

11、纳证明。需要指出的是，这个方法目前还没有被自动化，只能通过手工对协议进行分析。Strand Space方法的重要性在于：其一，它能够将以往分散在文献中的许多技术结合在一起构成一个简洁的数学模型；其二，它独立于任何特别的标准语言与工具；其三，它洞察到是Strand，而不是状态，是描述密码协议标准的更为实用的根本单位。因此，研究人员经常将这种方法作为密码协议形式化分析的新的理论根底，并且利用它对以前的提出的方法进行语义分析，例如Syverson为SVO逻辑引入Strand语义。3、密码协议平安需求的形式化分析将形式化方法应用于协议分析的早期工作集中在密码协议的秘密性验证上，例如，Dolve-Yao

12、模型。但是研究人员很快认识到，仅做到这一点是不够的，因为密码协议还提供其它效劳，例如：认证。因此，一个巫待解决的问题就是确定什么是一个平安协议的目标?从概念上讲，利用形式化方法分析密码协议的目标就是检查其平安性质在协议执行过程中是否遭到破坏。从功能上讲，就是要实现如下两点：其一，找到协议漏洞；其二，证明协议正确性。然而仅得出上述两种解释还是远远不够的，研究人员只能将它们作为寻求这个问题答案的依据或者方向，进而从不同角度对这个问题进行更加深入细致的研究。在这个问题上Diffe、VanOorschot和Wiener首先提出了针对认证协议的正确性的非形式化需求描述。它们认为:会话密钥必须是秘密的；协

13、议的运行轮数必须是匹配的。其中后者是指，如果A和B参加了同一轮协议，那么A接收到的反之亦然。其后，Woo和Lam给出了一个类似的方法定义密钥分发协议的平安性。它们首先定义了一个描述协议执行的语义模型，其中包括两个根本概念，即，一致性(correspondence)与秘密性。秘密性是不言自明的：一致性那么是要求特定事件的发生必须在另一些事件发生之后。由此可以看出，一致性的概念与匹配的协议轮数的概念具有一定的相似之处。但是它具有更广泛的含义，因为两个事件不一定必须是发送与接收同样的消息。另一种说明协议平安需求的方法表达在NRL协议分析器的标准语言中，它与Woo和Lam给出的一致性概念相似之处在于其

14、需求的说明是基于事件的序列。不同之处在于，它不是适用于所有协议的一般意义下的一致性概念。在此根底上Syverson和Meadows给出了一系列针对认证协议中各种消息的平安需求标准并给出具有再次认证性质的密钥分发协议的平安需求标准。此后，Yahalom提出了一个与上述方法类似但具有不同目标的方法。它利用Syverson和Meadows给出的平安需求标准来确定为保证协议满足这些标准所必须发送的消息的最小数目。然后构建了一个使用具有最小数目的消息的协议。它的目标是利用协议平安需求的公式来获取在这些需求规定的范围内的最好的性能。此外，在讨论上述问题的时候，研究人员无意中还揭示了密码协议平安需研究的一个

15、更深层次的意义。即，密码协议平安需求的问题非常近似于一个分布式系统的平安模型的问题。因为，当我们开始讨论密码协议的需求时，讨论的内容就是系统的哪一局部向系统的其它局部提供什么样的平安效劳，以及哪一局部以什么样的方式相信另一局部等等。这些问题就是在一般意义下我们考虑一个分布式系统平安需求时所必须提出的问题。因此，未来密码协议的分析领域与分布式系统的平安建模领域有望会越来越相互靠近。4、总结使用形式化方法分析密码协议的动机源于研究人员希望自己所设计的协议在投入使用之前就能够被证明是平安的。迄今为止，虽然还没有一种可信的方法能够证明一个密码协议是真正平安的。但是通过形式化的分析方法，研究人员己经发现

16、了许多协议中以前一直未被发现的平安漏洞，从而说明这些协议是不平安的。当然，研究人员也一直未放弃自己的初衷，为寻求一种能够最终证明一个密码协议是真正平安的方法而不断努力。参考文献：【1】 卿斯汉. 平安协议20年研究进展. 软件学报，2003，14(10):1740-1752.【2】 Bruce Schneier. 应用密码学：协议、算法和C源程序. 北京：机械工业出版社，2000.33-52.【3】 卢开澄. 计算机密码学. 第3版. 北京：清华大学出版社，2003.351-361.【4】 Clarke E M, Wing J M,Alur R,etal. Formal Methods:Sta

17、te of the Art and Future Directions. ACM ComputingSurveys.1996,28(4):626-643.【5】 Visser W, Havelund K,Brat G,etal. Model Checking Programs. Automated SoftwareEngineering,2003,10(2):203-232.【6】 Wolper P. The Meaning ofFormal:FromWeak to Strong Formal Methods. Springer International Joumal onSoftware Tools for Technology Transfer,1997,1(1-2):6-8.【7】 Poueli A. The Temporal Semanticsof Concurrent Programs.in:Proceedings of the international Sympoisum onSemantics of Concurrent Computation. London,UK:Springer-Verlag,1979:1-20. Pnucli S. In Transition FromGlobal to Modular Tempora