A Modular Correctness Proof of IEEE 802.11i and SSL/TLS
When networks are required to have mutual authentication between network access point and user devices, the IEEE 802.11i wireless networking protocol is often put to use. This authentication is usually provided before user connectivity and it comprises several parts such as an 802.1X authentication phase, allowing TLS over EAP, the 4-Way Handshake to establish a fresh session key, and an optional Group Key Handshake for group communications. This paper also delves on the SSL/TLS, which is used extensively apart from 802.11i. The use of SSL/TLS is more so because security continues to remain a primary concern when it comes to wireless networks, more so because intruders are often able to potentially access a network without physically entering the buildings where the network has been deployed. The paper also discusses the Wired Equivalent Privacy (WEP) protocol that lacks good key management. Although the WEP protocol has been provided to offer security, a number of cryptographic have been witnessed with the protocol. The IEEE 802.11i wireless networking protocol was a result of an understanding of the previous vulnerabilities that were witnessed in related wireless protocols. This paper extensively refers to the changes in 802.11i to offer better security so that users are able to carry out a formal proof of correctness using a Protocol Composition Logic. This proof discussed in the paper is modular and comes with a separate proof for each protocol section.