串空间模型的拓展和应用

作     者：陈力琼 

作者单位：上海交通大学 

学位级别：硕士

导师姓名：陈克非

授予年度：2008年

学科分类：08[工学] 081201[工学-计算机系统结构] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

主      题：安全协议 形式化分析 串空间模型 认证测试方法 

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