Model Checking Of WLAN IEEE 802.11 Authentication Protocol

The security of WLAN plays an extremely significant role in wireless technology. When IEEE802.11 is established, protocol emphasizes on open authentication and WEP authentication so as to supplement the security. The authentication protocol can make the wireless lan communication much safer and stable. As the latest generation of security protocol, IEEE802.11i proposes 4-way handshake protocol to administrate and distribute key, supplementing the blank space in WEP.This paper simulates and verifies the protocol by the means of model checking that is algorithm about automatical verification parallel or distributaion system. The key point of model checking is fomalization model establishment. Firstly, on the basis of traditional model establishment, this paper defines the conception of interior and exterior state of the model and formulates the model needed by SPIN at the moment of establishing. Secondly, starts the model checking of WEP. The results of this checking show that WEP authentication protocol has many defects. According to the circumstances in acual transportation and the defects of the key, starts the model checking of 4-way handshake to find out the flaw of this protocol in specific condition. Finally, analyzes and concludes the security of wirelss lan IEEE 802.11 through these two model checkings.Model checking authentical protocol is helpful in understanding, analyzing the protocol as well as finding out the defects through the characters of it. The results of these two model checkings can prove that WEP is so defective that it improper in wireless lan of highly security. At the same time, it also proves that 4-way handshake can help improve the key administration. However, the flaws of 4-way handshake in transportaion also influence the safety of protocol. The experiment results of this paper can be used as the theoretical reference for improving IEEE802.11.