Formal Verification for WiMAX Networks Using Enhanced Security Protocols
Article Sidebar
Main Article Content
Abstract
This study discusses the formal verification of the Worldwide Interoperability for Microwave Access (WiMAX) security protocol. WiMAX security specifications are defined as a security property that must be met by the protocol in a WiMAX network. The security properties that must be met include pseudonymity, information confidentiality, anti-tapping and session key secrecy.
Several studies have found several failures to comply with the security properties set by the WiMAX IEEE 802.16-2004 and IEEE 802.16e-2005 standards. Some of the attacks that can occur include jamming, scrambling, DoS attacks, replay attacks, modification of management messages, downgrade attacks, interleaving attacks and other types of security attacks. From some of these attacks there are several solutions to improve security protocols to overcome these attacks so that they can comply with security protocols.
Proof of security protocols in the ability to fulfill security properties can be done either formally or informally. The security protocol operational semantic model framework developed by Cas Cremers and Sjouke Mauw is used to carry out formal verification of proposed improvements to the authentication protocol and Privacy and Key Management (PKM) protocol.
Modeling the proposed protocol with an operational semantic framework has been able to prove the proposed improvement of the authentication protocol and PKM by using timestamps, SS/BS identity encryption and adding digital signatures or message digest values to ensure authentication is able to meet the specified security properties.
Downloads
Article Details
This work is licensed under a Creative Commons Attribution 4.0 International License.
References
IEEE 802.16 and WiMax: Broadband Wireless Access for everyone, Intel White Paper (2014)
IEEE std 802.16e2005: Air interface for fifixed broadband wireless access system amendment: Physical and medium access control layers for combined fifixed and mobile operation in licensed bands, IEEE (2016)
Johnston, D., Walker, J.: Overview of IEEE 802.16 Security. IEEE Security & Privacy (2014)
Mohammad Zabihi , Ramin Shaghaghi, Mohammad Esmail kalantari, “Improving Security Levels of IEEE 802.16e Authentication By Diffie-Hellman Method,” Wirel. Sens. Netw., vol. 02, no. 02, pp. 173–185, 2017, doi: 10.4236/wsn.2010.22023.
Xu, S., Matthews, M., Huang, C.-T.: Security Issues in Privacy and Key Management Protocols of IEEE 802.16. In: Proceedings of the 44th ACM Southeast Conference (ACMSE 2006) (March 2016)
Xu, S., Huang, C.T.: Attacks on PKM protocols of IEEE 802.16 and ts later versions. In: ISWCS 2016: Proceedings of the 3rd International Symposium on Wireless Communication Systems (2016)
Tian, H., Pang, L., Wang, Y.: Key management protocol of the IEEE 802.16e. Wuhan University Journal of Natural Sciences 12, (2017)
Sidharth, S., Sebastian, M.P.: A Revised Secure Authentication Protocol for IEEE 802.16 (e). In: International Conference on Advances in Computer Engineering (2019)
Yuksel, E.: Analysis of the PKMv2 protocol in IEEE 802.16e 2015 using static analysis. Informatics and Mathematical Modelling (2017)
Noudjoud Kahya, Nacira Ghoualmi, Pascal Lafourcade , Roumaissa khelf, “Formal Analysis of Key Management in mobile Wimax” Blaise Pascal University, Aubière, France, 2018.