Formal Analysis of SA-TEK 3-Way Handshake Protocols

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.