Formal Analysis of SA-TEK 3-Way Handshake Protocols  

作　　者：徐森 杨硕 张克非 XU Sen;YANG Shuo;ZHANG Kefei(College of Computer Science and Technology,Shenyang University of Chemical Technology,Shenyang 110142,China)

机构地区：[1]College of Computer Science and Technology,Shenyang University of Chemical Technology,Shenyang 110142,China

出　　处：《Journal of Shanghai Jiaotong university(Science)》2023年第6期753-762,共10页上海交通大学学报（英文版）

基　　金：the Startup Research Fund for the Doctoral Faculty of Shenyang University of Chemical Technology(No.51045084)。

摘　　要：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 re-authentication 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.

关 键 词：IEEE 802.16 3-way handshake CasperFDR formal analysis 

分 类 号：TP309.2[自动化与计算机技术—计算机系统结构]