SPIN-Based Verification of Authentication Protocols in WiMAX Networks

The rise in the use of the Internet and other communication technologies like WiMAX which are vulnerable to network attacks has necessitated the implementation of security protocols. Developing secure protocols has proved to be a difficult task as is evident from the presence of flaws in published protocols such as the Needham-Schroeder public key authentication protocol. Security protocols can be validated with formal verification techniques, increasing confidence in their use. The Initial Network Entry procedure in an IEEE 802.16 (WiMAX) network has security defects which can be exploited by the Man-in-the-Middle (MITM) attack, requiring the implementation of a suitable security protocol. In this paper, we analyse a modification of the Diffie-Hellman (DH) key exchange protocol proposed to mitigate this MITM attack and model the protocol and an intruder process with MITM capabilities in PROMELA formalism. We then use Linear Temporal Logic (LTL) to define the attributes the protocol should satisfy and carry out verification by use of the Simple PROMELA INterpreter (SPIN) model checker.