移动网络漫游认证协议的形式化研究
|
摘要
移动网络环境下实施漫游，可为那些由于工作或生活需要在不同区域间移动的用户提供很多的便利，也能为服务提供者带来很好的效益。要使得用户能随时随地的享受网络服务，并确保其个人信息安全，必须有一定的安全漫游协议作为技术支撑。在大量研究学者的共同努力下，目前已经提出了一些漫游的方案，但是在安全性方面或多或少都存在一些不足。从认证协议研究的背景入手，总结了传统认证协议存在的不能提供匿名性、灵活性差等问题，根据实际需求，对实现移动网络漫游的意义进行了论证，通过对前人研究成果的分析和归纳，比较了基于证书认证和基于身份认证研究的优缺点。在对移动IP协议、IEEE802.11协议、IAPP协议和基于身份加密的匿名漫游无线认证协议等几种常用的漫游认证协议进行分析研究后，提出了一种新的移动网络漫游认证协议SRAK，它集合了证书认证和身份认证的特点。研究了安全协议分析与设计的形式化方法，重点对符号理论方法中的BAN逻辑进行了研究，应用BAN逻辑找出了Aziz-Diffie协议中存在的不足，并提出了改进的措施，对Kailar逻辑和SVO逻辑进行了扩展和应用，同时结合认证测试理论和关联性理论对串空间的形式化分析方法也进行了一定的研究，并应用到对OR协议的分析中，发现其中存在的漏洞，针对性的进行了改进完善。运用Kailar逻辑的分析方法对新协议SRAK进行了分析、验证，证明该协议是安全可靠的。
The Implementation of roaming in mobile network environments can not onlybring a lot of convenience for those users who need to move between different areasdue to work or live, but also provide good benefits for service providers.To allowsusers to enjoy network services anytime and anywhere,and to ensure the security oftheir personal information, there must be a certain amount of secure roamingagreements as technical supports.A large number of research scholars have proposedsome of roaming programs in the joint efforts,but there are more or less someshortcomings in terms of security.This text begins with the background to the studyof authentication protocol, summarizes the problems of traditional authenticationprotocol such as no anonymity and no flexiblity.According to the actual demand, thispaper argues on the significance of mobile network roaming,and compared theadvantages and disadvantages between Certificate-based and Identity-basedauthentication study, by analyzing and generalizing the results of previousstudies.After the Analysis on the several commonly used protocol such as mobile IPprotocol,IEEE802.11, IAPP, and identity-based anonymous roaming wirelessauthentication protocol,this paper synthesizes its advantages and disadvantages,andproposes a new mobile network roaming authentication protocol SRAK,whichgathers together the features of certificate Certificate-based and Identity-basedauthentication.In addition, this paper has a research on the formal methods forsecurity protocol analysis and design, and makes focus on the BAN logic symboltheoretical method,which was used to inprove Aziz-Diffie protocol. It made Kailarlogic Extended and the SVO logic applied, and combined with certification testingtheory and relevance theory, it also carried out some research on the formal analysisof the string space method,which is applied to the analysis of OR, found that existsvulnerability,improving it.This article analyzes the new agreement SRAK by meansof Kailar logic theory,and prove that the protocol is safe and reliable.
The Implementation of roaming in mobile network environments can not onlybring a lot of convenience for those users who need to move between different areasdue to work or live, but also provide good benefits for service providers.To allowsusers to enjoy network services anytime and anywhere,and to ensure the security oftheir personal information, there must be a certain amount of secure roamingagreements as technical supports.A large number of research scholars have proposedsome of roaming programs in the joint efforts,but there are more or less someshortcomings in terms of security.This text begins with the background to the studyof authentication protocol, summarizes the problems of traditional authenticationprotocol such as no anonymity and no flexiblity.According to the actual demand, thispaper argues on the significance of mobile network roaming,and compared theadvantages and disadvantages between Certificate-based and Identity-basedauthentication study, by analyzing and generalizing the results of previousstudies.After the Analysis on the several commonly used protocol such as mobile IPprotocol,IEEE802.11, IAPP, and identity-based anonymous roaming wirelessauthentication protocol,this paper synthesizes its advantages and disadvantages,andproposes a new mobile network roaming authentication protocol SRAK,whichgathers together the features of certificate Certificate-based and Identity-basedauthentication.In addition, this paper has a research on the formal methods forsecurity protocol analysis and design, and makes focus on the BAN logic symboltheoretical method,which was used to inprove Aziz-Diffie protocol. It made Kailarlogic Extended and the SVO logic applied, and combined with certification testingtheory and relevance theory, it also carried out some research on the formal analysisof the string space method,which is applied to the analysis of OR, found that existsvulnerability,improving it.This article analyzes the new agreement SRAK by meansof Kailar logic theory,and prove that the protocol is safe and reliable.
引文
[1]周涛,徐静.改进的基于漫游场景的认证密钥交换协议[J].通信学报,2009,11.
[2]Simmons G J.Authentication theory coding theory[C].In Crypto’84.LNCS,1985,14(196):411-431.
[3]Needham R,Schroeder M.Using encryption for authentication in large networks of computers[J]. Communications of the ACM,1978,21(12):993-999.
[4]SUZUKIZ S,NAKADA K.An authentication technique based on distributed security management for the global mobility network[J].IEEE J Sel Areas in Commun,1997,15(8):1606-1617.
[5] BUTTYAN L,GBAGUIDI C.Extensions to an authentication tech-nique proposed for theglobal mobility network[J].IEEE Trans Com-mun,2000,48(3):373-376.
[6] HWANG KF,CHANG CC.A self-encryption mechanism for authen-tication of roaming andtelecomference services[J].IEEE TransWireless Commun,2003:400-407.
[7]赖晓龙,马建峰.可证明安全的基于802-11i的漫游认证协议[J].计算机学报,2005,12(28):02-2035.
[8] JIANG YX,LIN C.Mutual authentication and key exchange proto-cols for roaming servicesin wireless mobile networks[J].IEEE TransWireless Commun,2006,5(9):2569-2577.
[9]GIRAULT M.Self-certified public keys[A].Advances in Cryptology–Eurocrypt’91
[C].1991:490-497.
[10] SAEEDNIA S.Identity-based and Self-certified Key Exchange Proto-cols[A].Proc SecondAustralian Conf on Info.Security and Privacy[C].1997:303-313.
[11] SAEEDNIA S.A note on Girault’s self-certified model[J].Info Proc-essing Letters, Elsiver,2003,86(6):323-327.
[12] WU T C,CHANGE Y S,LIN T Y.Improvement of Saeednia’s selfcer-tified key exchangeprotocols[J]. Electronics letters,1998,34(1):1904-1905.
[13]顾永军,齐敬敬,王雅坤.基于身份加密的匿名漫游无线认证协议.计算机工程,2010,36(17):0176-0179.
[14]朱辉,李晖,苏万力等.基于身份的匿名无线认证方案[J].通信学报,2009,30(4):130-136.
[15] Canetti R, Krawczyk H. Analysis of Key-exchange Protocols and Their Use for BuildingSecure Channels[C]//Proc. of EuroCrypt’01. Innsbruck, Austria:[s. n.],2001:453-474.
[16]侯惠芳,刘光强,季新生等.基于公钥的可证明安全的异构无线网络认证方案[J].电子与信息学报,2009,31(10):2385-2391.
[17]Diffie w, Hellman ME. New Directions in Cryptography. IEEE Transaction on Inform ationTheory,1976,22(6):644一654.
[18]冯国柱,李超,吴翔.RSA公钥密码的信息论分析[J1.计算机工程与科学,2007,29(2):4-6.
[19] Rivest R, Shamir A, Adleman L. A method for obtaining digital signatures and public keycryptosystem [J]. Communications of ACM,1978,21(2):120-126.
[20]Oblitz N. Elliptic curve cryptosystems [J]. Mathematics of computation.1987,48:203-209.
[21] ElGamal T.A public key cryptosystem and a signature scheme based on discrete logarithms[J]. IEEE Transactions on Information Theory,1985,31:496-472.
[22]张丽媛.RSA密码算法的研究与实现[D].山东科技大学,2005,5.
[23]杨君,戴宗泽,杨栋毅,刘宏伟.一种椭圆曲线签名方案与基于身份的签名协议[J].软件学报,2000,11(10):1303-1306.
[24]朱辉.若干安全认证协议的研究与设计.电子科技大学博士学位论文.2009.
[25]孙旭,李雪梅,鲁长江.分组密码算法的研究与实现.成都理工大学学报,2006,33(6):640-644.
[26] William Stallings.Cryptography and Networks Security[M].北京:电子工业出版社,2006.
[27]杨义先,孙伟,钮心祈.现代密码新理论[M].北京:科学出版社,2002.
[28] Andrew S.Tanenbaum.潘爱民译.计算机网络[M].北京:清华人学出版社,2004,5.
[29]舒剑.认证密钥协商协议的设计与分析,电子科技大学博士学位论文,2010年12月.
[30]Garefalakis T.The Generalized Weil Pairing and the Discrete Logarithm Problem on ElliPticCurves.Theoretical Comput Sci,2004,32(l):59-72.
[31] Galbraith S,Harrision K,Soldera D.Implementing the Tate Pairing. Proeeedings of ANTS-V2002, LNCS2369. Berlin: Springer-Verlag,2002:324-337.
[32] Joux A.A One Round Protoeol for TriPartite Diffie-Hellman, Proeeedings of the4th Algorithmic Number Theory Symposium, LNCS1838. Berlin:Springer-Verlag,2000:385-394.
[33] Andrew Nash, William Duane, Celia Joseph, Derek Brink.张玉清,陈建奇,杨波,薛伟等译.公钥基础设施(PKI)实现和管理电子安全[M],清华大学出版社,2002.12.
[34] Pgutmann. PKI: it’s not dead, just resting [J].IEEE Computer,2002,35(8):41-49.
[35] J Linn,M Branchaud. An examination of asse rted PKI issues and proposed alternatives
[A].In Proceedings of the3rd Annual PK I R&D Workshop [C].Gaithers2-burg:NIST,2004.
[36] A Shamir. Identity-based cryptosystems and signature schemes[A].In Advances in Cryptology-Crypto′84[C]. Berlin:Springer-Verlag,1984:47-53.
[37] D Boneh,M Franklin. Identity-based encryption f rom the Weil pairing[A].In Advances inCryptology-CRYPTO2001[C]. Berlin: Springer-Berlag,2001:213-219.
[38]路晓明,冯登国.一种基于身份的多信任域网格认证模型[J].电子学报,2006,34(4):577-582.
[39]Lamport L.Password Authentication with Insecure Communication [J].Communications ofthe ACM,1981.24(11):770~772.
[40]C J Mitchell,L Chen.Comments on the S/KEY User Authentication Scheme[J].ACM Operating System Review,1996.30(4):12~16.
[41] Haller N,Metz C,Nesser P, et al. A One-Time Password System [S].RFC2289,1998,2.
[42]王涛,谢冬青,周洲仪.一种新的双向认证的一次性口令系统TAOTP[J].计算机应用研究,2005.9:128~130.
[43]陈炜,龙翔,高小鹏.一种用于移动IPv6的混合认证方法[J].软件学报,2005,16(09):1617-1624.
[44] Perkings C. IP Mobility Support for IPv4[S]. IETF RFC3344,2002.
[45]符刚,杨波.引入移动IP技术的WLAN安全漫游解决方案[J].计算机工程,2004,30(22):47-50.
[46] Aboba B, Simon D. PPP EAP TLS Authentication Protocol, RFC2716[S].1999:10-15.
[47]Josefsson S, Josefsson S, Glen Zorn, etal. Protected EAP Protocol (PEAP)[EB/OL]. http:www. globecom. net/ietf/draft/draft josefsson pppext eap tls eap06.html,2003:05-15.
[48]Haverinen H,Salowey J.EAP SIM Authentication[EB/OL].http:www.ietf.org/internet drafts/draft haverinen pppext eap sim10.txt.MAR,2003:05-15.
[49]马建峰,赖晓龙.802.11i RSN漫游认证协议的分析与设计[J].天津工业大学学报,2004,23(03):6-9.
[50]李富年.无线局域网内的漫游管理的研究和实现[J].网络与通信,2006,10:19-21.
[51]傅建庆,陈健,范容,陈小平,平玲娣.基于代理签名的移动通信网络匿名漫游认证协议[J].电子与信息学报,2011,33(1).
[52] Johnson D, Menezes A, and Vanstone S.The elliptic curve digital signature algorithm (ECDSA)[J]. International Journal of Information Security,2001,1(1):36-63.
[53] Lee Wei-bin and Chang-Kuo Y.A new delegation-based authentication protocol for use inportable communication systems[J].IEEE Transactions on Wireless Communications,2005,4(1):57-64.
[54]Ateniese G,Herzberg A,and Krawczyk H, et al.Untraceable mobility or how to travelincognito[J].Computer Networks,1999,31(8):785-899.
[55] Park J,Go J,Kim K.Wireless authentication protocol preserving user anonymity [C].InProceedings of the2001Symposium on Cryptography and Information Security. Janpan,Jan2001:23-26.
[56]侯惠芳,季新生,刘光强.异构无线网络中基于标识的匿名认证协议[J].通信学报,2011,32(5):153-161.
[57] Kang M H, Ryou H B,Choi W. Design of anonymity-preserving user authentication and keyagreement protocol for ubiquitous computing environments[C].In WINE2005. Hong Kong,China, December15-17,2005.
[58]彭华熹.一种基于身份的多信任域认证模型[J].计算机学报,2006,29(8):1271-1281.
[59]朱建明,马建峰.一种高效的具有用户匿名性的无线认证协议[J].通信学报,2004,25(6):12-18.
[60]彭华熹,冯登国.匿名无线认证协议的匿名性缺陷和改进[J].通信学报,2006,27(9):78-85.
[61]王亚弟,束妮娜,韩继红, eta1.密码协议形式化分析[M].北京:机械工业出版社,2006.
[62]王育民,刘建伟.通信网的安全一理论与技术[M].西安电子科技大学出版社,2000.
[63]卿斯汉.认证协议两种形式化分析方法的比较[J].计算机学报,2003,14(12):2028-2036.
[64] Lin Y d, Hsu Y C.Multihop cedllular: A new architecture for wireless communication[C]／Proceedings of the Conference on Computer Communications (Infocom’oo):Vol3,Mar26-30,2000,Tel Aviv,Is rael. Piscataway, NJ, USA: IEEE,2000:1273—1282.
[65] asin,D.A,M6dersheim S.and Vigano L,An On—the-Fly Model-Checker for SecurityProtocol Analysis. In8thEuropean Symposium on Research in Computer Security-ESORJC S’03,2003. LNCS2808: PP.253—270.
[66] Choo, K. K. R, Boyd C. and Hitchcoek Y, neimportance of proofs of security for keyestablishment protocols—Formal analysis of Jan—Chen,Yang.Shen·Shieh, Kiln-Huh—Hwang—Lee,Lin-Sun—Hwang, and Yeh—Sun protocols. Computer Communications,2006.29(15):2788-2797.
[67] Auamigeon,X. and Blanehet B.Reconstruction of Attacks against Cryptographic Protocols.18th IEEE Computer Security Foundations Workshop·CSFW’05,2005: PP.140-154.
[68] Cervesato,I., Durgin N., Lincoln P.D., ct a1., A Meta-Notation for Protocol Analysis.In12thIEEE Computer Security Foundations Workshop-CSFW’99,1999: PP.55-71.
[69]翁艳琴,石曙东,解颜铭.Aziz—Diffie协议的形式化分析及其改进[J],湖北师范学院学报（自然科学版）,2011,3(31):85~89.
[70]翁艳琴,石曙东,解颜铭.基于串空间认证测试理论的认证协议分析[J],微型机与应用,2012,3(31):51-54.
[71]杨超.无线网络协议的形式化分析与设计.西安电子科技大学博士学位论文,2008年6月.
[72] K.K.R.Choo,C.Boyd,Y.Hitchcock..Errors in computational complexityp roofs for protocols.Advances in Cryptology Asiaerypt2005,2005,624-643.
[73]Canetti,R. Universally Composable Security: A new paradigm for cryptographic protocols.In Proceedings of the42nd IEEE Symposium on Foundations of ComputerScience(FOCS),200:136-145.
[74]Canetti,R. and Krawczyk H. Universally composable notions of key exchange and securechannels.Advances in Cryptology·Euroerypt’02, Proceedings,2002.2332: pp.337-351.
[75]R.Canetti, H. Krawczyk.Analysis of key-exchangep rotocols and their use for buildingsecure channels.Advances in Cryptology-Eurocrypt2001,2001,453-474.
[76] R.Canetti. Universally Composable Security: A new paradigm for cryptographic protocols.In Proceedings of the42nd IEEE Symposium on Foundations of Computer Science(FOCS),2001,136-145.
[77]R.Canetti, H.Krawczyk. Universally composable notions of key exchange and securechannels. Advances in Cryptology-Eurocrypt2002, Proceedings,2002,337-351.
[78]曹春杰,杨超,马建峰,朱建明.WLAN Mesh漫游接入认证协议[J].计算机研究与发展,46(7):1102-1109,2009.
[79]石曙东.网络协议安全性分析中的逻辑化方法研究.博士学位论文,华中科技大学,2009.
[80]石曙东.一种安全协议的形式化验证方法[J].湖北师范学院学报(自然科学版),2004,1(24):15-18.
[2]Simmons G J.Authentication theory coding theory[C].In Crypto’84.LNCS,1985,14(196):411-431.
[3]Needham R,Schroeder M.Using encryption for authentication in large networks of computers[J]. Communications of the ACM,1978,21(12):993-999.
[4]SUZUKIZ S,NAKADA K.An authentication technique based on distributed security management for the global mobility network[J].IEEE J Sel Areas in Commun,1997,15(8):1606-1617.
[5] BUTTYAN L,GBAGUIDI C.Extensions to an authentication tech-nique proposed for theglobal mobility network[J].IEEE Trans Com-mun,2000,48(3):373-376.
[6] HWANG KF,CHANG CC.A self-encryption mechanism for authen-tication of roaming andtelecomference services[J].IEEE TransWireless Commun,2003:400-407.
[7]赖晓龙,马建峰.可证明安全的基于802-11i的漫游认证协议[J].计算机学报,2005,12(28):02-2035.
[8] JIANG YX,LIN C.Mutual authentication and key exchange proto-cols for roaming servicesin wireless mobile networks[J].IEEE TransWireless Commun,2006,5(9):2569-2577.
[9]GIRAULT M.Self-certified public keys[A].Advances in Cryptology–Eurocrypt’91
[C].1991:490-497.
[10] SAEEDNIA S.Identity-based and Self-certified Key Exchange Proto-cols[A].Proc SecondAustralian Conf on Info.Security and Privacy[C].1997:303-313.
[11] SAEEDNIA S.A note on Girault’s self-certified model[J].Info Proc-essing Letters, Elsiver,2003,86(6):323-327.
[12] WU T C,CHANGE Y S,LIN T Y.Improvement of Saeednia’s selfcer-tified key exchangeprotocols[J]. Electronics letters,1998,34(1):1904-1905.
[13]顾永军,齐敬敬,王雅坤.基于身份加密的匿名漫游无线认证协议.计算机工程,2010,36(17):0176-0179.
[14]朱辉,李晖,苏万力等.基于身份的匿名无线认证方案[J].通信学报,2009,30(4):130-136.
[15] Canetti R, Krawczyk H. Analysis of Key-exchange Protocols and Their Use for BuildingSecure Channels[C]//Proc. of EuroCrypt’01. Innsbruck, Austria:[s. n.],2001:453-474.
[16]侯惠芳,刘光强,季新生等.基于公钥的可证明安全的异构无线网络认证方案[J].电子与信息学报,2009,31(10):2385-2391.
[17]Diffie w, Hellman ME. New Directions in Cryptography. IEEE Transaction on Inform ationTheory,1976,22(6):644一654.
[18]冯国柱,李超,吴翔.RSA公钥密码的信息论分析[J1.计算机工程与科学,2007,29(2):4-6.
[19] Rivest R, Shamir A, Adleman L. A method for obtaining digital signatures and public keycryptosystem [J]. Communications of ACM,1978,21(2):120-126.
[20]Oblitz N. Elliptic curve cryptosystems [J]. Mathematics of computation.1987,48:203-209.
[21] ElGamal T.A public key cryptosystem and a signature scheme based on discrete logarithms[J]. IEEE Transactions on Information Theory,1985,31:496-472.
[22]张丽媛.RSA密码算法的研究与实现[D].山东科技大学,2005,5.
[23]杨君,戴宗泽,杨栋毅,刘宏伟.一种椭圆曲线签名方案与基于身份的签名协议[J].软件学报,2000,11(10):1303-1306.
[24]朱辉.若干安全认证协议的研究与设计.电子科技大学博士学位论文.2009.
[25]孙旭,李雪梅,鲁长江.分组密码算法的研究与实现.成都理工大学学报,2006,33(6):640-644.
[26] William Stallings.Cryptography and Networks Security[M].北京:电子工业出版社,2006.
[27]杨义先,孙伟,钮心祈.现代密码新理论[M].北京:科学出版社,2002.
[28] Andrew S.Tanenbaum.潘爱民译.计算机网络[M].北京:清华人学出版社,2004,5.
[29]舒剑.认证密钥协商协议的设计与分析,电子科技大学博士学位论文,2010年12月.
[30]Garefalakis T.The Generalized Weil Pairing and the Discrete Logarithm Problem on ElliPticCurves.Theoretical Comput Sci,2004,32(l):59-72.
[31] Galbraith S,Harrision K,Soldera D.Implementing the Tate Pairing. Proeeedings of ANTS-V2002, LNCS2369. Berlin: Springer-Verlag,2002:324-337.
[32] Joux A.A One Round Protoeol for TriPartite Diffie-Hellman, Proeeedings of the4th Algorithmic Number Theory Symposium, LNCS1838. Berlin:Springer-Verlag,2000:385-394.
[33] Andrew Nash, William Duane, Celia Joseph, Derek Brink.张玉清,陈建奇,杨波,薛伟等译.公钥基础设施(PKI)实现和管理电子安全[M],清华大学出版社,2002.12.
[34] Pgutmann. PKI: it’s not dead, just resting [J].IEEE Computer,2002,35(8):41-49.
[35] J Linn,M Branchaud. An examination of asse rted PKI issues and proposed alternatives
[A].In Proceedings of the3rd Annual PK I R&D Workshop [C].Gaithers2-burg:NIST,2004.
[36] A Shamir. Identity-based cryptosystems and signature schemes[A].In Advances in Cryptology-Crypto′84[C]. Berlin:Springer-Verlag,1984:47-53.
[37] D Boneh,M Franklin. Identity-based encryption f rom the Weil pairing[A].In Advances inCryptology-CRYPTO2001[C]. Berlin: Springer-Berlag,2001:213-219.
[38]路晓明,冯登国.一种基于身份的多信任域网格认证模型[J].电子学报,2006,34(4):577-582.
[39]Lamport L.Password Authentication with Insecure Communication [J].Communications ofthe ACM,1981.24(11):770~772.
[40]C J Mitchell,L Chen.Comments on the S/KEY User Authentication Scheme[J].ACM Operating System Review,1996.30(4):12~16.
[41] Haller N,Metz C,Nesser P, et al. A One-Time Password System [S].RFC2289,1998,2.
[42]王涛,谢冬青,周洲仪.一种新的双向认证的一次性口令系统TAOTP[J].计算机应用研究,2005.9:128~130.
[43]陈炜,龙翔,高小鹏.一种用于移动IPv6的混合认证方法[J].软件学报,2005,16(09):1617-1624.
[44] Perkings C. IP Mobility Support for IPv4[S]. IETF RFC3344,2002.
[45]符刚,杨波.引入移动IP技术的WLAN安全漫游解决方案[J].计算机工程,2004,30(22):47-50.
[46] Aboba B, Simon D. PPP EAP TLS Authentication Protocol, RFC2716[S].1999:10-15.
[47]Josefsson S, Josefsson S, Glen Zorn, etal. Protected EAP Protocol (PEAP)[EB/OL]. http:www. globecom. net/ietf/draft/draft josefsson pppext eap tls eap06.html,2003:05-15.
[48]Haverinen H,Salowey J.EAP SIM Authentication[EB/OL].http:www.ietf.org/internet drafts/draft haverinen pppext eap sim10.txt.MAR,2003:05-15.
[49]马建峰,赖晓龙.802.11i RSN漫游认证协议的分析与设计[J].天津工业大学学报,2004,23(03):6-9.
[50]李富年.无线局域网内的漫游管理的研究和实现[J].网络与通信,2006,10:19-21.
[51]傅建庆,陈健,范容,陈小平,平玲娣.基于代理签名的移动通信网络匿名漫游认证协议[J].电子与信息学报,2011,33(1).
[52] Johnson D, Menezes A, and Vanstone S.The elliptic curve digital signature algorithm (ECDSA)[J]. International Journal of Information Security,2001,1(1):36-63.
[53] Lee Wei-bin and Chang-Kuo Y.A new delegation-based authentication protocol for use inportable communication systems[J].IEEE Transactions on Wireless Communications,2005,4(1):57-64.
[54]Ateniese G,Herzberg A,and Krawczyk H, et al.Untraceable mobility or how to travelincognito[J].Computer Networks,1999,31(8):785-899.
[55] Park J,Go J,Kim K.Wireless authentication protocol preserving user anonymity [C].InProceedings of the2001Symposium on Cryptography and Information Security. Janpan,Jan2001:23-26.
[56]侯惠芳,季新生,刘光强.异构无线网络中基于标识的匿名认证协议[J].通信学报,2011,32(5):153-161.
[57] Kang M H, Ryou H B,Choi W. Design of anonymity-preserving user authentication and keyagreement protocol for ubiquitous computing environments[C].In WINE2005. Hong Kong,China, December15-17,2005.
[58]彭华熹.一种基于身份的多信任域认证模型[J].计算机学报,2006,29(8):1271-1281.
[59]朱建明,马建峰.一种高效的具有用户匿名性的无线认证协议[J].通信学报,2004,25(6):12-18.
[60]彭华熹,冯登国.匿名无线认证协议的匿名性缺陷和改进[J].通信学报,2006,27(9):78-85.
[61]王亚弟,束妮娜,韩继红, eta1.密码协议形式化分析[M].北京:机械工业出版社,2006.
[62]王育民,刘建伟.通信网的安全一理论与技术[M].西安电子科技大学出版社,2000.
[63]卿斯汉.认证协议两种形式化分析方法的比较[J].计算机学报,2003,14(12):2028-2036.
[64] Lin Y d, Hsu Y C.Multihop cedllular: A new architecture for wireless communication[C]／Proceedings of the Conference on Computer Communications (Infocom’oo):Vol3,Mar26-30,2000,Tel Aviv,Is rael. Piscataway, NJ, USA: IEEE,2000:1273—1282.
[65] asin,D.A,M6dersheim S.and Vigano L,An On—the-Fly Model-Checker for SecurityProtocol Analysis. In8thEuropean Symposium on Research in Computer Security-ESORJC S’03,2003. LNCS2808: PP.253—270.
[66] Choo, K. K. R, Boyd C. and Hitchcoek Y, neimportance of proofs of security for keyestablishment protocols—Formal analysis of Jan—Chen,Yang.Shen·Shieh, Kiln-Huh—Hwang—Lee,Lin-Sun—Hwang, and Yeh—Sun protocols. Computer Communications,2006.29(15):2788-2797.
[67] Auamigeon,X. and Blanehet B.Reconstruction of Attacks against Cryptographic Protocols.18th IEEE Computer Security Foundations Workshop·CSFW’05,2005: PP.140-154.
[68] Cervesato,I., Durgin N., Lincoln P.D., ct a1., A Meta-Notation for Protocol Analysis.In12thIEEE Computer Security Foundations Workshop-CSFW’99,1999: PP.55-71.
[69]翁艳琴,石曙东,解颜铭.Aziz—Diffie协议的形式化分析及其改进[J],湖北师范学院学报（自然科学版）,2011,3(31):85~89.
[70]翁艳琴,石曙东,解颜铭.基于串空间认证测试理论的认证协议分析[J],微型机与应用,2012,3(31):51-54.
[71]杨超.无线网络协议的形式化分析与设计.西安电子科技大学博士学位论文,2008年6月.
[72] K.K.R.Choo,C.Boyd,Y.Hitchcock..Errors in computational complexityp roofs for protocols.Advances in Cryptology Asiaerypt2005,2005,624-643.
[73]Canetti,R. Universally Composable Security: A new paradigm for cryptographic protocols.In Proceedings of the42nd IEEE Symposium on Foundations of ComputerScience(FOCS),200:136-145.
[74]Canetti,R. and Krawczyk H. Universally composable notions of key exchange and securechannels.Advances in Cryptology·Euroerypt’02, Proceedings,2002.2332: pp.337-351.
[75]R.Canetti, H. Krawczyk.Analysis of key-exchangep rotocols and their use for buildingsecure channels.Advances in Cryptology-Eurocrypt2001,2001,453-474.
[76] R.Canetti. Universally Composable Security: A new paradigm for cryptographic protocols.In Proceedings of the42nd IEEE Symposium on Foundations of Computer Science(FOCS),2001,136-145.
[77]R.Canetti, H.Krawczyk. Universally composable notions of key exchange and securechannels. Advances in Cryptology-Eurocrypt2002, Proceedings,2002,337-351.
[78]曹春杰,杨超,马建峰,朱建明.WLAN Mesh漫游接入认证协议[J].计算机研究与发展,46(7):1102-1109,2009.
[79]石曙东.网络协议安全性分析中的逻辑化方法研究.博士学位论文,华中科技大学,2009.
[80]石曙东.一种安全协议的形式化验证方法[J].湖北师范学院学报(自然科学版),2004,1(24):15-18.