基于串空间模型的形式化方法的扩展与应用
|
摘要
安全协议是实现信息安全的基础,是网络安全通信的核心技术,它的正确性对网络的安全起着非常重要的作用,因此其自身的安全性问题已成为安全研究的重要内容。然而怎样保证安全协议的安全性,怎样设计协议才能使之满足安全性的要求,都是安全协议研究领域需要不断探索的问题。为了分析安全协议的安全性,研究人员提出了形式化分析的方法,并利用这类方法找出了许多协议的缺陷和攻击,对安全协议的设计和分析提供了很大的帮助。但是,出于安全的考虑,现在的安全协议加入了很多新的密码运算,而一些形式化分析方法在设计时没有对这些运算进行定义,所以无法用来分析某些安全协议。因此,本文以串空间模型、诚实理想和认证测试方法为基础,对这些问题进行了深入的研究,取得了一些的成果。论文的主要研究内容有以下几个方面:
首先,对串空间模型、诚实理想及认证测试方法在经典安全协议分析中的应用做了深入研究,并通过对这些协议形式化的分析发现了其中存在的安全缺陷和攻击,给出了相应的攻击方式,并以分析结果为依据对这些协议提出了具体的改进方案。
其次,在对串空间模型、诚实理想及认证测试方法深入研究的基础上,指出它们对加入了签名运算和哈希运算的安全协议不能有效分析,因此要对串空间模型、诚实理想及认证测试方法进行扩展。主要扩展了串空间中自由假设、子项关系以及入侵者模型,扩展了诚实理想的相关定义和定理,扩展了认证测试方法中的分量、测试分量、转换边、被转换边、输出测试方法、输入测试方法以及主动测试方法。
最后,通过对一个不可否认电子邮件传输协议的分析,验证了扩展后的诚实理想及认证测试方法的准确性。
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.
首先,对串空间模型、诚实理想及认证测试方法在经典安全协议分析中的应用做了深入研究,并通过对这些协议形式化的分析发现了其中存在的安全缺陷和攻击,给出了相应的攻击方式,并以分析结果为依据对这些协议提出了具体的改进方案。
其次,在对串空间模型、诚实理想及认证测试方法深入研究的基础上,指出它们对加入了签名运算和哈希运算的安全协议不能有效分析,因此要对串空间模型、诚实理想及认证测试方法进行扩展。主要扩展了串空间中自由假设、子项关系以及入侵者模型,扩展了诚实理想的相关定义和定理,扩展了认证测试方法中的分量、测试分量、转换边、被转换边、输出测试方法、输入测试方法以及主动测试方法。
最后,通过对一个不可否认电子邮件传输协议的分析,验证了扩展后的诚实理想及认证测试方法的准确性。
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.
引文
[1] Meadows C.Formal verification of cryptographic protocols.a survey.In Proceedings of ASIACRYPT’94, Advances in Cryptology, volume 917 LNCS, Springer, 1994:135--150.
[2] D.Denning and G Sacco, Timestamps in key distribution protocols, Communications of the ACM, 1981, 24(8):533-536.
[3] Clark J.Jacob J.A survey of authentication protocol literature.Available via URL:http://www.cs.york.ac.uk/~jac/papers/drareviewps.ps,1997.
[4] Michael Burrows, Martin Abadi, Roger M Needham.A Logic of Authenticationg.ACM Transactions on Computer Sysrems, 1990, 8(1):18~36.
[5] Burrows M,Abadi M,Needham R.A logic of authentieation.In Proceedings of the Royal Society of London A,Vol426:233-271,1989.
[6]卿汉斯.安全协议的设计与逻辑分析[J].软件学报,2003,14(7):1300-1309.
[7] L.GOng,R.Needham and R.Yahalom.Reasoning about belief in cryptographic Protocols. Proceedings of the1990 IEEE Computer Society Symposium on Research in Security and Privacy,Los Alamitos:IEEE Computer Society Press,1990:234-248.
[8] M.Abadi, M.R.Tuttle.A semantics for a logic of authentieation.Proceedings of the 10th ACM Symposium.PrineiPles of Distributed Computing,Montreal, Canada:ACM Press,1991:201-216.
[9] P.van Oorsehot.Extending cryptographic logics of belief to key agreement Protocols.Proceedings of the lst ACM Conference on Computer and Communications Security, New York, USA:ACM Press,1993:233-243.
[10] P.Syverson and P.van Oorsehot.On unifying some cryptographic Protocol logics. Proceedings of the l994 IEEE Computer Society Symposium on Research in Security and Privacy, Los Alamitos:IEEE Computer Society Press,1994:14-28.
[11] R.Kailar.Aceountability in Electronic Commerce Protocols. IEEE Trans on Software Engineering, 22(5):313-328,1996.
[12] Woo T, Lam S S. A Semantic Model for Authentication Protocols. In Proceedings of IEEE Symposium on Security and Privacy, 1993:178~194.
[13] D.Dolev,and A.Yao.on the security of Public key Protocols. Technical Report No.STAN一CS一81-854, Dept.of Computer Science, Stanford University, May, 1981.
[14] F.Javier Thayer Fabrega,Jonathan C.Herzog,and Joshua D.Gutmian.Honest ideals on strand spaces. In Proceedings of the 11th IEEE computer security Foundations Workshop.IEEE Computer Society Press,June 1998.
[15] Joshua D,Guttman,F Javier Thayer Fabrega,Authentication tests. In Proceedings of the 2000 IEEE Symposium on Security and Privacy.IEEE Computer Society Press,2000,96-109.
[16] Thayer FJ,Herzog JC,Guttman JD.Strand Space: Proving Security Protocols Correct. Journal Of Computer Security,1999,7(2-3):191-230
[17] Guttman JD,Thayer FJ.Authentication Tests and the Structure of Bundles. Theoretical Computer Seience.2002,283(2):333-380.
[18] Even S, Goldreich O, Lempel A.A randomizing protocol for signing contracts. Communications of the ACM, 1985, 28(6):637-647.
[19]卿汉斯,一种新型的非否认协议[J].软件学报,2000:11(10):1338-1343.
[20]蔡永泉,朱勇,Zhou-Gollmann非否认协议的分析与改进[J].计算机应用研究,2007:24(7):222-245.
[21] Jonathan C.Herzog.The Diffie-Hellman Key-Agreement Scheme in the Strand-Space Model. In Proceedings,16th IEEE Computer Security Foundations Workshop,IEEECS Press,2003.
[22]张岚,何良生.串空间理论的扩展及其应用[J].计算机工程与应用,2006(18)136-138.
[23] Otway D, Rees. Efficient and timely mutual authentication.[J].Operating Systems Review, 1987,21(1):8-10.
[24]卿汉斯.安全协议[M].北京:清华大学出版社,2005:81-82.
[25]卿汉斯.安全协议[M].北京:清华大学出版社,2005:327-333.
[26]王亚弟,束妮娜,韩继红,王娜.密码协议形式化分析.[M].北京:机械工业出版社,2007,15-16.
[27]刘家芬.安全协议形式化分析中认证测试方法的研究[D].成都:电子科技大学,2008.
[28] Millen J,Clark Freedman S.The Interrogator: Protocol security analysis.IEEE Transactions on Software Engineering,1987,13(2):274~288.
[29] Millen J.The Interrogator Model. Proceedings of the 1995 IEEE Symposium on Security and Privacy, IEEE Computer Society Press,1995:251~260.
[30] Dolev D,Yao A.On the Security of Public Key Protocols.IEEE Transactions on Information Theory, 1983,29(2):198~208.
[31] Thayer F,Herzog J,Guttman J.Strand Space: Why is a Security Protocols Correct. In Proceedings of the 1998 IEEE Symposium on Security and Priacy,1998:160~171.
[32] Thayer F,Herzog J,Guttman J.Honest Ideals on Strand Space. In Proceedings of the IEEE Computer Security Foundations Workshop XI,1998.
[33] Guttman J, Fabrega J T. Authentication test and the Structure of Bundles. Theoretical Computer Science,2001.
[34]周宏斌,黄连生,桑田.基于串空间的安全协议形式化验证模型及算法[J].计算机研究与发展,2003,43(12):251-256
[35]范红,冯登国.安全协议理论与方法[M].北京:科学出版社,2003
[36]卿汉斯.密码学与计算机网络安全[M].北京:清华大学出版社, 2000.
[37]卿汉斯.安全协议[M].北京:清华大学出版社.2005
[38]方燕萍.串空间模型及其认证测试方法的扩展与应用[D].苏州:苏州大学,2009.
[39]王亮.电子商务安全协议的一种形式化分析方法[D].苏州:苏州大学,2010.
[40]卿汉斯.安全协议的设计与逻辑分析[J].软件学报,2003, 14(7):1300-1309
[41]冯登国.可证明安全性理论与方法研究[J].软件学报,2005, 16(10):1743-1756
[42]华东明.安全协议的形式化方法及其应用的研究:[D].北京:中国科学院计算技术研究所,2005
[43]王惠斌,祝跃飞,常青美.协议组合逻辑系统研究[J].郑州大学学报:理学版, 2008, 40(4): 56-59.
[44]蒋睿,李建华,潘理.基于Strand space模型的x509协议分析[J]上海交通大学学报.2004, 38(21):169 173.
[45]赵自强,胡国彪,张玉中.改进型Otway-Rees协议的串空间模型分析[J] .科技风,2011.3(下):70-71.
[46]杨明,罗军周.基于认证测试的安全协议分析[J],软件学报.2006,17(l):148-156
[47]李谢华,杨树堂.基于消息类型检测的认证测试分析方法[J].上海交通大学学报. 2007,41(l):85-89
[48]龙士工.串空间理论及其在安全协议分析中的应用研究[D].贵州:贵州大学:2007.
[49]怀进鹏,李先贤,密码代数模型及其安全性[J],中国科学E辑12(33) (2003),1087~1106.
[50]吴光伟,董荣胜,基于串空间的Athena分析技术研究[J],计算机科学,2006,33(8): 9-13.
[2] D.Denning and G Sacco, Timestamps in key distribution protocols, Communications of the ACM, 1981, 24(8):533-536.
[3] Clark J.Jacob J.A survey of authentication protocol literature.Available via URL:http://www.cs.york.ac.uk/~jac/papers/drareviewps.ps,1997.
[4] Michael Burrows, Martin Abadi, Roger M Needham.A Logic of Authenticationg.ACM Transactions on Computer Sysrems, 1990, 8(1):18~36.
[5] Burrows M,Abadi M,Needham R.A logic of authentieation.In Proceedings of the Royal Society of London A,Vol426:233-271,1989.
[6]卿汉斯.安全协议的设计与逻辑分析[J].软件学报,2003,14(7):1300-1309.
[7] L.GOng,R.Needham and R.Yahalom.Reasoning about belief in cryptographic Protocols. Proceedings of the1990 IEEE Computer Society Symposium on Research in Security and Privacy,Los Alamitos:IEEE Computer Society Press,1990:234-248.
[8] M.Abadi, M.R.Tuttle.A semantics for a logic of authentieation.Proceedings of the 10th ACM Symposium.PrineiPles of Distributed Computing,Montreal, Canada:ACM Press,1991:201-216.
[9] P.van Oorsehot.Extending cryptographic logics of belief to key agreement Protocols.Proceedings of the lst ACM Conference on Computer and Communications Security, New York, USA:ACM Press,1993:233-243.
[10] P.Syverson and P.van Oorsehot.On unifying some cryptographic Protocol logics. Proceedings of the l994 IEEE Computer Society Symposium on Research in Security and Privacy, Los Alamitos:IEEE Computer Society Press,1994:14-28.
[11] R.Kailar.Aceountability in Electronic Commerce Protocols. IEEE Trans on Software Engineering, 22(5):313-328,1996.
[12] Woo T, Lam S S. A Semantic Model for Authentication Protocols. In Proceedings of IEEE Symposium on Security and Privacy, 1993:178~194.
[13] D.Dolev,and A.Yao.on the security of Public key Protocols. Technical Report No.STAN一CS一81-854, Dept.of Computer Science, Stanford University, May, 1981.
[14] F.Javier Thayer Fabrega,Jonathan C.Herzog,and Joshua D.Gutmian.Honest ideals on strand spaces. In Proceedings of the 11th IEEE computer security Foundations Workshop.IEEE Computer Society Press,June 1998.
[15] Joshua D,Guttman,F Javier Thayer Fabrega,Authentication tests. In Proceedings of the 2000 IEEE Symposium on Security and Privacy.IEEE Computer Society Press,2000,96-109.
[16] Thayer FJ,Herzog JC,Guttman JD.Strand Space: Proving Security Protocols Correct. Journal Of Computer Security,1999,7(2-3):191-230
[17] Guttman JD,Thayer FJ.Authentication Tests and the Structure of Bundles. Theoretical Computer Seience.2002,283(2):333-380.
[18] Even S, Goldreich O, Lempel A.A randomizing protocol for signing contracts. Communications of the ACM, 1985, 28(6):637-647.
[19]卿汉斯,一种新型的非否认协议[J].软件学报,2000:11(10):1338-1343.
[20]蔡永泉,朱勇,Zhou-Gollmann非否认协议的分析与改进[J].计算机应用研究,2007:24(7):222-245.
[21] Jonathan C.Herzog.The Diffie-Hellman Key-Agreement Scheme in the Strand-Space Model. In Proceedings,16th IEEE Computer Security Foundations Workshop,IEEECS Press,2003.
[22]张岚,何良生.串空间理论的扩展及其应用[J].计算机工程与应用,2006(18)136-138.
[23] Otway D, Rees. Efficient and timely mutual authentication.[J].Operating Systems Review, 1987,21(1):8-10.
[24]卿汉斯.安全协议[M].北京:清华大学出版社,2005:81-82.
[25]卿汉斯.安全协议[M].北京:清华大学出版社,2005:327-333.
[26]王亚弟,束妮娜,韩继红,王娜.密码协议形式化分析.[M].北京:机械工业出版社,2007,15-16.
[27]刘家芬.安全协议形式化分析中认证测试方法的研究[D].成都:电子科技大学,2008.
[28] Millen J,Clark Freedman S.The Interrogator: Protocol security analysis.IEEE Transactions on Software Engineering,1987,13(2):274~288.
[29] Millen J.The Interrogator Model. Proceedings of the 1995 IEEE Symposium on Security and Privacy, IEEE Computer Society Press,1995:251~260.
[30] Dolev D,Yao A.On the Security of Public Key Protocols.IEEE Transactions on Information Theory, 1983,29(2):198~208.
[31] Thayer F,Herzog J,Guttman J.Strand Space: Why is a Security Protocols Correct. In Proceedings of the 1998 IEEE Symposium on Security and Priacy,1998:160~171.
[32] Thayer F,Herzog J,Guttman J.Honest Ideals on Strand Space. In Proceedings of the IEEE Computer Security Foundations Workshop XI,1998.
[33] Guttman J, Fabrega J T. Authentication test and the Structure of Bundles. Theoretical Computer Science,2001.
[34]周宏斌,黄连生,桑田.基于串空间的安全协议形式化验证模型及算法[J].计算机研究与发展,2003,43(12):251-256
[35]范红,冯登国.安全协议理论与方法[M].北京:科学出版社,2003
[36]卿汉斯.密码学与计算机网络安全[M].北京:清华大学出版社, 2000.
[37]卿汉斯.安全协议[M].北京:清华大学出版社.2005
[38]方燕萍.串空间模型及其认证测试方法的扩展与应用[D].苏州:苏州大学,2009.
[39]王亮.电子商务安全协议的一种形式化分析方法[D].苏州:苏州大学,2010.
[40]卿汉斯.安全协议的设计与逻辑分析[J].软件学报,2003, 14(7):1300-1309
[41]冯登国.可证明安全性理论与方法研究[J].软件学报,2005, 16(10):1743-1756
[42]华东明.安全协议的形式化方法及其应用的研究:[D].北京:中国科学院计算技术研究所,2005
[43]王惠斌,祝跃飞,常青美.协议组合逻辑系统研究[J].郑州大学学报:理学版, 2008, 40(4): 56-59.
[44]蒋睿,李建华,潘理.基于Strand space模型的x509协议分析[J]上海交通大学学报.2004, 38(21):169 173.
[45]赵自强,胡国彪,张玉中.改进型Otway-Rees协议的串空间模型分析[J] .科技风,2011.3(下):70-71.
[46]杨明,罗军周.基于认证测试的安全协议分析[J],软件学报.2006,17(l):148-156
[47]李谢华,杨树堂.基于消息类型检测的认证测试分析方法[J].上海交通大学学报. 2007,41(l):85-89
[48]龙士工.串空间理论及其在安全协议分析中的应用研究[D].贵州:贵州大学:2007.
[49]怀进鹏,李先贤,密码代数模型及其安全性[J],中国科学E辑12(33) (2003),1087~1106.
[50]吴光伟,董荣胜,基于串空间的Athena分析技术研究[J],计算机科学,2006,33(8): 9-13.