Show simple item record

dc.contributor.advisorMjølsnes, Stig Frodenb_NO
dc.contributor.advisorAndresen, Steinar Hidlenb_NO
dc.contributor.authorEian, Martinnb_NO
dc.date.accessioned2014-12-19T14:14:54Z
dc.date.available2014-12-19T14:14:54Z
dc.date.created2012-09-23nb_NO
dc.date.issued2012nb_NO
dc.identifier555989nb_NO
dc.identifier.isbn978-82-471-3763-5nb_NO
dc.identifier.isbn978-82-471-3762-8nb_NO
dc.identifier.urihttp://hdl.handle.net/11250/262618
dc.description.abstractWireless network access protocols are used in numerous safety critical applications. Network availability is essential for safety critical applications,since loss of availability can cause personal or material damage. An adversary can disrupt the availability of a wireless network using denial of service (DoS) attacks. The most widely used wireless protocols are vulnerable to DoS attacks. Researchers have published DoS attacks against IEEE 802.11 local area networks (LANs), IEEE 802.16 wide area networks (WANs) and GSM andUMTS mobile networks. In this work, we analyze DoS vulnerabilities in wireless network protocols and define four categories of attacks:  jamming attacks, flooding attacks, semantic attacks and implementation specific attacks. We identify semantic attacks as the most severe threat to current andfuture wireless protocols, and as the category that has received the least attention by researchers. During the first phase of the research project we discover semantic DoS vulnerabilities in the IEEE 802.11 communication protocols through manual analysis. The 802.11 standard has been subject to manual analysis of DoS vulnerabilities for more than a decade, thus our results indicate that protocol vulnerabilities can elude manual analysis. We conclude that formal methods are required in order to improve protocol robustness against semantic DoS attacks.We propose a formal method that can be used to automatically discover protocol vulnerabilities. The formal method defines a protocol model, adversary model and cost model. The protocol participants and adversary are modeled as finite state transducers, while the cost is modeled as a function of time. Our primary goal is to construct a formal method that is practical, i.e. does not require a vast amount of resources to implement, and useful, i.e. able to discover protocol vulnerabilities. We verify and validate our proposed method by modeling the 802.11w amendment to the 802.11 standard using Promela as the modeling language. We then use the SPIN model checker to verify the model properties and experiments to validate the results. The modeling and experiments result in the discovery and experimental validation of four new deadlock vulnerabilities that had eluded manual analysis. We find one deadlock vulnerability in 802.11i and three deadlock vulnerabilitiesin 802.11w. A deadlock vulnerability is the most severe form of communication protocol DoS vulnerabilities, and their discovery and removal are an essential part of robust protocol design. Thus, we conclude that our proposed formal method is both practical and useful.nb_NO
dc.languageengnb_NO
dc.publisherNTNUnb_NO
dc.relation.ispartofseriesDoctoral Theses at NTNU, 1503-8181; 2012:230nb_NO
dc.relation.haspartEian, Martin. Fragility of the Robust Security Network. APPLIED CRYPTOGRAPHY AND NETWORK SECURITY: 400-416, 2009. <a href='http://dx.doi.org/10.1007/978-3-642-01957-9_25'>10.1007/978-3-642-01957-9_25</a>.nb_NO
dc.relation.haspartEian, Martin. A Practical Cryptographic Denial of Service Attack against 802.11i TKIP and CCMP. CRYPTOLOGY AND NETWORK SECURITY: 62-75, 2010. <a href='http://dx.doi.org/10.1007/978-3-642-17619-7_6'>10.1007/978-3-642-17619-7_6</a>.nb_NO
dc.relation.haspartEian, Martin; Mjølsnes, Stig F.. The modeling and comparison of wireless network denial of service attacks. Proceedings of the 3rd ACM SOSP Workshop on Networking, Systems, and Applications on Mobile Handhelds: 1-6, 2011. <a href='http://dx.doi.org/10.1145/2043106.2043113'>10.1145/2043106.2043113</a>.nb_NO
dc.relation.haspartEian, Martin; Mjølsnes, Stig F.. A Formal Analysis of IEEE 802.11w Deadlock Vulnerabilities. Proceedings of the 31st Annual IEEE International Conference on Computer Communications: 918-926, 2012. <a href='http://dx.doi.org/10.1109/INFCOM.2012.6195841'>10.1109/INFCOM.2012.6195841</a>.nb_NO
dc.subjectWireless Network Securityen_GB
dc.subjectAvailabilityen_GB
dc.subjectDenial of Serviceen_GB
dc.subjectFormal Methodsen_GB
dc.subject802.11en_GB
dc.subject802.11ien_GB
dc.subject802.11wen_GB
dc.titleRobustness in Wireless Network Access Protocolsnb_NO
dc.typeDoctoral thesisnb_NO
dc.source.pagenumber109nb_NO
dc.contributor.departmentNorges teknisk-naturvitenskapelige universitet, Fakultet for informasjonsteknologi, matematikk og elektroteknikk, Institutt for telematikknb_NO
dc.description.degreePhD i telematikknb_NO
dc.description.degreePhD in Telematicsen_GB


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record