Qualitative and Quantitative Security Analyses for ZigBee Wireless Sensor Networks

Wireless sensor networking is a challenging and emerging technology that will soon become an inevitable part of our modern society. Today wireless sensor networks are broadly used in industrial and civilian application areas including environmental monitoring, surveillance tasks, healthcare applications, home automation, and traffic control. The challenges for research in this area are due to the unique features of wireless sensor devices such as low processing power and associated low energy. On top of this, wireless sensor networks need secure communication as they operate in open fields or unprotected environments and communicate on broadcasting technology. As a result, such systems have to meet a multitude of quantitative constraints (e.g. timing, power consumption, memory usage, communication bandwidth) as well as security requirements (e.g. authenticity, confidentiality, integrity). One of the main challenges arise in dealing with the security needs of such systems where it is less likely that absolute security guarantees can be sustained - because of the need to balance security against energy consumption in wireless sensor network standards like ZigBee. This dissertation builds on existing methods and techniques in different areas and brings them together to create an efficient verification system. The overall ambition is to provide a wide range of powerful techniques for analyzing models with quantitative and qualitative security information. We stated a new approach that first verifies low level security protocol s in a qualitative manner and guarantees absolute security, and then takes these verified protocols as actions of scenarios to be verified in a quantitative manner. Working on the emerging ZigBee wireless sensor networks, we used probabilistic verification that can return probabilistic results with respect to the trade-off between security and performance. In this sense, we have extended various existing ideas and also proposed new ideas to improve verification. Especially in the problem of key update, we believe we have contributed to the solution for not only wireless sensor networks but also many other types of systems that require key updates. Besides we produced automated tools that were intended to demonstrate what kind of tools can developed on different purposes and application domains.