Security Verification of 802.11i 4-Way Handshake Protocol

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 pair-wise 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 paper, the authors adopt formal specification and verification methods to analyze the 4-way handshake protocol. They give its formal models utilizing two kinds of High-level Petri Nets. Based on these formal models, they use two verification methods, model checking and insecure states deduction, to perform an integrated security verification process.