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.
|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 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||Joint Workshop on Foundations of Computer Security and Automated Reasoning for Security Protocol Analysis|
|Period||01/01/2007 → …|