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

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

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

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

Istanbul Technical University

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-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 language	English
Title of host publication	Proceedings of Joint Workshop on Foundations of Computer Security and Automated Reasoning for Security Protocol Analysis
Editors	Pierpaolo Degano, Ralf Kusters, Luca Vigano, Steve Zdancewic
Publication date	2007
Pages	149-164
Publication status	Published - 2007
Event	Joint Workshop on Foundations of Computer Security and Automated Reasoning for Security Protocol Analysis - Wrocław, Poland Duration: 1 Jan 2007 → …

Conference

Conference	Joint Workshop on Foundations of Computer Security and Automated Reasoning for Security Protocol Analysis
City	Wrocław, Poland
Period	01/01/2007 → …

OpenUrl availability

Full text

Cite this

@inproceedings{980aa876e2274d68b4bc5bdaf86cebc3,

title = "A Secure Simplification of the PKMv2 Protocol in IEEE 802.16e-2005",

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.",

author = "Ender Yuksel and Nielson, {Hanne Riis} and Nielsen, {Christoffer Rosenkilde} and Orencik, {Mehmet Bulent}",

year = "2007",

language = "English",

pages = "149--164",

editor = "Pierpaolo Degano and Ralf Kusters and Luca Vigano and Steve Zdancewic",

booktitle = "Proceedings of Joint Workshop on Foundations of Computer Security and Automated Reasoning for Security Protocol Analysis",

note = "Joint Workshop on Foundations of Computer Security and Automated Reasoning for Security Protocol Analysis, FCS-ARSPA '07 ; Conference date: 01-01-2007",

}

Yuksel, E, Nielson, HR, Nielsen, CR & Orencik, MB 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, Joint Workshop on Foundations of Computer Security and Automated Reasoning for Security Protocol Analysis, Wrocław, Poland, 01/01/2007.

A Secure Simplification of the PKMv2 Protocol in IEEE 802.16e-2005. / Yuksel, Ender; Nielson, Hanne Riis; Nielsen, Christoffer Rosenkilde et al.
Proceedings of Joint Workshop on Foundations of Computer Security and Automated Reasoning for Security Protocol Analysis. ed. / Pierpaolo Degano; Ralf Kusters; Luca Vigano; Steve Zdancewic. 2007. p. 149-164.

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review

TY - GEN

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

AU - Yuksel, Ender

AU - Nielson, Hanne Riis

AU - Nielsen, Christoffer Rosenkilde

AU - Orencik, Mehmet Bulent

PY - 2007

Y1 - 2007

N2 - 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.

AB - 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.

M3 - Article in proceedings

SP - 149

EP - 164

BT - Proceedings of Joint Workshop on Foundations of Computer Security and Automated Reasoning for Security Protocol Analysis

A2 - Degano, Pierpaolo

A2 - Kusters, Ralf

A2 - Vigano, Luca

A2 - Zdancewic, Steve

T2 - Joint Workshop on Foundations of Computer Security and Automated Reasoning for Security Protocol Analysis

Y2 - 1 January 2007

ER -

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

Abstract

Conference

OpenUrl availability

Fingerprint

Cite this