TY - GEN
T1 - Formalization and Verification of XMPP Communication Mechanism Using CSP
AU - Wu, Di
AU - Dong, Wenting
AU - Zhu, Huibiao
N1 - Publisher Copyright:
© 2025 Knowledge Systems Institute Graduate School. All rights reserved.
PY - 2025
Y1 - 2025
N2 - XMPP is an open-standard communication protocol, offering services including near-real-time messaging, presence information and request-response. Owing to its exceptional openness, flexibility and scalability, it has been extensively adopted in cloud computing and the Internet of Things (IoT). Consequently, ensuring the reliability and security of the XMPP protocol is of great importance. In this paper, we employ process algebra CSP (Communicating Sequential Processes) to model the communication mechanism of the XMPP system. Additionally, the model checking tool PAT (Process Analysis Toolkit) is utilized to verify six critical properties: deadlock freedom, client faking, server faking, data reachability, key leakage and data leakage. The verification results demonstrate that the XMPP communication mechanism guarantees reliability and security.
AB - XMPP is an open-standard communication protocol, offering services including near-real-time messaging, presence information and request-response. Owing to its exceptional openness, flexibility and scalability, it has been extensively adopted in cloud computing and the Internet of Things (IoT). Consequently, ensuring the reliability and security of the XMPP protocol is of great importance. In this paper, we employ process algebra CSP (Communicating Sequential Processes) to model the communication mechanism of the XMPP system. Additionally, the model checking tool PAT (Process Analysis Toolkit) is utilized to verify six critical properties: deadlock freedom, client faking, server faking, data reachability, key leakage and data leakage. The verification results demonstrate that the XMPP communication mechanism guarantees reliability and security.
KW - CSP
KW - Instant Messaging
KW - PAT
KW - Verification
KW - XMPP
UR - https://www.scopus.com/pages/publications/105018737693
U2 - 10.18293/SEKE2025-092
DO - 10.18293/SEKE2025-092
M3 - 会议稿件
AN - SCOPUS:105018737693
T3 - Proceedings of the International Conference on Software Engineering and Knowledge Engineering, SEKE
SP - 153
EP - 158
BT - Proceedings - SEKE 2025
PB - Knowledge Systems Institute Graduate School
T2 - 37th International Conference on Software Engineering and Knowledge Engineering, SEKE 2025
Y2 - 29 September 2025 through 4 October 2025
ER -