Formal Verification of IEEE802.16m PKMv3 Protocol Using CasperFDR

Abstract

IEEE 802.16m is the standard representing the security architecture for multi hop relay of broadband wireless access. The security sublayer is provided within IEEE 802.16m MAC layer for privacy and access control, which includes the Privacy and Key Management (PKM) protocol. This paper models the PKMv3 key agreement protocol using CasperFDR and analyzes the output. A few Attacks are found in this version. The specifications through which these attacks are found are presented. © Springer-Verlag Berlin Heidelberg 2010.