Formal Verification of Initial Network Entry in WiMAX Networks
The Initial Network Entry procedure is the first stage in establishing a connection in an IEEE 802.16 (WiMAX) network. The process involves the transmission of unencrypted management messages, which constitutes a major security flaw. The Man-In-The-Middle (MITM) attack exploits this weakness in the network by eavesdropping, interception and fabrication of the management messages, resulting in a breach in the reliability of the entire network. In this paper, the authors analyze a modification of the Diffie-Hellman key exchange protocol proposed to mitigate the man-in-the-middle attack in WiMAX by modelling the protocol in Promela.