Formal Verification of the IEEE 802.11i WLAN Security Protocol
With the increased usage of Wireless LANs (WLANs), businesses and educational institutions are becoming more concerned about wireless network security. In this paper, the authors investigate the integrity of the security model developed by them based on 802.11i Robust Security Network (RSN), strengthening their desire towards establishing a secure wireless network environment. They have used the Symbolic Analysis Laboratory (SAL) tools to formally verify the Behavior Tree models. This paper presents the several Linear Temporal Logic (LTL) formulas established to prove the credibility of their model. They also discuss probable software issues that could arise during implementation. By examining all possible execution traces of the security protocol they have proved their implementation model to be complete and consistent.