Automatic vulnerability checking of IEEE 802.16 WiMAX protocols through TLA+

Prasad Narayana*, Ruiming Chen, Yao Zhao, Yan Chen, Zhi Fu, Hai Zhou

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contribution

14 Scopus citations

Abstract

Vulnerability analysis is indispensably the first step towards securing a network protocol, but currently remains mostly a best effort manual process with no completeness guarantee. Formal methods are proposed for vulnerability analysis and most existing work focus on security properties such as perfect forwarding secrecy and correctness of authentication. However, it remains unclear how to apply these methods to analyze more subtle vulnerabilities such as denial-of-service (DoS) attacks. To address this challenge, in this paper, we propose use of TLA+ to automatically check DoS vulnerability of network protocols with completeness guarantee. In particular, we develop new schemes to avoid state space explosion in property checking and to model attackers' capabilities for finding realistic attacks. As a case study, we successfully identify threats to IEEE 802.16 air interface protocols.

Original languageEnglish (US)
Title of host publication2nd Workshop on Secure Network Protocols, NPSec
Pages44-49
Number of pages6
DOIs
StatePublished - 2006
Event2006 2nd Workshop on Secure Network Protocols, NPSec - Santa Barbara, CA, United States
Duration: Nov 12 2006Nov 12 2006

Publication series

Name2nd Workshop on Secure Network Protocols, NPSec

Other

Other2006 2nd Workshop on Secure Network Protocols, NPSec
CountryUnited States
CitySanta Barbara, CA
Period11/12/0611/12/06

ASJC Scopus subject areas

  • Computer Networks and Communications

Fingerprint Dive into the research topics of 'Automatic vulnerability checking of IEEE 802.16 WiMAX protocols through TLA+'. Together they form a unique fingerprint.

  • Cite this

    Narayana, P., Chen, R., Zhao, Y., Chen, Y., Fu, Z., & Zhou, H. (2006). Automatic vulnerability checking of IEEE 802.16 WiMAX protocols through TLA+. In 2nd Workshop on Secure Network Protocols, NPSec (pp. 44-49). [4110436] (2nd Workshop on Secure Network Protocols, NPSec). https://doi.org/10.1109/NPSEC.2006.320346