IEEE 802.16 is the standard for broadband wireless access. The security sublayer is provided within IEEE 802.16 MAC layer for privacy and access control, in which the privacy and key management (PKM) protocols are specified. In IEEE 802.16e, SA-TEK 3-way handshake is added into PKM protocols, aiming to facilitate reauthentication and key distribution. This paper analyzes the SA-TEK 3-way handshake protocol, and proposes an optimized version. We also use CasperFDR, a popular formal analysis tool, to verify our analysis. Moreover, we model various simplified versions to find the functions of those elements in the protocol, and correct some misunderstandings in related works using other formal analysis tools.
XU Sen* (徐森),YANG Shuo (杨硕)，ZHANG Kefei (张克非)
. Formal Analysis of SA-TEK 3-Way Handshake Protocols[J]. Journal of Shanghai Jiaotong University(Science), 2023
, 28(6)
: 753
-762
.
DOI: 10.1007/s12204-021-2340-2
[1] IEEE. Air interface for broadband wireless access systems – Amendment 3: Advanced air interface: IEEE Std 802.16m-2011 [S]. New York: IEEE, 2011.
[2] IEEE. Air interface for fixed and mobile broadband wireless access systems – Amendment 2: Physical and medium access control layers for combined fixed and mobile operation in licensed bands: IEEE Std 802.16e- 2005 [S]. New York: IEEE, 2006.
[3] HOARE C A R. Communicating sequential processes [J]. Communications of the ACM, 1978, 21(8): 666- 677.
[4] ROSCOE A W. Modelling and verifying key-exchange protocols using CSP and FDR [C]//The Eighth IEEE Computer Security Foundations Workshop. County Kerry, Ireland: IEEE, 1995: 98-107.
[5] FDR2 User Manual. Failure-divergence refinement [M]. Oxford: Formal Systems (Europe) Ltd., 2000.
[6] LOWE G. Casper A compiler for the analysis of security protocols [J]. Journal of Computer Security, 1998, 6(1/2): 53-84.
[7] XU S, HUANG C T, MATTHEWS M M. Modeling and analysis of IEEE 802.16 PKM protocols using CasperFDR [C]//IEEE International Symposium on Wireless Communication Systems. Reykjavik, Iceland: IEEE, 2008: 653-657.
[8] XU S. Security protocols in WirelessMAN [D]. South Carolina, USA: University of South Carolina, 2008.
[9] ZHU X, XU Y, LI X, et al. Formal analysis of the PKMv3 protocol [J]. Mobile Networks and Applications, 2018, 23(1): 44-56.
[10] JIANG J, MAO H, SHAO R, et al. Formal verification and improvement of the PKMv3 protocol using CSP [C]//2018 IEEE 42nd Annual Computer Software and Applications Conference (COMPSAC). Tokyo, Japan: IEEE, 2018: 682-687.
[11] LAL N, KUMAR S. An efficient uplink scheduler for WiMAX communication system with prevention from security attacks [J]. New Review of Information Networking, 2019, 24(2): 133-152.
[12] PANDA P K, CHATTOPADHYAY S. A modified PKM environment for the security enhancement of IEEE 802.16e [J]. Computer Standards & Interfaces, 2019, 61: 107-120.
[13] RAJU K V K, KUMARI V V, VARMA N S, et al. Formal verification of IEEE802.16m PKMv3 protocol using CasperFDR [M]//Information and communication technologies. Berlin, Heidelberg: Springer, 2010: 590-595.
[14] YUKSEL E, NIELSON H R, NIELSEN C R, et al. A secure simplification of the PKMv2 protocol in IEEE 802.16e-2005 [C]//Joint Workshop on Foundations of Computer Security and Automated Reasoning for Security Protocol Analysis (FCS-ARSPA’07). Wroclaw, Poland: Local Organization, 2007: 149-164.
[15] CHAUHAN V, INGUVA S. IEEE 802.16e 3-way handshake [EB/OL]. (2006-03-26). http://seclab.stanford.edu/pcl/cs259/WWW06/ projects/project09.
[16] XU S, MATTHEWS M, HUANG C T. Security issues in privacy and key management protocols of IEEE 802.16 [C]//Proceedings of the 44th Annual Southeast Regional Conference. Melbourne, FL, USA: ACM Press, 2006: 113-118.
[17] DOLEV D, YAO A. On the security of public key protocols [J]. IEEE Transactions on Information Theory, 1983, 29(2): 198-208.
[18] LOWE G. A hierarchy of authentication specifications [C]//The Tenth IEEE Computer Security Foundations Workshop. Rockport, MA, USA: IEEE, 1997: 31-43.
