A formal security analysis of ZigBee (1.0 and 3.0)

Li Li, Proyash Podder, Endadul Hoque

Research output: Chapter in Book/Entry/PoemConference contribution

1 Scopus citations


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.

Original languageEnglish (US)
Title of host publicationProceedings of the 7th Symposium on Hot Topics in the Science of Security, HotSoS 2020
PublisherAssociation for Computing Machinery
Number of pages11
ISBN (Electronic)9781450375610
StatePublished - Sep 21 2020
Event7th Symposium on Hot Topics in the Science of Security, HotSoS 2020 - Lawrence, Virtual, United States
Duration: Sep 22 2020Sep 24 2020

Publication series

NameACM International Conference Proceeding Series


Conference7th Symposium on Hot Topics in the Science of Security, HotSoS 2020
Country/TerritoryUnited States
CityLawrence, Virtual


  • Protocol verification
  • Symbolic analysis
  • ZigBee

ASJC Scopus subject areas

  • Software
  • Human-Computer Interaction
  • Computer Vision and Pattern Recognition
  • Computer Networks and Communications


Dive into the research topics of 'A formal security analysis of ZigBee (1.0 and 3.0)'. Together they form a unique fingerprint.

Cite this