Analysing ZigBee Key Establishment Protocols
This work addresses security vulnerabilities in wireless sensor network protocols, which is critical for IoT applications, though it appears incremental as it applies existing analysis techniques to a specific protocol.
The researchers analyzed the ZigBee-2007 End-to-End Application Key Establishment Protocol using LySa process calculus and control flow analysis, discovering an unknown flaw and proposing a verified fix.
In this report, we present our approach for protocol analysis together with a real example where we find an important flow in a contemporary wireless sensor network security protocol. We start by modelling protocols using a specific process algebraic formalism called LySa process calculus. We then apply an analysis based on a special program analysis technique called control flow analysis. We apply this technique to the ZigBee-2007 End-to-End Application Key Establishment Protocol and with the help of the analysis discover an unknown flaw. Finally we suggest a fix for the protocol, and verify that the fix works by using the same technique.