Formal Verification of PKMv3 Protocol Using ProVerif

IEEE Std 802.16m-2011 is the official name of the IEEE standard describing the advanced air interface for WiMAX 2. At the security sublayer, the Privacy Key Management version 3 (PKMv3) protocol defines the procedures for authentication and key exchange to secure the communication between the base station and the mobile station. PKMv3, introduced as an upgrade to PKMv1 and PKMv2, aims to address the security issues identified in previous versions. Few studies analyzed this protocol in detail. Some reports claimed that PKMv3 is vulnerable, even though no new version of the protocol has been released since the publication of this standard. The main goal of this paper is to evaluate these claims by creating a complete model of PKMv3 using ProVerif, a powerful pi calculus-based tool for the automatic verification of security protocols. Our model incorporates the EAP-TLS 1.3 protocol and the TEK-Invalid message exchange. We test the protocol against a set of security properties, and the result is compared with related work. The analysis shows that, under the perfect cryptography assumption, a faithful formal representation of the protocol ensures security properties, and that several previously reported vulnerabilities stem from inaccurate modeling rather than from flaws in the protocol itself.