Formal Verification Of Security Protocol Adopted In 802.11I

Wireless Local Area Networks (WLAN), famous for its mobility and facility, has been widely deployed in recent years. With its fast development, kinds of attacks that aim to destroy access to WLAN or wiretap messages to learn certain secret have aroused public corcern. It is becoming more and more significant to establish an integrated security protocol which is much suitable for WLAN. Research on formal verification and analysis dealing with such problems is the topic of this paper.802.11i security standard, which is established by IEEE, is the primary research content in this paper, especially its four-way handshake protocol used to produce and manage the pair-wise keys used to encrypt data. Throughout the verification process of such protocol, a kind of DOS attack is found. Besides other two published solutions, a new improvement based on digital envelope technology has been proposed. AP and client make use of pair-wise master key and public key at the same time to encrypt the significant parameters which are used to produce pair-wire keys and check identity of each other. This improvement can eliminate the DOS attacks and make handshake process simpler, so the corresponding cost decreased.Two methods based on high-level Petri Net will be adopted in this paper. One is model checking technology based on Petri net, and the other is to check, by the...