WiMAX无线网络安全接入技术的研究
|
摘要
由于无线传输信道的开放性,任何具有接收能力的设备都可以随时对网络进行窃听,因此,无线网络与有线网络相比较更容易遭受窃听、非法访问等网络攻击。安全认证协议作为整个无线网络安全接入系统的基础保障,一旦遭受攻击,则将使整个安全系统受到严重的威胁,不但合法客户站不能正常访问系统、提取信息,而且攻击者可以非法登录基站,进行信息窃取、信息破坏,威胁整个无线网络安全。由此可见,安全认证协议在无线网络安全接入系统中的地位是十分关键和极其重要的。
WiMAX无线网络作为一种无线城域网技术,它主要是解决点到多点条件下的空中接口标准问题,它能向固定、携带、游牧和高速移动的设备提供宽带无线连接,以及在“最后一英里”宽带接入领域可以作为一些现有技术的无线替代品。复杂的网络应用环境就要求WiMAX无线网络安全接入技术具有较为良好的安全性,而且作为WiMAX无线网络安全接入技术的关键,WiMAX无线网络安全认证协议的安全性保证愈发显得更加重要。目前,对于WiMAX无线网络安全认证协议的安全性研究虽然取得了一定的成果,但是还是缺乏在一个安全框架下进行安全认证协议的设计,进而进行形式化分析与证明的研究。
为了有效应对WiMAX无线网络安全接入所面临的威胁,本文着眼于运用DDMP组合理论建立一种更加安全的适合WiMAX无线网络的安全认证协议。本文在对WiMAX无线网络安全接入技术和DDMP组合理论进行深入研究和分析的基础上,重点对WiMAX无线网络安全认证协议进行了研究。
在WiMAX无线网络安全认证协议的发展过程中,David Johnston为IEEE802.16e标准提出的PKMv2安全认证协议草案(DJ-PKMV2)对于IEEE802.16e-2005标准最后的制定起到了至关重要的作用。本文通过DDMP组合理论的协议演绎系统(PCL)对DJ-PKMv2安全认证协议进行了形式化分析,发现DJ-PKMv2安全认证协议存在交错攻击。之后基于DJ-PKMv2安全认证协议的基础构件,运用协议演绎系统(PDS)演绎设计了一种新的WiMAX无线网络安全认证协议,并且使用协议组合逻辑(PCL)给出了新协议的模块化正确性和安全性证明。新设计的FZM-PKMv2安全认证协议具有良好的密钥机密性和会话认证性,可以有效防御Lowe's攻击、交错攻击等网络攻击,与现有PKMv2安全认证协议版本相比更加适合WiMAX无线网络复杂的网络应用环境。
The openness of transmission channel enables the eavesdropping to the internet of any devices with reception ability. Thus,wireless network suffers from eavesdropping and illegal network attack comparatively more than wireline network. As the foundations for secured wireless access the security authentication protocol will threaten the whole security system once it gets attacked.The legal customers won't be able to access the system and to extract information and the attackers could unfortunately login the base stations illegally to steal information and to destroy them even, thus jeopardizing the security of the whole network. Therefore, the security authentication protocol plays a very critical role in wireless network secured access system.
The WiMAX wireless network as one of the wireless metropolitan area network technologies,It mainly solves the air interface standard problem under the point-multipoint condition, it could provide stationary, portable,mobile and high speed device with broadband wireless connection and could be wireless substitute of current last-mile broadband access technologies.The complicate network application environment requires high security of the WiMAX wireless secured access network as a key point for WiMAX wireless network secured access technologies.The security promise of WiMAX wireless network authentication protocol is becoming more and more important.Research progress on WiMAX wireless network authentication protocol has been made, but it lacks the method of design a new authentication protocol and present a formal correctness and security proof of the new protocol under a security framework.
In this paper, in order to effectively face the threaten of WiMAX Wireless Network Access Security Technology, we use the DDMP composition theory to derivate a new authentication protocol in WiMAX wireless network. Based on the research of WiMAX Wireless Network Access Security Technology and DDMP composition theory, we mainly analyzed the authentication protocol of WiMAX Wireless Network.
In the history of development of WiMAX wireless security authentication,the draft of PKMv2 security authentication (DJ-PKMV2) for 802.16e provided by David Johnston plays a vital role in the final formulation of standard IEEE 802.16e-2005. In this paper, we used the Protocol Composition Logic (PCL) to analyze the DJ-PKMv2 authentication protocol's security and to detect interleaving attack. Based on the DJ-PKMv2 authentication protocol's component,we used the Protocol Derivation System (PDS)to derivate a new authentication protocol(FZM-PKMv2) in WiMAX wireless network based on the vulnerability of system security. Finally we presented a formal correctness and security proof with Protocol Composition Logic(PCL).FZM-PKMv2 authentication protocol has key secrecy and session authentication, it can defend the Lowe's attack、the interleaving attack and so on. Compared with other PKMv2 security authentication protocol this new protocol is more suitable for complicate wireless network application environment used in WiMAX.
WiMAX无线网络作为一种无线城域网技术,它主要是解决点到多点条件下的空中接口标准问题,它能向固定、携带、游牧和高速移动的设备提供宽带无线连接,以及在“最后一英里”宽带接入领域可以作为一些现有技术的无线替代品。复杂的网络应用环境就要求WiMAX无线网络安全接入技术具有较为良好的安全性,而且作为WiMAX无线网络安全接入技术的关键,WiMAX无线网络安全认证协议的安全性保证愈发显得更加重要。目前,对于WiMAX无线网络安全认证协议的安全性研究虽然取得了一定的成果,但是还是缺乏在一个安全框架下进行安全认证协议的设计,进而进行形式化分析与证明的研究。
为了有效应对WiMAX无线网络安全接入所面临的威胁,本文着眼于运用DDMP组合理论建立一种更加安全的适合WiMAX无线网络的安全认证协议。本文在对WiMAX无线网络安全接入技术和DDMP组合理论进行深入研究和分析的基础上,重点对WiMAX无线网络安全认证协议进行了研究。
在WiMAX无线网络安全认证协议的发展过程中,David Johnston为IEEE802.16e标准提出的PKMv2安全认证协议草案(DJ-PKMV2)对于IEEE802.16e-2005标准最后的制定起到了至关重要的作用。本文通过DDMP组合理论的协议演绎系统(PCL)对DJ-PKMv2安全认证协议进行了形式化分析,发现DJ-PKMv2安全认证协议存在交错攻击。之后基于DJ-PKMv2安全认证协议的基础构件,运用协议演绎系统(PDS)演绎设计了一种新的WiMAX无线网络安全认证协议,并且使用协议组合逻辑(PCL)给出了新协议的模块化正确性和安全性证明。新设计的FZM-PKMv2安全认证协议具有良好的密钥机密性和会话认证性,可以有效防御Lowe's攻击、交错攻击等网络攻击,与现有PKMv2安全认证协议版本相比更加适合WiMAX无线网络复杂的网络应用环境。
The openness of transmission channel enables the eavesdropping to the internet of any devices with reception ability. Thus,wireless network suffers from eavesdropping and illegal network attack comparatively more than wireline network. As the foundations for secured wireless access the security authentication protocol will threaten the whole security system once it gets attacked.The legal customers won't be able to access the system and to extract information and the attackers could unfortunately login the base stations illegally to steal information and to destroy them even, thus jeopardizing the security of the whole network. Therefore, the security authentication protocol plays a very critical role in wireless network secured access system.
The WiMAX wireless network as one of the wireless metropolitan area network technologies,It mainly solves the air interface standard problem under the point-multipoint condition, it could provide stationary, portable,mobile and high speed device with broadband wireless connection and could be wireless substitute of current last-mile broadband access technologies.The complicate network application environment requires high security of the WiMAX wireless secured access network as a key point for WiMAX wireless network secured access technologies.The security promise of WiMAX wireless network authentication protocol is becoming more and more important.Research progress on WiMAX wireless network authentication protocol has been made, but it lacks the method of design a new authentication protocol and present a formal correctness and security proof of the new protocol under a security framework.
In this paper, in order to effectively face the threaten of WiMAX Wireless Network Access Security Technology, we use the DDMP composition theory to derivate a new authentication protocol in WiMAX wireless network. Based on the research of WiMAX Wireless Network Access Security Technology and DDMP composition theory, we mainly analyzed the authentication protocol of WiMAX Wireless Network.
In the history of development of WiMAX wireless security authentication,the draft of PKMv2 security authentication (DJ-PKMV2) for 802.16e provided by David Johnston plays a vital role in the final formulation of standard IEEE 802.16e-2005. In this paper, we used the Protocol Composition Logic (PCL) to analyze the DJ-PKMv2 authentication protocol's security and to detect interleaving attack. Based on the DJ-PKMv2 authentication protocol's component,we used the Protocol Derivation System (PDS)to derivate a new authentication protocol(FZM-PKMv2) in WiMAX wireless network based on the vulnerability of system security. Finally we presented a formal correctness and security proof with Protocol Composition Logic(PCL).FZM-PKMv2 authentication protocol has key secrecy and session authentication, it can defend the Lowe's attack、the interleaving attack and so on. Compared with other PKMv2 security authentication protocol this new protocol is more suitable for complicate wireless network application environment used in WiMAX.
引文
[1]唐雄燕.宽带无线接入技术及应用：WiMAX与WiFi.北京：电子工业出版社,2006
[2]王孙名,唐红,沈建国.新一代宽带无线移动通信网络管理的研究.通信技术,2007,40(12),201-205
[3]IEEE 802.16 and WiMAX:Broadband Wireless Access for everyone.Intel White Paper,2004,1-8
[4]http://standards.ieee.org/getieee802/80-2.16.html
[5]Xu.Sen,Matthews.Manton, Huang.Chin-Tser. Security issues in privacy and key management protocols of IEEE 802.16.44th Annual ACM Southeast Conference,Melbourne, Florida, USA,2006,113-118
[6]IEEE 802.16a Standard and WiMAX Igniting Broadband Wireless Access White Paper,2005
[7]IEEE Std.802.16TM-2004, IEEE Standard for Local and Metropolitan Area Networks,part 16,Air Interface for Fixed Broadband Wireless Access Systems, IEEE Press,2004
[8]IEEE Std.802.16TM-2005,IEEE Standard for Local and Metropolitan Area Networks,part 16,Air Interface for Fixed Broadband Wireless Access Systems, IEEE Press,2006
[9]Wang. Fan,Ghosh.Amitava, Love.Robert.IEEE 802.16e system performance: Analysis and simulations.IEEE International Symposium on Personal,Indoor and Mobile Radio Communications, PIMRC,2005,900-904
[10]Yarali.A, Rahman.S.WiMAX broadband wireless access technology:Services, architecture and deployment models.Electrical and Computer Engineering,2008. CCECE 2008, Canada,2008,77-82
[11]Kim Dongmyoung, Cai Hua,Na Minsoo,et al..Performance measurement over Mobile WiMAX/IEEE 802.16e network.2008 IEEE International Symposium on A World of Wireless,Mobile and Multimedia Networks,Newport Beach, CA, 2008,1-8
[12]Agrawal Dharma P, Gossain Hrishikesh, Cavalcanti Dave, et al.. Recent advances and evolution of WLAN and WMAN standards.IEEE Wireless Communications, USA,2008,54-55
[13]Daniel Johnsson, Fredrik Bjarkeson, WiMAX IEEE802.16e Worldwide Interoperability for Microwave Access.2008
[14]Frank Ohrtman:WiMAX Handbook.McGraw-Hill,2005
[15]Deepak Pareek:WiMAX Taking Wireless to the MAX.Auerbach Publications, 2006
[16]Mobile WiMAX-Part 1:A Technical Overview and Performance Evaluation. WiMAX Forum,2006
[17]Mobile WiMAX-Part 2:A Comparative Analysis.WiMAX Forum,2006
[18]D.Johnston, J.Walker, Overview of IEEE 802.16 Security. IEEE Security & Privacy,2004,40-48
[19]Derrick Boom.Denial of Service Vulnerabilities in IEEE 802.16 wireless Networks.IEEE Security & Privacy,2004,1-88
[20]Abdelrahman Elleithy, Alaa Abuzaghleh, Abdelshakour Abuzneid.A New Mechanism to Solve IEEE 802.16 Authentication Vulnerabilitie. IEEE 802.16, 2008,1-8
[21]Michel Barbeau.Rogue-Base Station Detection in WiMax/802.16 Wireless Access Networks.2006,61(11/12),1-14
[22]Tonderai Muchenje,Ntima Mabanza, Hippolyte Muyingi.Security Issues on a Converged WiFi and WiMAX.2007
[23]Fan Yang.Security Analysis and Improvement for Mesh Mode in IEEE 802.16. Wireless Communications,Networking and Mobile Computing, Wuhan,2006, 1-4
[24]Romano Fantacci, Leonardo Maccari, Tommaso Pecorella. A secure and performant token-based authentication for infrastructure and mesh 802.1X networks.2007,1-3
[25]Fuqiang Liu,Lei Lu.A WPKI-Based security mechanism for IEEE 802.16e. WiCOM International Conference,Wuhan,2006,1-4
[26]Taeshik Shon, Wook Choi. An analysis of mobile WiMAX security: vulnerabilities and solutions. Lecture Notes in Computer Science,2007, 4658/2007,88-97
[27]Sen Xu,Chin-Tser Huang. Attacks on PKM protocols of IEEE 802.16 and Its Later Versions.Proceedings of 3rd International Symposium on Wireless Communication System (ISWCS 2006),2006,1-5
[28]D.Johnston,J.Walker, Mutual Authentication for PKMv2.IEEE 2004,2004, 1-7
[29]Hung-Min Sun, Yue-Hsun Lin, Shuai-Min Chen, et al..Secure and fast handover scheme based on pre-authentication method for 802.16/WiMAX infrastructure networks.2007 IEEE Region 10 Conference, Taipei,2007,1-4
[30]A. Datta.Security analysis of network protocols:compositional reasoning and complexity-theoretic Foundations.[PhD Thesis].Computer Science Department, Stanford University,2005
[31]A. Datta, A. Derek, J.C. Mitchell, et al..A Derivation System for Security Protocols and its Logical Formalization.In Proceedings of 16th IEEE Computer Security Foundations Workshop, June 2003,109-125
[32]A. Datta, A. Derek, J. C. Mitchell, et al.. A Derivation System and Compositional Logic for Security Protocols.Journal of Computer Security (Special Issue of Selected Papers from CSFW-16),2005,13,423-482
[33]A. Datta, A. Derek, J. C. Mitchell, et al..Secure Protocol Composition.In Proceedings of 19th Annual Conference on Mathematical Foundations of Programming Semantics,Electronic Notes in Theoretical Computer Science, 2004,83,1-32
[34]A. Datta, A. Derek, J.C. Mitchell,et al..Protocol Composition Logic(PCL). Electronic Notes in Theoretical Computer Science,1 April 2007,172,1-47
[35]Kuhlman,Doug Moriarty, Ryan Braskich,et al..A Correctness Proof of a Mesh Security Architecture.Computer Security Foundations Symposium,2008.CSF '08. IEEE 21st,2008,315-330
[36]Cas Cremers.On the protocol composition logic PCL. Proceedings of the 2008 ACM symposium on Information, computer and communications security,2008, 66-76
[37]Changhua He, Mukund Sundararajan, Anupam Datta, et al.. A modular correctness proof of IEEE 802.11i and TLS.In Proceedings of the 12th ACM Conference on Computer and Communications Security (CCS'05), November 2005,1-14
[38]C. Meadows,D.Pavlovic. Deriving, attacking and defending the GDOI protocol. In Proceedings of 9th European Symposium On Research in Computer Security, September 2004,53-72
[39]J. C. Mitchell, A. Roy, A. Derek. Analysis of EAP-GPSK Authentication Protocol.2008,NUMB 5037,309-327
[40]A. Roy, A. Datta, J.C. Mitchell.Formal Proofs of Cryptographic Security of Diffie-Hellman-Based Protocols.2008, NUMB 4912,312-329
[41]M. Burrows, M. Abadi, and R. Needham. A logic of authentication. ACM Transactions on Computer Systems,1990,8(1),18-36
[42]M.Abadi,A. D.Gordon.A calculus for cryptographic protocols:the spi calculus. Information and Computation,1999,143,1-70
[43]L.C. Paulson.Proving properties of security protocols by induction.In 10th IEEE Computer Security Foundations Workshop,1997,70-83
[44]J.C. Mitchell, M.Mitchell,U.Stern.Automated analysis of cryptographic protocols using Mur'.In Proc.IEEE Symp.Security and Privacy,1997,141-151
[45]M. Burrows, M. Abadi, R. Needham. A logic of authentication. ACM Transactions on Computer Systems,1990,8(1),18-36
[46]R.M.Needham,M.D.Schroeder.Using encryption for authentication in large networks of computers.Communications of the ACM,1978,21(12),993-999
[47]D.Dolev,A. Yao.On the security of public-key protocols.IEEE Transactions on Information Theory,1983,2(29),1-26
[48]R. W. Floyd.Assigning meaning to programs. Mathematical Aspects of Computer Science:Proceedings of American Mathematics Society Symposia, 1967,19,19-31
[49]W.Diffie,P.C.van Oorschot,M.J. Wiener.Authentication and authenticated key exchanges.Designs,Codes and Cryptography,1992,2,107-125
[50]R. Bird, I. Gopal, A. Herzberg, et al..Systematic design of a family of attack resistant authentication protocols. IEEE Journal on Selected Areas in Communications,1993,1(5),679-693
[51]M.Bellare, R. Canetti, H.Krawczyk. A modular approach to the design and analysis of authentication and key exchange protocols.In Proceedings of 30th Annual Symposium on the Theory of Computing. ACM,1998,1-26
[52]N. Durgin, J.C.Mitchell, D.Pavlovic. A compositional logic for protocol correctness.In Proceedings of 14th IEEE Computer Security Foundations Workshop,2001,241-255
[53]N.Durgin,J.C. Mitchell, D.Pavlovic.A compositional logic for provingrity properties of protocols.Journal of Computer Security,2003,11,677-721
[54]Tie Man-xia, Li Jian-dong, Wang Yu-min.A correctness proof of WAPI key management protocol based on PCL. Journal of Electronics & Information Technology,2009,31(2),444-447
[55]Gavin Lowe.Some new attacks upon security protocols.Computer Security Foundations Workshop,1996,Proceedings,9th IEEE, Kenmare,Ireland,1996, 10-12
[56]朱英敏.IEEE 802.16无线城域网安全子层分析与研究[湖南大学硕士论文].长沙：湖南大学,2009,20-21
[2]王孙名,唐红,沈建国.新一代宽带无线移动通信网络管理的研究.通信技术,2007,40(12),201-205
[3]IEEE 802.16 and WiMAX:Broadband Wireless Access for everyone.Intel White Paper,2004,1-8
[4]http://standards.ieee.org/getieee802/80-2.16.html
[5]Xu.Sen,Matthews.Manton, Huang.Chin-Tser. Security issues in privacy and key management protocols of IEEE 802.16.44th Annual ACM Southeast Conference,Melbourne, Florida, USA,2006,113-118
[6]IEEE 802.16a Standard and WiMAX Igniting Broadband Wireless Access White Paper,2005
[7]IEEE Std.802.16TM-2004, IEEE Standard for Local and Metropolitan Area Networks,part 16,Air Interface for Fixed Broadband Wireless Access Systems, IEEE Press,2004
[8]IEEE Std.802.16TM-2005,IEEE Standard for Local and Metropolitan Area Networks,part 16,Air Interface for Fixed Broadband Wireless Access Systems, IEEE Press,2006
[9]Wang. Fan,Ghosh.Amitava, Love.Robert.IEEE 802.16e system performance: Analysis and simulations.IEEE International Symposium on Personal,Indoor and Mobile Radio Communications, PIMRC,2005,900-904
[10]Yarali.A, Rahman.S.WiMAX broadband wireless access technology:Services, architecture and deployment models.Electrical and Computer Engineering,2008. CCECE 2008, Canada,2008,77-82
[11]Kim Dongmyoung, Cai Hua,Na Minsoo,et al..Performance measurement over Mobile WiMAX/IEEE 802.16e network.2008 IEEE International Symposium on A World of Wireless,Mobile and Multimedia Networks,Newport Beach, CA, 2008,1-8
[12]Agrawal Dharma P, Gossain Hrishikesh, Cavalcanti Dave, et al.. Recent advances and evolution of WLAN and WMAN standards.IEEE Wireless Communications, USA,2008,54-55
[13]Daniel Johnsson, Fredrik Bjarkeson, WiMAX IEEE802.16e Worldwide Interoperability for Microwave Access.2008
[14]Frank Ohrtman:WiMAX Handbook.McGraw-Hill,2005
[15]Deepak Pareek:WiMAX Taking Wireless to the MAX.Auerbach Publications, 2006
[16]Mobile WiMAX-Part 1:A Technical Overview and Performance Evaluation. WiMAX Forum,2006
[17]Mobile WiMAX-Part 2:A Comparative Analysis.WiMAX Forum,2006
[18]D.Johnston, J.Walker, Overview of IEEE 802.16 Security. IEEE Security & Privacy,2004,40-48
[19]Derrick Boom.Denial of Service Vulnerabilities in IEEE 802.16 wireless Networks.IEEE Security & Privacy,2004,1-88
[20]Abdelrahman Elleithy, Alaa Abuzaghleh, Abdelshakour Abuzneid.A New Mechanism to Solve IEEE 802.16 Authentication Vulnerabilitie. IEEE 802.16, 2008,1-8
[21]Michel Barbeau.Rogue-Base Station Detection in WiMax/802.16 Wireless Access Networks.2006,61(11/12),1-14
[22]Tonderai Muchenje,Ntima Mabanza, Hippolyte Muyingi.Security Issues on a Converged WiFi and WiMAX.2007
[23]Fan Yang.Security Analysis and Improvement for Mesh Mode in IEEE 802.16. Wireless Communications,Networking and Mobile Computing, Wuhan,2006, 1-4
[24]Romano Fantacci, Leonardo Maccari, Tommaso Pecorella. A secure and performant token-based authentication for infrastructure and mesh 802.1X networks.2007,1-3
[25]Fuqiang Liu,Lei Lu.A WPKI-Based security mechanism for IEEE 802.16e. WiCOM International Conference,Wuhan,2006,1-4
[26]Taeshik Shon, Wook Choi. An analysis of mobile WiMAX security: vulnerabilities and solutions. Lecture Notes in Computer Science,2007, 4658/2007,88-97
[27]Sen Xu,Chin-Tser Huang. Attacks on PKM protocols of IEEE 802.16 and Its Later Versions.Proceedings of 3rd International Symposium on Wireless Communication System (ISWCS 2006),2006,1-5
[28]D.Johnston,J.Walker, Mutual Authentication for PKMv2.IEEE 2004,2004, 1-7
[29]Hung-Min Sun, Yue-Hsun Lin, Shuai-Min Chen, et al..Secure and fast handover scheme based on pre-authentication method for 802.16/WiMAX infrastructure networks.2007 IEEE Region 10 Conference, Taipei,2007,1-4
[30]A. Datta.Security analysis of network protocols:compositional reasoning and complexity-theoretic Foundations.[PhD Thesis].Computer Science Department, Stanford University,2005
[31]A. Datta, A. Derek, J.C. Mitchell, et al..A Derivation System for Security Protocols and its Logical Formalization.In Proceedings of 16th IEEE Computer Security Foundations Workshop, June 2003,109-125
[32]A. Datta, A. Derek, J. C. Mitchell, et al.. A Derivation System and Compositional Logic for Security Protocols.Journal of Computer Security (Special Issue of Selected Papers from CSFW-16),2005,13,423-482
[33]A. Datta, A. Derek, J. C. Mitchell, et al..Secure Protocol Composition.In Proceedings of 19th Annual Conference on Mathematical Foundations of Programming Semantics,Electronic Notes in Theoretical Computer Science, 2004,83,1-32
[34]A. Datta, A. Derek, J.C. Mitchell,et al..Protocol Composition Logic(PCL). Electronic Notes in Theoretical Computer Science,1 April 2007,172,1-47
[35]Kuhlman,Doug Moriarty, Ryan Braskich,et al..A Correctness Proof of a Mesh Security Architecture.Computer Security Foundations Symposium,2008.CSF '08. IEEE 21st,2008,315-330
[36]Cas Cremers.On the protocol composition logic PCL. Proceedings of the 2008 ACM symposium on Information, computer and communications security,2008, 66-76
[37]Changhua He, Mukund Sundararajan, Anupam Datta, et al.. A modular correctness proof of IEEE 802.11i and TLS.In Proceedings of the 12th ACM Conference on Computer and Communications Security (CCS'05), November 2005,1-14
[38]C. Meadows,D.Pavlovic. Deriving, attacking and defending the GDOI protocol. In Proceedings of 9th European Symposium On Research in Computer Security, September 2004,53-72
[39]J. C. Mitchell, A. Roy, A. Derek. Analysis of EAP-GPSK Authentication Protocol.2008,NUMB 5037,309-327
[40]A. Roy, A. Datta, J.C. Mitchell.Formal Proofs of Cryptographic Security of Diffie-Hellman-Based Protocols.2008, NUMB 4912,312-329
[41]M. Burrows, M. Abadi, and R. Needham. A logic of authentication. ACM Transactions on Computer Systems,1990,8(1),18-36
[42]M.Abadi,A. D.Gordon.A calculus for cryptographic protocols:the spi calculus. Information and Computation,1999,143,1-70
[43]L.C. Paulson.Proving properties of security protocols by induction.In 10th IEEE Computer Security Foundations Workshop,1997,70-83
[44]J.C. Mitchell, M.Mitchell,U.Stern.Automated analysis of cryptographic protocols using Mur'.In Proc.IEEE Symp.Security and Privacy,1997,141-151
[45]M. Burrows, M. Abadi, R. Needham. A logic of authentication. ACM Transactions on Computer Systems,1990,8(1),18-36
[46]R.M.Needham,M.D.Schroeder.Using encryption for authentication in large networks of computers.Communications of the ACM,1978,21(12),993-999
[47]D.Dolev,A. Yao.On the security of public-key protocols.IEEE Transactions on Information Theory,1983,2(29),1-26
[48]R. W. Floyd.Assigning meaning to programs. Mathematical Aspects of Computer Science:Proceedings of American Mathematics Society Symposia, 1967,19,19-31
[49]W.Diffie,P.C.van Oorschot,M.J. Wiener.Authentication and authenticated key exchanges.Designs,Codes and Cryptography,1992,2,107-125
[50]R. Bird, I. Gopal, A. Herzberg, et al..Systematic design of a family of attack resistant authentication protocols. IEEE Journal on Selected Areas in Communications,1993,1(5),679-693
[51]M.Bellare, R. Canetti, H.Krawczyk. A modular approach to the design and analysis of authentication and key exchange protocols.In Proceedings of 30th Annual Symposium on the Theory of Computing. ACM,1998,1-26
[52]N. Durgin, J.C.Mitchell, D.Pavlovic. A compositional logic for protocol correctness.In Proceedings of 14th IEEE Computer Security Foundations Workshop,2001,241-255
[53]N.Durgin,J.C. Mitchell, D.Pavlovic.A compositional logic for provingrity properties of protocols.Journal of Computer Security,2003,11,677-721
[54]Tie Man-xia, Li Jian-dong, Wang Yu-min.A correctness proof of WAPI key management protocol based on PCL. Journal of Electronics & Information Technology,2009,31(2),444-447
[55]Gavin Lowe.Some new attacks upon security protocols.Computer Security Foundations Workshop,1996,Proceedings,9th IEEE, Kenmare,Ireland,1996, 10-12
[56]朱英敏.IEEE 802.16无线城域网安全子层分析与研究[湖南大学硕士论文].长沙：湖南大学,2009,20-21