【作者】 陈力琼；

【导师】 陈克非；

【作者基本信息】 上海交通大学 ， 计算机系统结构， 2008， 硕士

【摘要】 随着Internet技术的发展,安全协议在电子商务和电子政务中的应用越来越多。与此相应的就是人们对协议的安全性更加关注,随之涌现出各种安全协议的形式化分析方法。本文简要介绍了串空间模型的符号系统及其基本概念和理论,分析了基于串空间模型的极小元、理想与诚实、认证测试方法这三个分支的原理和应用场合,并体现了串空间模型的特点及优势。在此基础上,本文以广义的挑战-应答协议和网络上广泛使用的SSL/TLS握手协议为例,用串空间模型中的相关符号和丛图对协议进行建模,并在此基础上用认证测试方法分别对广义和实际协议进行分析找到了协议的漏洞及具体攻击路径,在对相关协议改进的同时还归纳出对称和非对称密码体制下协议分析和设计的一套指导原则,利用这些原则去分析相应的网络协议,能够得到较好的结果,这进一步扩充了串空间模型在协议分析领域中的应用,并很大程度上地证明了串空间模型的理论及实践价值。另外,串空间模型的基本概念和理论及其在协议分析上的应用尚存在一些局限和缺陷。本研究从串空间模型对各类密码操作和安全特性的表示出发,对其符号系统、基本假设、攻击者能力、消息格式及串空间的各个分支(特别是认证测试方法)等各方面进行了一定程度上的改进和拓展。据此本文还用Yahalom协议验证了拓展的认证测试方法在分析协议及其各种安全特性上的能力和优势,证明它能作为一种指导协议设计的有效工具。此外,凭借串空间模型的符号和丛图对认证协议进行建模,汲取逻辑推理和模型检测等各类形式化分析方法的优势,本文定义了一套全新的协议分析方法--基于消息匹配的认证协议分析方法,并详细解释了该方法的原理和概念,阐述了具体的分析步骤。此方法通过在攻击者扮演不同角色的情况下,用常量或变量在各个阶段对协议的基本元素进行描述,并在分析过程中给变量逐步赋值,同时让协议主体通过匹配消息的格式来寻找协议的漏洞。本文以Needham-Schroeder protocol为例,介绍了如何在实际协议分析中运用此方法找出协议的攻击路径及相应的改进方法,最后还结合串空间的其他分支进一步简化了分析过程,也从另一方面对串空间模型进行了拓展和应用。更多还原

【Abstract】 With the development of Internet technology, security protocols play a more and more important role in e-business and e-government application. Due to so much attention paid on the field of security protocols analysis, kinds of formal methods for protocol analysis spring up during recent years. we introduce the basic concept and theory of strand space and analyze three branches of strand space in detail, not only their theory but also how to apply them to analyze protocols in practice. the character and advantage of strand space can be demonstrated.Then, by virtue of strand space, we analyze general challeange-response protocol and SSL/TLS handshake protocol in a careful way. By modeling protocols with strand space, we give a detail analysis on corresponding protocols under different cryptography system step by step. As a result, we find the effective attack of these protocols through authentication test and hereby modify the implementation of the protocols. In addition, we obtain some important principles for protocol analysis and design which can be applied to solve related problems in the filed of security protocols. All the above extend the application of strand space, and represent the value of strand space both in theory and practice.Moreover, strand space still has some flaws in some aspects. On the focus of cryptography operation and security goals analyzed by strand space, the reaseach perfects some branches of strand space besides its basic concept, premise and capability of attackers. Specially, applying the extended branch of authentication test to analyze Yahalom protocol, we can get good result to prove the the performance of the amelioration. Furthermore, it can help design protocol to a certain extent.Modeling the protocols by the bundle chart of strand space, the research put forwad a new method for protocol analysis based on message matching. This method not only absorbs the merits of some methods about logic reasoning and model checking, but also has its own complete theory and steps for protocol analysis. Through assigning constants to variable for elements of protocols, honest principles can find attacks by matching the form of message during different roles played by attackers. Take Needham-Schroeder protocol as an example, we execute this method step by step and concequently find the flaw of this protocol. Then we can also combine the exsiting branches of strand space to simplify this new method. In conclusion, This new formal method is an important and useful xtension to strand space .更多还原