A formal analysis of IEEE 802.11w deadlock vulnerabilities

Formal methods can be used to discover obscure denial of service (DoS) vulnerabilities in wireless network protocols. The application of formal methods to the analysis of DoS vulnerabilities in communication protocols is not a mature research area. Although several formal models have been proposed, they lack a clear and convincing demonstration of their usefulness and practicality. This paper bridges the gap between theory and practice, and shows how a simple protocol model can be used to discover protocol deadlock vulnerabilities. A deadlock vulnerability is the most severe form of DoS vulnerabilities, thus checking for deadlock vulnerabilities is an essential part of robust protocol design. We demonstrate the usefulness of the proposed method through the discovery and experimental validation of deadlock vulnerabilities in the published IEEE 802.11w amendment to the 802.11 standard. We present the complete procedure of our approach, from model construction to verification and validation. An Appendix includes the complete model source code, which facilitates the replication and extension of our results. The source code can also be used as a template for modeling other protocols.