Formal Analysis of SA-TEK 3-Way Handshake Protocols

doi:10.1007/s12204-021-2340-2

Abstract

Abstract: 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.

Key words: IEEE 802.16, 3-way handshake, CasperFDR, formal analysis

摘要： IEEE 802.16是无线宽带接入的标准。在IEEE 802.16 MAC层内有一个安全子层，用于隐私保护和访问控制，其中定义了一个隐私和密钥管理（PKM）协议。在IEEE 802.16e新标准中，SA-TEK 3步握手协议被添加到PKM协议里，旨在方便重新认证和密钥分发。本文分析了SA-TEK 3步握手协议，指出了它的缺陷，并提出了一个优化版本。我们还使用了流行的形式化分析工具CasperFDR来验证我们的分析。我们对该协议的各种简化版本进行了建模，以确定协议中相关元素的功能。此外我们还比较了其它形式化工具比如Scyther的分析结果，并纠正了相关工作中的一些错误。非形式化分析和形式化分析的结果都验证了我们改进的协议更加高效可靠，而Casper工具在分析特定安全属性方面也具有一定的优势。

关键词: IEEE 802.16标准，3步握手协议，CasperFDR，形式化分析

CLC Number:

TP309.2

XU Sen* (徐森),YANG Shuo (杨硕)，ZHANG Kefei (张克非). Formal Analysis of SA-TEK 3-Way Handshake Protocols[J]. J Shanghai Jiaotong Univ Sci, 2023, 28(6): 753-762.

References 18

[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.
[1]	IEEE. Air interface for broadband wireless access systems – Amendment 3: Advanced air interface: IEEE Std 802.16m-2011 [S]. New York: IEEE, 2011.
[8]	XU S. Security protocols in WirelessMAN [D]. South Carolina, USA: University of South Carolina, 2008.
[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.
[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.
[3]	HOARE C A R. Communicating sequential processes [J]. Communications of the ACM, 1978, 21(8): 666- 677.
[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.
[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.
[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.
[5]	FDR2 User Manual. Failure-divergence refinement [M]. Oxford: Formal Systems (Europe) Ltd., 2000.
[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.
[6]	LOWE G. Casper A compiler for the analysis of security protocols [J]. Journal of Computer Security, 1998, 6(1/2): 53-84.
[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.
[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.
[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.
[8]	XU S. Security protocols in WirelessMAN [D]. South Carolina, USA: University of South Carolina, 2008.
[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.
[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.
[17]	DOLEV D, YAO A. On the security of public key protocols [J]. IEEE Transactions on Information Theory, 1983, 29(2): 198-208.
[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.
[18]	LOWE G. A hierarchy of authentication specifications [C]//The Tenth IEEE Computer Security Foundations Workshop. Rockport, MA, USA: IEEE, 1997: 31-43.
[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.