TY - GEN
T1 - Formalization and Verification of MQTT-SN Communication Using CSP
AU - Lin, Wei
AU - Chen, Sini
AU - Zhu, Huibiao
N1 - Publisher Copyright:
© 2024, The Author(s), under exclusive license to Springer Nature Switzerland AG.
PY - 2024
Y1 - 2024
N2 - The MQTT-SN protocol is a lightweight version of the MQTT protocol and is customized for Wireless Sensor Networks (WSN). It removes the need for the underlying protocol to provide ordered and reliable connections during transmission, making it ideal for sensors in WSN with extremely limited computing power and resources. Due to the widespread use of WSN in various areas, the MQTT-SN protocol has promising application prospects. Furthermore, security is crucial for MQTT-SN, as sensor nodes applying this protocol are often deployed in uncontrolled wireless environments and are vulnerable to a variety of external security threats. To ensure the security of the MQTT-SN protocol without compromising its simplicity, we introduce the ChaCha20-Poly1305 cryptographic authentication algorithm. In this paper, we formally model the MQTT-SN communication system using Communicating Sequential Process (CSP) and then verify seven properties of this model using Process Analysis Toolkit (PAT), including deadlock freedom, divergence freedom, data reachability, client security, gateway security, broker security, and data leakage. According to the verification results in PAT, our model satisfies all the properties above. Therefore, we can conclude that the MQTT-SN protocol is secure with the introduction of ChaCha20-Poly1305.
AB - The MQTT-SN protocol is a lightweight version of the MQTT protocol and is customized for Wireless Sensor Networks (WSN). It removes the need for the underlying protocol to provide ordered and reliable connections during transmission, making it ideal for sensors in WSN with extremely limited computing power and resources. Due to the widespread use of WSN in various areas, the MQTT-SN protocol has promising application prospects. Furthermore, security is crucial for MQTT-SN, as sensor nodes applying this protocol are often deployed in uncontrolled wireless environments and are vulnerable to a variety of external security threats. To ensure the security of the MQTT-SN protocol without compromising its simplicity, we introduce the ChaCha20-Poly1305 cryptographic authentication algorithm. In this paper, we formally model the MQTT-SN communication system using Communicating Sequential Process (CSP) and then verify seven properties of this model using Process Analysis Toolkit (PAT), including deadlock freedom, divergence freedom, data reachability, client security, gateway security, broker security, and data leakage. According to the verification results in PAT, our model satisfies all the properties above. Therefore, we can conclude that the MQTT-SN protocol is secure with the introduction of ChaCha20-Poly1305.
KW - Communicating Sequential Process (CSP)
KW - Formal Methods
KW - MQTT-SN Protocol
KW - Modeling
KW - Verification
UR - https://www.scopus.com/pages/publications/85180156776
U2 - 10.1007/978-3-031-49252-5_10
DO - 10.1007/978-3-031-49252-5_10
M3 - 会议稿件
AN - SCOPUS:85180156776
SN - 9783031492518
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 115
EP - 132
BT - Engineering of Computer-Based Systems - 8th International Conference, ECBS 2023, Proceedings
A2 - Kofroň, Jan
A2 - Margaria, Tiziana
A2 - Seceleanu, Cristina
PB - Springer Science and Business Media Deutschland GmbH
T2 - 8th International Conference on Engineering of Computer-Based Systems, ECBS 2023
Y2 - 16 October 2023 through 18 October 2023
ER -