Analysis of IEEE 802.11i WLAN Security Protocol

Abstract

As wireless LAN (WLAN) deployments increase, so does the challenge to provide these networks with adequate security. Business organizations, educational institutions and government co-operations are becoming more and more concerned about their e-security. The need for reliable and robust security mechanisms for WLANs is increasing. The latest WLAN security protocol IEEE 802.11i guarantees robust security with improved authentication, authorization and key distribution mechanisms. However, though the newest security protocol assures dependable communication sessions, the credibility of the three connection phases; security policy selection, authentication and key distribution needs further investigation. The loosely coupled state machines of the participating components can pave the way to security breaches. In this study we have investigated the integrity of these three phases. The analysis is carried out in two stages. Initially, the three phases are modeled using Genetic Software Engineering (GSE) methodology and then formally verified with Symbolic Analysis Laboratory (SAL) tools. We established several Linear Temporal Logic (LTL) formulas to model check our models. We have also examined and analyzed possible security threats due to various issues arising from software implementations and intruder behaviors.