@MASTERSTHESIS\{IMM2007-05159,
    author       = "E. Yuksel",
    title        = "Analysis of the PKMv2 Protocol in {IEEE} 802.16e-2005 Using Static Analysis",
    year         = "2007",
    school       = "Informatics and Mathematical Modelling, Technical University of Denmark, {DTU}",
    address      = "Richard Petersens Plads, Building 321, {DK-}2800 Kgs. Lyngby",
    type         = "",
    note         = "Supervised by Hanne Riis Nielson, {IMM,} {DTU}",
    url          = "http://www2.compute.dtu.dk/pubdb/pubs/5159-full.html",
    abstract     = "The {IEEE} 802.16e-2005 specification provides an air interface standard for metropolitan area wireless broadband service. {IEEE} 802.16 is the basis for Worldwide Interoperability for Microwave Access (WiMAX) certification which is the next evolution in wireless technology. The latest version of the standard, the {IEEE} 802.16e addresses mobility and also enhances the security sublayer of the {IEEE} 802.16 standard. Since wireless technology is broadcast and transmitted data can be intercepted, wireless users face more risks than wired users. The former {IEEE} 802.16 standards used the Privacy and Key Management (PKM) protocol which had many critical drawbacks. In {IEEE} 802.16e, a new version of this protocol called PKMv2 is released. PKMv2 has radical changes and in contrast with the previous version it seems to have an exaggerated mixture of security features like nonces, message authentication codes, key ids, certificates, etc.

The PKMv2 includes two main issues: an Authentication/Authorization protocol to establish a shared Authorization Key (AK), and a {3-}Way Security Association (SA) Traffic Encryption Key (TEK) Handshake. The former is strengthened with de facto standards such as {RSA} and {EAP,} therefore the PKMv2 {SA-TEK} {3-}Way Handshake (PKMv2 {SA-TEK} {3W} {HS}), which is used for transferring TEKs to mobile stations (MS) after authentication will be the specific point of this thesis.

Static analysis is successfully used for automatically validating security properties of classical and modern cryptographic protocols. In this thesis we will show how the very same technique can be used to validate modern wireless network security protocols, in particular, we study the {IEEE} 802.16e PKMv2 {SA-TEK} {3W} {HS}.

We derived a model of the protocol and described it using LySa, a process calculus in the pi/spi calculus family allowing communication protocols to be specified and annotated for validation of authentication properties. After that, we carried out a static analysis of our LySa model using the static analysis tool LySa-tool. Validating the base protocol, we studied our proposal on an optimized but still secure protocol. Having established systematic experiments on our models of modified versions of the protocol, we analyzed the robustness and security features. In conclusion we found improvements that increased the performance while being still secure."
}