【作者】 刘家芬；

【导师】 周明天；

【作者基本信息】 电子科技大学 ， 计算机应用技术， 2009， 博士

【摘要】 安全协议是安全共享网络资源的机制和规范，是构建网络安全环境的基石，其安全性对整个网络环境的安全起着至关重要的作用。由于协议安全属性的多样性和微妙性、攻击者模型的不确定性、协议运行环境的复杂性和协议会话的高并发性，安全协议的设计与分析至今仍是一项具有挑战性的工作。形式化方法的出现有助于精确定义安全协议的目标，准确描述安全协议的行为，验证安全协议是否满足预期目标。人们在安全协议的形式化分析上研究探索了近三十年，但这个领域仍然远未成熟。串空间理论的出现将安全协议形式化分析推向了一个新的高度，它以简洁、严谨、高效的特点成为近年来安全协议形式化领域的研究热点。在串空间理论上发展起来的认证测试方法以挑战-应答机制为基础，它充分利用串空间理论中代表事件因果关系的偏序结构，不仅继承了传统串空间模型简单直观、状态空间少的优点，还简化了证明过程，更符合安全协议形式化分析的发展方向。本文以认证测试方法在协议形式化分析和协议辅助设计中的应用、认证测试理论的扩展和改进，基于认证测试的协议自动化分析算法的设计与实现为主要内容，进行了系统深入的研究，取得了如下创新性成果：1．从协议分析的角度考虑对协议安全构成威胁的攻击类型和攻击者行为，着重对最为常见的攻击形式——重放攻击进行了分类研究。指出了Syverson重放攻击分类法的不足，按攻击产生的原因将重放攻击分成了五类，针对每个类别列出具体的攻击实例，并提出抵御该类攻击的原则性方法。这种新的重放攻击分类法对于更好地认识各种攻击的原理及寻找有效解决措施具有积极的意义。2．分别使用串空间最小元素方法、理想诚实方法和认证测试方法对Otway-Rees协议进行分析，总结了这三种方法进行协议分析的过程和特点，指出认证测试方法是前两者的归纳与概括，是理论上的进一步深入，其证明过程更简洁高效。使用认证测试方法对X．509三消息协议进行保密性和认证性分析，指出该协议存在的问题及可能受到的攻击；对协议加以改进，并使用认证测试方法证明了改进协议的正确性。3．结合协议设计一般原则和J．D．Guttman的协议设计思想，阐述了将认证测试方法用于辅助协议设计的可行性，提出了基于认证测试的通用协议设计思想。将协议设计过程分解为五个步骤，详细讨论了对称密钥体制和不对称密钥体制下构造认证测试的方法。并使用该方法设计了一个新的双向认证密钥协商协议，扩展了认证测试方法的应用范围。4．将基于认证测试的安全协议形式化分析过程标准化，解决了“认证测试方法的证明过程过于依赖分析人员的主观判断”和“认证测试元素出现位置可能不唯一”的问题，使得认证测试的应用过程更严谨规范，有利于自动化分析工具的实现。使用标准化方法对BAN-Yahalom协议进行分析，找到了针对该协议的一个已知攻击的更普遍形式。5．分析了认证测试方法中“测试元素不能是任何常规结点消息组成元素的真子项”这一局限性产生的根本原因，指出了Perrig和Song改进方案的漏洞，提出的新认证测试理论有效突破了认证测试定理无法分析多重加密协议的局限性，并通过理论证明和实例分析说明了新认证测试定理的正确性，进一步扩展了认证测试方法的应用范围。6．针对“认证测试理论不能识别类型缺陷攻击”的不足，结合强制类型检查思想，将消息项的类型和检查机制引入认证测试方法，使得认证测试方法可以根据应用需求检测出不同层次的类型缺陷攻击。并以Otway-Rees、Andrew RPC和Woo-Lam改进协议的分析为例，确认了这一改进的成功。7．根据认证测试理论的上述三点改进，模拟手工证明过程，设计了一个基于认证测试的协议自动化分析算法ATAPA并进行了初步实现。该算法利用串空间理论和认证测试方法的思想，有效避免了传统自动化分析工具的状态空间爆炸问题，同时能获得较高的分析效率。使用ATAPA算法对NSL协议、Woo-Lam改进协议的认证属性进行分析，得到了与目标一致的结论，一方面证明了协议自动化分析算法的成功，另一方面也验证了改进认证测试理论的正确性。更多还原

【Abstract】 Security protocols are designed for communication over insecure network. Security protocols work as core components of network security, so their correctness is crucial to network security. The designing and analyzing of security protocols remains a challenge for the subtlety of security goals, the uncertainty of penetrator model, the complexity of the running environment, and the high concurrency of protocol sessions. Formal methods contribute to define security goal of protocols precisely, describe behavior of protocol accurately, and verify whether the protocol meet the target correctly. Through nearly three decades of development, formal analysis of security protocols is immature yet. The emergence of strand space theory sets off a new upsurge of security protocols formal analysis. Strand space theory attracts sights of researchers soon for its compact model, precise definition and efficient proof. Authentication test based upon challenge-response mechanism is a novel method derived from strand space theory. It inherits advantages of strand space, simplifies proving process further, and provides more powerful analysis capabilities on authentication properties.This thesis makes an in-depth study of authentication test’s application in analyzing and designing of security protocols, expands authentication test theory in three aspects, and then designs an automatic protocol verification algorithm based on enhanced authentication test. Related efforts result in following major innovative achievements:1. Taxonomic study of replay attacks which may do great harm to security of protocols. Proposed a new classification method based on the underlying reasons for success of attacks. For each category, examples of successful attacks are listed and the methods against those attacks in principle are presented.2. Minimal-element method, ideal-honest method and authentication test method are separately used to verify secrecy and agreement properties of Otway-Rees protocol, followed by summarizing the characteristics of each method through comparison. It shows that authentication test is the most concise and efficient one for protocol analysis. As a case study, secrecy and agreement properties of X.509, an asymmetric key protocol, are verified, then found and amended the flaws in it.3. Applied authentication test to auxiliary protocol designing. Described the thought and procedure of designing protocols in terms of authentication test from standpoint of protocol analysis. Especially discussed the difference in constructing authentication test under symmetric-key and asymmetric-key cryptography. Designed a new mutual authentication protocol with key negotiation using that approach.4. Standardized the proving process of protocols’ security attributes with authentication test to make it more rigorous, formal and easy to implement in automatic tools. BAN-Yahalom is analyzed with the standardized proving method, and found a normal form of an attack to it.5. Illustrated the essential cause of limitation of authentication test, that test component cannot occurs as proper subterm of other component. Pointed out the deficiency in Perrig and Song’s authentication test version, then proposed the improved authentication test and proved its soundness both in formal and case study.6. With the idea of forced type checkage, defined different types for terms in messages, designed the inspection rules of authentication test method, so as to detect type-flaw-attacks on different levels according to application requirements. Confirmed the effectiveness of our improvements by analyzing Otway-Rees, Andrew RPC and Woo-Lam protocols.7. Imitating the manual proving process, designed an automatic protocol verification algorithm ATAPA based on improved authentication test theory mentioned above. With the programming implementation of the algorithm, verified the attributes of NSL and Woo-Lam protocols. Proved the soundness of both the algorithm and the improved authentication test theory.更多还原