Formal Analysis and Verification of XMPP with Crash-Stop Failures

The Extensible Messaging and Presence Protocol (XMPP) is an open-standard instant messaging protocol. Owing to its openness, flexibility, and extensibility, it demonstrates broad application prospects in the Internet of Things (IoT). However, dynamic and insecure network environments increase the uncertainty of interactions, posing significant challenges to the reliability and security of the protocol. In this paper, we utilize Multiparty Session Types (MPST) to formally model the core communication mechanisms of XMPP and its Publish-Subscribe (PubSub) extension under crash scenarios. Furthermore, to rigorously verify the security of the model, an intruder model is introduced to simulate potential threats. Then, the model checking tool mpstk is employed to verify the properties of the model, including safety, deadlock-freedom, liveness, liveness⁺, and liveness⁺⁺. The verification results demonstrate that the model satisfies all these properties, effectively validating its reliability and security within complex environments.