Formal security analysis and improvement based on the ZLL touchlink commissioning protocol
摘要
The ZLL Touchlink Commissioning protocol is a widely used smart light control protocol designed for rapid pairing and network configuration of lighting systems. It is especially useful for small and medium-sized smart lighting systems that are part of the Internet of Things (IoT). Due to inherent vulnerabilities and the lack of confidentiality and integrity guarantees in the open transmission channels, this protocol is vulnerable to attacks by adversaries. Motivated from these, this paper analyses the ZLL Touchlink Commissioning protocol using formal modeling based on the colored Petri net (CPN) theory and the Dolev-Yao attacker theory. The analysis reveals that this protocol is susceptible to various attacks, including replay attack, eavesdropping, tampering, and key compromise impersonation attack (KCIA). To address the aforementioned security concerns, this paper leverages physically unclonable function and a registration authority to strengthen the protocol’s security and proposes a key update scheme that synchronously updates the session and network keys. Ultimately, through a formal analysis of the proposed scheme, it is demonstrated that this scheme can achieve authentication and device anonymity, while effectively resisting replay attack, eavesdropping, tampering, and KCIA. In comparison to existing protocols, the proposed scheme significantly enhances security features while maintaining low computation and communication costs.