The Formal Analysis Methods Of Wireless Network Security Protocol

With the rapid growth of wireless network applications,network security has become an important issue,thus formal design and analysis of security protocol is rapidly developed and widely applied.In this paper,the formal methods for verifying security protocols are classified and analyzed from technological points of view.The developing history of analyzing approaches and techniques on security protocols are surveyed.The main results are as following:●The formal analysis method - BAN logical analysis is deeply studied.With BAN-like logic,WAI,the authentication infrastructure of Chinese WLAN security standard WAPI and its implementation plan,is analyzed on the security.●The computational complexity analysis methods are deeply studied with key points focused on Canetti-Krawczyk model and universally composable model.The main contents including:1.We analyzed the security of the IEEE 802.11i 4-way handshake protocol with the Canetti-Krawczyk(CK)model.The results show that 4-way handshake protocol can not only satisfy the definition of Session Key security defined in the CK model, but also the universal composition security,a stronger definition of security.2.With the CK model,we prove that WLAN Authentication and Privacy Infrastructure (WAPI)is insecure.A new protocol is proposed to fix the security problems of WAPI,especially those in the authentication and key agreement procedure.This protocol is designed and analyzed with a modular methodology and proved secure with the CK model,thus it can guarantee the desirable security attributes.3.We propose a bi-encryption-based session key distribu-tion protocol which is suit for the wireless environment.The proposed protocol is proven to satisfy the security definitions of the CK model,in the sense of the bi-encryption schemes satisfy the security of adaptive Chosen Ciphertext attack(CCA2).4.Existing RFID solutions cannot be applied directly in supply chain environment to address the security issues in this context,because of a set of special RFID security requirements to be addressed for supply chain management.In this paper, the unique set of security requirements for secure RFID communications in supply chains are identified,a universally composable model that satisfies the security requirements is propose,and a lightweight protocol is designed to realize the universally composable model.5.An anonymous Hash certification ideal function and a more universal certificate CA model are proposed.We define the security requirements and security notions for this model in the framework of universal composable security and prove in the plain model(not in the random-oracle model)that these security notions can be achieved using combinations of a secure digital signature scheme,a symmetrical encryption mechanism,a family of pseudorandom functions,and a family of oneway collision-free hash functions.●Finally,PCL,Protocol Composition Logic,the most developed result of formal analysis model is deeply studied.We propose a lightweight protocol for RFID communications in supply chains to securely realize visibility,together with a correctness proof based on the protocol composition logic model.