串空间模型的拓展和应用
|
摘要
随着Internet技术的发展,安全协议在电子商务和电子政务中的应用越来越多。与此相应的就是人们对协议的安全性更加关注,随之涌现出各种安全协议的形式化分析方法。本文简要介绍了串空间模型的符号系统及其基本概念和理论,分析了基于串空间模型的极小元、理想与诚实、认证测试方法这三个分支的原理和应用场合,并体现了串空间模型的特点及优势。
在此基础上,本文以广义的挑战-应答协议和网络上广泛使用的SSL/TLS握手协议为例,用串空间模型中的相关符号和丛图对协议进行建模,并在此基础上用认证测试方法分别对广义和实际协议进行分析找到了协议的漏洞及具体攻击路径,在对相关协议改进的同时还归纳出对称和非对称密码体制下协议分析和设计的一套指导原则,利用这些原则去分析相应的网络协议,能够得到较好的结果,这进一步扩充了串空间模型在协议分析领域中的应用,并很大程度上地证明了串空间模型的理论及实践价值。
另外,串空间模型的基本概念和理论及其在协议分析上的应用尚存在一些局限和缺陷。本研究从串空间模型对各类密码操作和安全特性的表示出发,对其符号系统、基本假设、攻击者能力、消息格式及串空间的各个分支(特别是认证测试方法)等各方面进行了一定程度上的改进和拓展。据此本文还用Yahalom协议验证了拓展的认证测试方法在分析协议及其各种安全特性上的能力和优势,证明它能作为一种指导协议设计的有效工具。
此外,凭借串空间模型的符号和丛图对认证协议进行建模,汲取逻辑推理和模型检测等各类形式化分析方法的优势,本文定义了一套全新的协议分析方法--基于消息匹配的认证协议分析方法,并详细解释了该方法的原理和概念,阐述了具体的分析步骤。此方法通过在攻击者扮演不同角色的情况下,用常量或变量在各个阶段对协议的基本元素进行描述,并在分析过程中给变量逐步赋值,同时让协议主体通过匹配消息的格式来寻找协议的漏洞。本文以Needham-Schroeder protocol为例,介绍了如何在实际协议分析中运用此方法找出协议的攻击路径及相应的改进方法,最后还结合串空间的其他分支进一步简化了分析过程,也从另一方面对串空间模型进行了拓展和应用。
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 .
在此基础上,本文以广义的挑战-应答协议和网络上广泛使用的SSL/TLS握手协议为例,用串空间模型中的相关符号和丛图对协议进行建模,并在此基础上用认证测试方法分别对广义和实际协议进行分析找到了协议的漏洞及具体攻击路径,在对相关协议改进的同时还归纳出对称和非对称密码体制下协议分析和设计的一套指导原则,利用这些原则去分析相应的网络协议,能够得到较好的结果,这进一步扩充了串空间模型在协议分析领域中的应用,并很大程度上地证明了串空间模型的理论及实践价值。
另外,串空间模型的基本概念和理论及其在协议分析上的应用尚存在一些局限和缺陷。本研究从串空间模型对各类密码操作和安全特性的表示出发,对其符号系统、基本假设、攻击者能力、消息格式及串空间的各个分支(特别是认证测试方法)等各方面进行了一定程度上的改进和拓展。据此本文还用Yahalom协议验证了拓展的认证测试方法在分析协议及其各种安全特性上的能力和优势,证明它能作为一种指导协议设计的有效工具。
此外,凭借串空间模型的符号和丛图对认证协议进行建模,汲取逻辑推理和模型检测等各类形式化分析方法的优势,本文定义了一套全新的协议分析方法--基于消息匹配的认证协议分析方法,并详细解释了该方法的原理和概念,阐述了具体的分析步骤。此方法通过在攻击者扮演不同角色的情况下,用常量或变量在各个阶段对协议的基本元素进行描述,并在分析过程中给变量逐步赋值,同时让协议主体通过匹配消息的格式来寻找协议的漏洞。本文以Needham-Schroeder protocol为例,介绍了如何在实际协议分析中运用此方法找出协议的攻击路径及相应的改进方法,最后还结合串空间的其他分支进一步简化了分析过程,也从另一方面对串空间模型进行了拓展和应用。
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 .
引文
[1] Syverson P. A taxonomy of replay attacks. In: Proceedings of the Computer Security Foundations Workshop. Los Alamitos: IEEE Computer Society Press, 1994. 187-191.
[2] Wang GL, Qing SH, Zhou ZF. Some new attacks upon authentication protocols. Journal of Software, 2001,12(6):907-913 (in Chinese with English abstract).
[3] R.M.Needham and M.D. Schroeder.Using encryption for authentication of large network2 of Computers.Communications of the ACM,1978,21(12):993-999
[4] D.Denning and G.Sacco.Timestamps in key distribution protocols.Communication of the ACM.1981.24(8)
[5] Dolev D, Yao A. On the security of public key protocols. IEEE Transactions on Information Theory, 1983,29(2):198~208.
[6] Zhou J, Gollmann D. Towards verification of non-repudiation protocols. In: International Refinement Workshop and Formal Methods Pacific 1998. Berlin: Springer-Verlag, 1998. 370-380.
[7] Qing SH. A new non-repudiation protocol. Journal of Software, 2000,11(10):1338-1343 (in Chinese with English abstract).
[8] Mitchell J, Mitchell M, Stern U. Automated analysis of cryptographic protocols using murphi. In: Proceedings of the 1997 IEEE Computer Society Symposium on Research in Security and Privacy. Los Alamitos: IEEE Computer Society Press, 1997. 141-151.
[9] David L.Dill,Andreas J.Drexler,Alan J.Hu and C. Han Yang. Protocol Verification as a Hardware Design Aid.1992 IEEE International Conference on Computer Design: VLSI Computers and Processors,IEEE Computer Society,1992,522-525
[10] Abadi M, Gordon AD. A calculus for cryptographic protocols: The spi calculus. In: Proceedings of the 4th ACM Conference on Computer and Communications Security. 1997. 36~47.
[11] Milner R, Parrow J, Walker D. A calculus of mobile processes. Information and Computation, 1992,100(1):1~77.
[12] F. Javier Thayer Fabrega, Jonathan C. Herzog, Joshua D. Guttman. Honest Ideals on Strand Spaces. Proceedings, 1998 Computer Security Foundations Workshop, June 1998
[13] J. D. Guttman and F. J. THAYER F′abrega. Authentication tests. In Proceedings, 2000IEEE Symposium on Security and Privacy. May, IEEE Computer Society Press, 2000.
[14] Joshua Guttman and F. Javier Thayer Fabrega. Authentication Tests and the Structure of Bundles Theoretical Computer Science, 2001.
[15] Perrig A, Song D. Looking for diamonds in the desert-extending automatic protocol generation to three-party authentication and key agreement. In: Proceedings of the 13th IEEE Computer Security Foundations Workshop. Los Alamitos: IEEE Computer Society Press, 2000. 64-76.
[16] Song D. Athena: A new efficient automatic checker for security protocol analysis. In:Proceedings of the 1999 IEEE Computer Security Foundations Workshop. Los Alamitos: IEEE Computer Society Press, 1999. 192-202.
[17] 吴光伟,董荣胜,基于串空间的Athena分析技术研究,计算机科学,2006,33(8):9-13
[18] 范红、冯登国. 安全协议理论与方法. 科学出版社 2003:42-44
[19] Burrows M, Abadi M, Needham R. A logic of authentication. Research Report 39, Digital Systems Research Center, 1989.
[20] Syverson, PF, van Oorschot PC. On unifying some cryptographic protocol logics. In: Proceedings of the 1994 IEEE Computer Society Symposium on Research in Security and Privacy. Los Alamitos: IEEE Computer Society Press, 1994. 14-28.
[21] Cervesato I, Durgin N, Kanovich M, Scedrov A. Interpreting strands in linear logic. In: Veith H, Heintze N, Clark E, eds. Proc. of the 2000 Workshop on Formal Methods and Computer Security. Chicago, 2000.
[22] Steve Schneider. Verifying authentication protocols with CSP. In Proceedings of the 10th IEEE Computer Security Foundations Workshop, pages 3{17. IEEE Computer Society Press, 1997.
[23] Millen JK. CAPSL: Common authentication protocol specification language. Technical Report, MP 97B48, The MITRE Corporation, 1997.
[24] Syverson, PF, van Oorschot PC. On unifying some cryptographic protocol logics. In: Proceedings of the 1994 IEEE Computer Society Symposium on Research in Security and Privacy. Los Alamitos: IEEE Computer Society Press, 1994. 14-28.
[25] Thayer FJ, Herzog JC, Guttman JD. Strand spaces: Why is a security protocol correct? In: Proceedings of the 1998 IEEE.Symposium on Security and Privacy. Los Alamitos: IEEE Computer Society Press, 1998.160-171.
[26] Thayer FJ, Herzog JC, Guttman JD. Strand spaces: Proving security protocols correct. Journal of Computer Security, 1999,7(2-3):191-230.
[27] J Heather , GLowe , S Schneider. How to prevent type flaw attacks on security protocols. In : Proceedings of the 13th IEEE Computer Security Foundations Workshop. IEEE Computer Society Press ,2000.255-268.
[28] Fábrega FJT, Herzog JC, Guttman JD. Honest ideals on strand spaces. In: Proc. of the 11th IEEE Computer Security Foundations Workshop. IEEE Computer Sociery Press, 1998.
[29] C.Mitchell. Limitations of challenge-response entity authentication.Electronic Letters. 1989:25(17).
[30] 卿斯汉,认证协议两种形式化分析方法的比较,软件学报,2003,14:1000-9825.
[31] 来学嘉,Seminar/报告/私人交流,认证协议,2006
[32] Netscape Communication Corp Kipp E.B. Hickman:The SSL Protocol. Feb, 9th, 1995
[33] T.Dieks,Request for Comments:246,http://www.ietf.org/rfc/rfc2246.txt.
[34] 刘家芬,周明天,认证测试方法对X.509认证协议的分析,计算机工程与应用,2006,08:23-25.
[35] Guttman J D, Herzog A L , Thayer F J. A uthentication and confidentiality via IPSec[EB/O L]. http: //www.ccs.neu.edu/home/guttman/esorics-ipsec. pdf, 2004207215.
[36] Guttman J D, Herzog A L , Thayer F J. A uthentication and confidentiality via IPSec[EB/OL]. http: //www.ccs.neu.edu/home/guttman/esorics-ipsec.pdf, 2004207215.
[37] KremerS, Rask in J F. Game analysis of abuse-free contract signing [EB/OL]. http://www.csl.sri. com/programs/security/csfw/csfw15/slides/kremer.pdf, 2004207215.
[38] Guttman J D. Security protocol design via authentication tests [EB/OL]. http://www.ccs.neu.edu/home/guttman/at-design.pdf, 2004207215.
[39] Feige U, Fiat A, Shamir A. Zero knowledge proofs of identity. In: Proc. of the 19th ACM Symp. Theory of Computing. 1987.210?217.
[40] 孙海波,林东岱,李莉,基于理想的协议安全分析,软件学报,2005,16:2150-2156.
[41] 杨明,罗军州,基于认证测试的安全协议分析,软件学报,2006,17:148-156.
[42] StallingsW 杨明译.密码编码学与网络安全,原理与实践(第2版)[M].北京:电子工业出版社,2002.
[43] 李谢华,李建华,杨树堂,基于认证测试的通用安全协议设计方法,上海交通大学学报,2006,40(3):524-527.
[44] 邢育红,卜凡金,李大兴,基于串空间模型的电子商务协议的形式化分析,计算机工程与应用,2006,3:123-126
[45] R.Needham and M.Schroeder. Usin encryption for authentication in large networks of computers. Communications of the ACM.December 1978,21(12):992-998
[46] Joshua D. Guttman and F. Javier Thayer F_abrega. Protocol independence through disjoint encryption. In Proceedings, 13th Computer Security Foundations Workshop. IEEE Computer
[2] Wang GL, Qing SH, Zhou ZF. Some new attacks upon authentication protocols. Journal of Software, 2001,12(6):907-913 (in Chinese with English abstract).
[3] R.M.Needham and M.D. Schroeder.Using encryption for authentication of large network2 of Computers.Communications of the ACM,1978,21(12):993-999
[4] D.Denning and G.Sacco.Timestamps in key distribution protocols.Communication of the ACM.1981.24(8)
[5] Dolev D, Yao A. On the security of public key protocols. IEEE Transactions on Information Theory, 1983,29(2):198~208.
[6] Zhou J, Gollmann D. Towards verification of non-repudiation protocols. In: International Refinement Workshop and Formal Methods Pacific 1998. Berlin: Springer-Verlag, 1998. 370-380.
[7] Qing SH. A new non-repudiation protocol. Journal of Software, 2000,11(10):1338-1343 (in Chinese with English abstract).
[8] Mitchell J, Mitchell M, Stern U. Automated analysis of cryptographic protocols using murphi. In: Proceedings of the 1997 IEEE Computer Society Symposium on Research in Security and Privacy. Los Alamitos: IEEE Computer Society Press, 1997. 141-151.
[9] David L.Dill,Andreas J.Drexler,Alan J.Hu and C. Han Yang. Protocol Verification as a Hardware Design Aid.1992 IEEE International Conference on Computer Design: VLSI Computers and Processors,IEEE Computer Society,1992,522-525
[10] Abadi M, Gordon AD. A calculus for cryptographic protocols: The spi calculus. In: Proceedings of the 4th ACM Conference on Computer and Communications Security. 1997. 36~47.
[11] Milner R, Parrow J, Walker D. A calculus of mobile processes. Information and Computation, 1992,100(1):1~77.
[12] F. Javier Thayer Fabrega, Jonathan C. Herzog, Joshua D. Guttman. Honest Ideals on Strand Spaces. Proceedings, 1998 Computer Security Foundations Workshop, June 1998
[13] J. D. Guttman and F. J. THAYER F′abrega. Authentication tests. In Proceedings, 2000IEEE Symposium on Security and Privacy. May, IEEE Computer Society Press, 2000.
[14] Joshua Guttman and F. Javier Thayer Fabrega. Authentication Tests and the Structure of Bundles Theoretical Computer Science, 2001.
[15] Perrig A, Song D. Looking for diamonds in the desert-extending automatic protocol generation to three-party authentication and key agreement. In: Proceedings of the 13th IEEE Computer Security Foundations Workshop. Los Alamitos: IEEE Computer Society Press, 2000. 64-76.
[16] Song D. Athena: A new efficient automatic checker for security protocol analysis. In:Proceedings of the 1999 IEEE Computer Security Foundations Workshop. Los Alamitos: IEEE Computer Society Press, 1999. 192-202.
[17] 吴光伟,董荣胜,基于串空间的Athena分析技术研究,计算机科学,2006,33(8):9-13
[18] 范红、冯登国. 安全协议理论与方法. 科学出版社 2003:42-44
[19] Burrows M, Abadi M, Needham R. A logic of authentication. Research Report 39, Digital Systems Research Center, 1989.
[20] Syverson, PF, van Oorschot PC. On unifying some cryptographic protocol logics. In: Proceedings of the 1994 IEEE Computer Society Symposium on Research in Security and Privacy. Los Alamitos: IEEE Computer Society Press, 1994. 14-28.
[21] Cervesato I, Durgin N, Kanovich M, Scedrov A. Interpreting strands in linear logic. In: Veith H, Heintze N, Clark E, eds. Proc. of the 2000 Workshop on Formal Methods and Computer Security. Chicago, 2000.
[22] Steve Schneider. Verifying authentication protocols with CSP. In Proceedings of the 10th IEEE Computer Security Foundations Workshop, pages 3{17. IEEE Computer Society Press, 1997.
[23] Millen JK. CAPSL: Common authentication protocol specification language. Technical Report, MP 97B48, The MITRE Corporation, 1997.
[24] Syverson, PF, van Oorschot PC. On unifying some cryptographic protocol logics. In: Proceedings of the 1994 IEEE Computer Society Symposium on Research in Security and Privacy. Los Alamitos: IEEE Computer Society Press, 1994. 14-28.
[25] Thayer FJ, Herzog JC, Guttman JD. Strand spaces: Why is a security protocol correct? In: Proceedings of the 1998 IEEE.Symposium on Security and Privacy. Los Alamitos: IEEE Computer Society Press, 1998.160-171.
[26] Thayer FJ, Herzog JC, Guttman JD. Strand spaces: Proving security protocols correct. Journal of Computer Security, 1999,7(2-3):191-230.
[27] J Heather , GLowe , S Schneider. How to prevent type flaw attacks on security protocols. In : Proceedings of the 13th IEEE Computer Security Foundations Workshop. IEEE Computer Society Press ,2000.255-268.
[28] Fábrega FJT, Herzog JC, Guttman JD. Honest ideals on strand spaces. In: Proc. of the 11th IEEE Computer Security Foundations Workshop. IEEE Computer Sociery Press, 1998.
[29] C.Mitchell. Limitations of challenge-response entity authentication.Electronic Letters. 1989:25(17).
[30] 卿斯汉,认证协议两种形式化分析方法的比较,软件学报,2003,14:1000-9825.
[31] 来学嘉,Seminar/报告/私人交流,认证协议,2006
[32] Netscape Communication Corp Kipp E.B. Hickman:The SSL Protocol. Feb, 9th, 1995
[33] T.Dieks,Request for Comments:246,http://www.ietf.org/rfc/rfc2246.txt.
[34] 刘家芬,周明天,认证测试方法对X.509认证协议的分析,计算机工程与应用,2006,08:23-25.
[35] Guttman J D, Herzog A L , Thayer F J. A uthentication and confidentiality via IPSec[EB/O L]. http: //www.ccs.neu.edu/home/guttman/esorics-ipsec. pdf, 2004207215.
[36] Guttman J D, Herzog A L , Thayer F J. A uthentication and confidentiality via IPSec[EB/OL]. http: //www.ccs.neu.edu/home/guttman/esorics-ipsec.pdf, 2004207215.
[37] KremerS, Rask in J F. Game analysis of abuse-free contract signing [EB/OL]. http://www.csl.sri. com/programs/security/csfw/csfw15/slides/kremer.pdf, 2004207215.
[38] Guttman J D. Security protocol design via authentication tests [EB/OL]. http://www.ccs.neu.edu/home/guttman/at-design.pdf, 2004207215.
[39] Feige U, Fiat A, Shamir A. Zero knowledge proofs of identity. In: Proc. of the 19th ACM Symp. Theory of Computing. 1987.210?217.
[40] 孙海波,林东岱,李莉,基于理想的协议安全分析,软件学报,2005,16:2150-2156.
[41] 杨明,罗军州,基于认证测试的安全协议分析,软件学报,2006,17:148-156.
[42] StallingsW 杨明译.密码编码学与网络安全,原理与实践(第2版)[M].北京:电子工业出版社,2002.
[43] 李谢华,李建华,杨树堂,基于认证测试的通用安全协议设计方法,上海交通大学学报,2006,40(3):524-527.
[44] 邢育红,卜凡金,李大兴,基于串空间模型的电子商务协议的形式化分析,计算机工程与应用,2006,3:123-126
[45] R.Needham and M.Schroeder. Usin encryption for authentication in large networks of computers. Communications of the ACM.December 1978,21(12):992-998
[46] Joshua D. Guttman and F. Javier Thayer F_abrega. Protocol independence through disjoint encryption. In Proceedings, 13th Computer Security Foundations Workshop. IEEE Computer