【作者】 赵自强；

【导师】 王新庄； 范安东；

【作者基本信息】 成都理工大学 ， 计算数学， 2011， 硕士

【摘要】 安全协议是实现信息安全的基础,是网络安全通信的核心技术,它的正确性对网络的安全起着非常重要的作用,因此其自身的安全性问题已成为安全研究的重要内容。然而怎样保证安全协议的安全性,怎样设计协议才能使之满足安全性的要求,都是安全协议研究领域需要不断探索的问题。为了分析安全协议的安全性,研究人员提出了形式化分析的方法,并利用这类方法找出了许多协议的缺陷和攻击,对安全协议的设计和分析提供了很大的帮助。但是,出于安全的考虑,现在的安全协议加入了很多新的密码运算,而一些形式化分析方法在设计时没有对这些运算进行定义,所以无法用来分析某些安全协议。因此,本文以串空间模型、诚实理想和认证测试方法为基础,对这些问题进行了深入的研究,取得了一些的成果。论文的主要研究内容有以下几个方面:首先,对串空间模型、诚实理想及认证测试方法在经典安全协议分析中的应用做了深入研究,并通过对这些协议形式化的分析发现了其中存在的安全缺陷和攻击,给出了相应的攻击方式,并以分析结果为依据对这些协议提出了具体的改进方案。其次,在对串空间模型、诚实理想及认证测试方法深入研究的基础上,指出它们对加入了签名运算和哈希运算的安全协议不能有效分析,因此要对串空间模型、诚实理想及认证测试方法进行扩展。主要扩展了串空间中自由假设、子项关系以及入侵者模型,扩展了诚实理想的相关定义和定理,扩展了认证测试方法中的分量、测试分量、转换边、被转换边、输出测试方法、输入测试方法以及主动测试方法。最后,通过对一个不可否认电子邮件传输协议的分析,验证了扩展后的诚实理想及认证测试方法的准确性。更多还原

【Abstract】 Security protocol is the basis for achieving information security, is the core technology of network security Communication, Its correctness plays an important role in the network security, Therefore, the safety of their own has become an important part of security research. But how to ensure the safety of security protocols, how to design a protocol to make it meet the safety requirements, are issues need to continue to explore in security protocols research areas. In order to analyze the security of security protocols, the researchers propose a formal analysis, and use these methods found many shortcomings and attack methods of many protocols, Formal analysis provides a great help to the design and analysis of security protocols. However, the security protocols adds many new cryptographic operations for security considerations, and some formal methods have not define these operations, so it can not be used to analyze these security protocols. Therefore, this article These issues study these problems in-depth bases on strand space model, honest vision and authentication tests, obtains some results. The main research as follows:First, this article makes a thorough study in the strand space model, honest vision and authentication tests in the classic analysis of security protocols, and finds security flaws and attacks on these protocols through formal analysis of these agreements , gives the corresponding attack and specific improvements on these protocols based on the results .Secondly, we find the strand space model, honest vision and authentication tests can not be effectively analyzed these security protocol which join the signature algorithm and hash operations. So we extend the strand space model, honest vision and certification testing methods. We extend free hypothesis, child relationships, and the intruder model in the strand apace, definitions and theorem of honest ideal. We extends test weight, the conversion side, is converted to side, output test, input test and active testing.Finally, we verify the integrity of the expanded vision and the accuracy of authentication test through analysis an e-mail transmission protocol.更多还原