| 为此，研究人员对BAN逻辑进行了改进，这些改进后的逻辑统称作BAN类逻辑。其中，由Gong, Needham和Yahalom提出的GNY逻辑试图消除BAN逻辑中的若千不合理的初始假设；由Abadi和Tuttle提出的AT逻辑从语义的角度进一步对BAN逻辑进行了修正；Syverson和VanOorschot提出的SVO逻辑吸收TBAN. GNY与AT逻辑的优点，是目前为止最为完善的BAN类逻辑[5]。
除了上面介绍的BAN类逻辑，还出现了NCP逻辑、Kailar逻辑以及CS逻辑等等。
(3)借助图论的Strand Space方法
1998年，Thayer，Herzog和Gutman提出了一种分析密码协议安全性的新方法[6]，即Strand Space。它利用图论方法来建立协议中因果关系的模型，但本质上仍是基于代数的分析方法。它主要用于证明一个协议的正确性。Strand用于描述在协议执行过程中协议主体的一个行为序列，它是一个线性结构。而Strand Space就是关于Strand的集合。各Strand通过消息的发送与接收相钩连，钩连的整体称作Bundle，它是一个用于描述Strand间通信的图结构。该方法根据主体所具有数据组成的模板来判断协议是否正确。并且该方法提出的理想的概念有助于状态可达性的归纳证明。
需要指出的是，这个方法目前还没有被自动化，只能通过手工对协议进行分析。Strand Space方法的重要性在于：
其一，它能够将以往分散在文献中的许多技术结合在一起构成一个简洁的数学模型；
其二，它独立于任何特别的规范语言与工具；
其三，它洞察到是Strand，而不是状态，是描述密码协议规范的更为实用的基本单位。因此，研究人员经常将这种方法作为密码协议形式化分析的新的理论基础，并且利用它对以前的提出的方法进行语义分析，例如Syverson为SVO逻辑引入Strand语义。
3、密码协议安全需求的形式化分析
将形式化方法应用于协议分析的早期工作集中在密码协议的秘密性验证上，例如，Dolve-Yao模型。但是研究人员很快认识到，仅做到这一点是不够的，因为密码协议还提供其它服务，例如：认证。因此，一个巫待解决的问题就是确定什么是一个安全协议的目标?
从概念上讲，利用形式化方法分析密码协议的目标就是检查其安全性质在协议执行过程中是否遭到破坏。从功能上讲，就是要实现如下两点：其一，找到协议漏洞；其二，证明协议正确性。然而仅得出上述两种解释还是远远不够的，研究人员只能将它们作为寻求这个问题答案的依据或者方向，进而从不同角度对这个问题进行更加深入细致的研究。在这个问题上Diffe、VanOorschot和Wiener[7,8]首先提出了针对认证协议的正确性的非形式化需求描述。它们认为:会话密钥必须是秘密的；协议的运行轮数必须是匹配的。其中后者是指，如果A和B参加了同一轮协议，那么A接收到的来自于B的消息的记录必须与B发送消息的记录相匹配，反之亦然。
其后，Woo和Lam给出了一个类似的方法定义密钥分发协议的安全性。它们首先定义了一个描述协议执行的语义模型，其中包括两个基本概念，即，一致性(correspondence)与秘密性。秘密性是不言自明的：一致性则是要求特定事件的发生必须在另一些事件发生之后。由此可以看出，一致性的概念与匹配的协议轮数的概念具有一定的相似之处。但是它具有更广泛的含义，因为两个事件不一定必须是发送与接收同样的消息。
另一种说明协议安全需求的方法体现在NRL协议分析器的规范语言中，它与Woo和Lam给出的一致性概念相似之处在于其需求的说明是基于事件的序列。不同之处在于，它不是适用于所有协议的一般意义下的一致性概念。在此基础上Syverson和Meadows给出了一系列针对认证协议中各种消息的安全需求规范并给出具有再次认证性质的密钥分发协议的安全需求规范。
此后，Yahalom提出了一个与上述方法类似但具有不同目标的方法[9]。它利用Syverson和Meadows给出的安全需求规范来确定为保证协议满足这些规范所必须发送的消息的最小数目。然后构建了一个使用具有最小数目的消息的协议。它的目标是利用协议安全需求的公式来获取在这些需求规定的范围内的最好的性能。
此外，在讨论上述问题的时候，研究人员无意中还揭示了密码协议安全需研究的一个更深层次的意义。即，密码协议安全需求的问题非常近似于一个分布式系统的安全模型的问题。因为，当我们开始讨论密码协议的需求时，讨论的内容就是系统的哪一部分向系统的其它部分提供什么样的安全服务，以及哪一部分以什么样的方式相信另一部分等等。这些问题就是在一般意义下我们考虑一个分布式系统安全需求时所必须提出的问题。因此，未来密码协议的分析领域与分布式系统的安全建模领域有望会越来越相互靠近。
4、总结
使用形式化方法分析密码协议的动机源于研究人员希望自己所设计的协议在投入使用之前就能够被证明是安全的。迄今为止，虽然还没有一种可信的方法能够证明一个密码协议是真正安全的。但是通过形式化的分析方法，研究人员己经发现了许多协议中以前一直未被发现的安全漏洞，从而说明这些协议是不安全的。当然，研究人员也一直未放弃自己的初衷，为寻求一种能够最终证明一个密码协议是真正安全的方法而不断努力。
参考文献：
[1] 卿斯汉. 安全协议20年研究进展[J]. 软件学报，2003，14(10):1740-1752.
[2] Bruce Schneier. 应用密码学：协议、算法和C源程序[M]. 北京：机械工业出版社，2000.33-52.
[3] 卢开澄. 计算机密码学[M]. 第3版. 北京：清华大学出版社，2003.351-361.
[4] Clarke E M, Wing J M,Alur R,etal. Formal Methods:State of the Art and Future Directions[J]. ACM ComputingSurveys.1996,28(4):626-643.
[5] Visser W, Havelund K,Brat G,etal. Model Checking Programs[J]. Automated SoftwareEngineering,2003,10(2):203-232.
[6] Wolper P. The Meaning ofFormal:FromWeak to Strong Formal Methods[J]. Springer International Joumal onSoftware Tools for Technology Transfer,1997,1(1-2):6-8.
[7] Poueli A. The Temporal Semanticsof Concurrent Programs[A].in:Proceedings of the international Sympoisum onSemantics of Concurrent Computation[C]. London,UK:Springer-Verlag,1979:1-20.
[8] Pnucli S. In Transition FromGlobal to Modular Temporal Rcasoning about Programs[J]. Logics and Models ofConcurrent Systems,1985:123-144.
[9] Puncli A linear and BranchingStructures in the Semantics and Logics of Reactive Systems[A]. in:proceedingsof the 12th Colloquium on Automata, Languages andProgramming[C]. London, UK:Springer-Verlag.1985:15-32
2/2 首页 上一页 1 2 |
