Modern instant messaging systems require end-to-end (E2E) security guarantees while operating over server-mediated infrastructures that cannot be fully trusted. At the same time, the impending transition to post-quantum cryptography raises nontrivial challenges for the design of secure messaging protocols that preserve these guarantees. In this work, we present the design of a post-quantum end-to-end secure protocol for instant messaging applications under an untrusted relay model. The proposed construction relies on lattice-based primitives standardized by NIST, namely ML-KEM for key establishment and ML-DSA for authentication, and follows a Double-KEM pattern combined with explicit context binding to derive an E2E session key known only to the communicating clients. The server acts solely as an authenticated relay and never gains access to plaintext messages or session keys. In addition to the protocol design, we complement the protocol description with an automated symbolic verification using ProVerif, establishing injective mutual authentication and session-key secrecy under a Dolev–Yao adversary model. Finally, we characterize the computational cost of different authentication and verification policies and evaluate the performance of the handshake on heterogeneous cloud-based architectures. The results provide practical insight into the feasibility of deploying post-quantum end-to-end secure protocols within existing instant messaging infrastructures.
Abiega-L’Eglisse et al. (Thu,) studied this question.