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

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

    Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

    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.
    Original languageEnglish
    Title of host publicationProceedings of Joint Workshop on Foundations of Computer Security and Automated Reasoning for Security Protocol Analysis
    EditorsPierpaolo Degano, Ralf Kusters, Luca Vigano, Steve Zdancewic
    Publication date2007
    Pages149-164
    Publication statusPublished - 2007
    EventJoint Workshop on Foundations of Computer Security and Automated Reasoning for Security Protocol Analysis - Wrocław, Poland
    Duration: 1 Jan 2007 → …

    Conference

    ConferenceJoint Workshop on Foundations of Computer Security and Automated Reasoning for Security Protocol Analysis
    CityWrocław, Poland
    Period01/01/2007 → …

    Cite this

    Yuksel, E., Nielson, H. R., Nielsen, C. R., & Orencik, M. B. (2007). A Secure Simplification of the PKMv2 Protocol in IEEE 802.16e-2005. In P. Degano, R. Kusters, L. Vigano, & S. Zdancewic (Eds.), Proceedings of Joint Workshop on Foundations of Computer Security and Automated Reasoning for Security Protocol Analysis (pp. 149-164)