A Formal Security Analysis of Zigbee
pdf
| The rapid increase in the number of IoT devices in recent years indi-cates how much financial investment and efforts the tech-industries and the device manufacturers have put in. Unfortunately, this ag-gressive competition can give rise to poor quality IoT devices that are prone to adversarial attacks. To make matter worse, these at-tacks 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. Consid-ering 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 secu-rity 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.
Li Li is a graduate student in the Department of Electrical Engineering and Computer Science at Syracuse University. His research interests span over computer and IoT systems security, network security, and privacy-preserving protocols.
Tags:
License: CC-2.5
Submitted by Anonymous
on