Formal Verification of 802.11i using Strand Space Formalism

Despite an appealing desire to shift from wired to wireless domain and substantial deployment of wireless applications, wireless security is still a stumbling block. As a remedy, IEEE has designed a new protocol, 802.11i, for wireless local area networks addressing security issues. Formal analysis is important to ensure that protocols work properly without having to resort to tedious testing and debugging which can only show the presence of errors, never their absence. We analyze the protocol model for 802.11i in a formal setting. We translate the 802.11i protocol into Strand Space Model for protocol verification. We prove the authentication property of the resulting model using the Strand Space formalism. The intruder is imbued with powerful capabilities and repercussion to possible attacks are evaluated. Our analysis proves that authentication is not compromised in the presented model.