Wireless communications provide higher transmission rate than cellular systems, and are very convenient to deploy with important flexibility. However, many serious security problems obstruct its widely adoption. IEEE 802.11i standard is designed to replace the original Wired Equivalent Privacy (WEP) which provides poor security safeguard. 802.11i proposes an exciting concept named RSNA (Robust Security Network Association). It adopts many security mechanisms to form an integrated and cooperative-working unit to provide confidentiality, integrity, secure access control and availability of wireless communications. As a significant part of 802.11i, 4way handshake protocol is adopted to implement key management and secure the wireless transmission between the mobile supplicant and the authenticator. Therefore, it is quite necessary and important to perform formal security verification of current 4-way handshake protocol in order to make better analysis of its security and performance, and improve its reliability and efficiency.
Many research focused on 802.11i security analysis, especially on the key management protocols. They find several design flaws and propose effective improvements. However, some of their results  may not have strong reliability and accuracy because they do not utilize formal specification and verification methods. Furthermore, some proposed repairs do not sound convictive without enough security and performance evaluation. In this paper, we adopt formal specification and verification methods to analyze the 4-way handshake protocol. Our contributions are listed as follows:
• Formal models of original 4-way handshake protocol are presented. We utilize two kinds of High- level Petri Nets (HPN): M-Nets and Colored Petri Nets (CPNets) as modeling tools. They are capable of exactly specifying both protocol framework and functional details.
• Formal verification is performed to verify whether the 4-way handshake protocol can provide strong security guarantee. We utilize model checking and insecure states deduction methods to carry out the security verification based on HPN models. Through such integrated verification, a vulnerability to DoS attack during handshake is confirmed and analyzed.
• A new improvement named enhanced two-way handshake protocol is proposed. According to our security analysis and performance evaluation, it is more reliable and costs less computation and communication time. The rest of this paper is structured as follows. Section II briefly introduces the HPN based formal verification methods. Section III presents the modeling and verification of the 4-way handshake protocol and compares such two verifications. A new improvement is proposed in section IV with a security and performance discussion. The conclusion and future work are drawn in section V.
Key management is a significant part of secure wireless communication. In IEEE 802.11i standard, 4-way handshake protocol is designed to exchange key materials and generate a fresh pairwise key for subsequent data transmissions between the mobile supplicant and the authenticator. Due to several design flaws, original 4-way handshake protocol cannot provide satisfying security and performance. In this study, we adopt formal specification and verification methods to analyze the 4-way handshake protocol. We give its formal models utilizing two kinds of High-level Petri Nets. Based on these formal models, we use two verification methods, model checking and insecure states deduction, to perform an integrated security verification process. The verification results confirm that the 4way handshake protocol is vulnerable to Denial-of-Service attack during handshake. To repair such vulnerability, we propose an improved key management scheme named enhanced two-way handshake protocol. According to security analysis and performance evaluation, our proposal could provide stronger security capability and cost less computation and communication time.
According to above verification results, the 4-way handshake protocol is vulnerable to a kind of DoS attack . The authenticator firstly sends Msg1 and waits for Msg2 in a period of timeout. If the authenticator does not receive Msg2 before timeout, it will retransmit Msg1. Therefore the supplicant calculates a new PTK every time it receives Msg1. The intruder just makes good use of this weakness to launch an attack. Firstly, it forges a spurious Msg1 and sends it to the authenticator right after the authenticator sending normal Msg1. Mobile supplicant does not have strong ability to distinguish the genuine Msg1 from the forged one and considers the forged one as a retransmitted packet. It deals with them in the same way and computes PTK twice. When the normal Msg3 arrives, verifying the MIC in Msg3 will be destined to fail. Such behaviors result in the unexpected termination of handshake.
Enhanced Two-way Handshake Protocol Ref. proposes an improvement named Nonce Re-use. It can effectively avoid the DoS attack mentioned above. However, it may result in another DoS attacks against CPU resources. These two DoS attacks can not make a satisfying tradeoff. Ref. presents another improvement. It intends to reduce flows of 4-way handshake, but effectively avoids this DoS attacks. In this improvement, two kinds of counters are introduced to prevent replay attacks, but it is quite hard to synchronize the counters. What is worse, installing PTK process needs a timeout period. The additional cost obstructs the adoption of two-way handshake protocol.
Security Analysis The purpose of original 4-way handshake includes three aspects. First, confirm both sides have the same PMK. Second, generate PTK with nonces provided by each side. Third, install PTK to synchronously protect the following process. The enhanced two-way handshake protocol we proposed can effectively achieve these purposed without introducing other vulnerability and security weakness.
It is a significant issue to design secure and efficient key management protocol in 802.11i standard. The original 4-way handshake protocol could not provide satisfying security and performance. In this paper, we model the 4-way handshake protocol with two kinds of High-level Petri Nets. Based on these formal models, we perform an integrated formal verification using model checking method and insecure states deduction methods. The verification results show that the 4way handshake protocol is vulnerable to DoS attack during handshake. To repair such vulnerability, we propose a new improvement, called enhanced two-way handshake protocol. According to security analysis and performance evaluation, our proposal is a more reliable key management scheme and costs less computation and communication time. Our future research will focus on the simulation study and the actual implementation of the enhanced two-way handshake protocol. We shall verify its security under more attack models, and its performance will be measured and compared with other WLAN key management protocols.