A formal security analysis of ZigBee (1.0 and 3.0)

The rapid increase in the number of IoT devices in recent years indicates how much financial investment and efforts the tech-industries and the device manufacturers have put in. Unfortunately, this aggressive competition can give rise to poor quality IoT devices that are prone to adversarial attacks. To make matter worse, these attacks can compromise not only security but also safety, since an IoT device can directly operate on the physical world. Many recently reported attacks are due to the insecurity present in the underlying communication protocol stacks, and ZigBee is one of them. Considering the emergence and adoption of ZigBee 3.0 and the current market share of ZigBee 1.0, it is essential to study and analyze these protocol stacks at their specification level so that any insecurity at the specification level should be identified and fixed before they go into production. With that goal in mind, in this paper, we develop a model for ZigBee (1.0 and 3.0) and reason about its security properties using a security protocol verification tool (named Tamarin). Our model of ZigBee closely follows the ZigBee specification, and the security properties are derived from the ZigBee specification. We use Tamarin to verify these properties on our model and report our findings on ZigBee 1.0 and ZigBee 3.0.