@CONFERENCE\{IMM2007-05637,
    author       = "E. Yuksel and H. R. Nielsen and C. R. Nielson and M. B. Orencik",
    title        = "A Secure Simplification of the PKMv2 Protocol in {IEEE} 802.16e-2005",
    year         = "2007",
    pages        = "149-164",
    booktitle    = "Proceedings of Joint Workshop on Foundations of Computer Security and Automated Reasoning for Security Protocol Analysis",
    volume       = "",
    series       = "",
    editor       = "Degano, Pierpaolo and Kusters, Ralf and Vigano, Luca and Zdancewic, Steve",
    publisher    = "",
    organization = "",
    address      = "",
    url          = "http://www2.compute.dtu.dk/pubdb/pubs/5637-full.html",
    abstract     = "Static analysis is successfully used for automatically validating
security properties of classical cryptographic protocols. In this paper,
we shall employ the same technique to a modern security protocol
for wireless networks, namely the latest version of the Privacy and Key
Management protocol for {IEEE} 802.16e, PKMv2. This protocol seems
to have an exaggerated mixture of security features. Thus, we iteratively
investigate which components are necessary for upholding the security
properties and which can be omitted safely. This approach is based on
the LySa process calculus and employs the corresponding automated
analysis tool, the LySaTool."
}