A Secure Simplification of the PKMv2 Protocol in IEEE 802.16e-2005

Ender Yuksel, Hanne Riis Nielsen, Christoffer Rosenkilde Nielson, Mehmet Bulent Orencik

AbstractStatic 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.
TypeConference paper [Submitted]
ConferenceProceedings of Joint Workshop on Foundations of Computer Security and Automated Reasoning for Security Protocol Analysis
EditorsDegano, Pierpaolo and Kusters, Ralf and Vigano, Luca and Zdancewic, Steve
Year2007    pp. 149-164
Electronic version(s)[pdf]
BibTeX data [bibtex]
IMM Group(s)Computer Science & Engineering