Symbolic Formal Analysis of Quantum-Resistant Messaging Protocols Based on the Split KEM Mechanism
Katarina Boras, Ante Đerek
Quantum computers, growing only stronger with time, are threatening to break all asymmetric cryptography that is in use today. To mitigate such a devastating scenario, the cryptographic community is putting great effort into developing and evaluating quantum-resistant (post-quantum) primitives and protocols. An important part of the evaluation of such protocols is formal analysis using automated tools such as the Tamarin prover, used to formally prove security properties of a given protocol. Signal is an instant messaging protocol used by millions of people every day. In this paper, we use Tamarin to model and formally verify the security properties of Signal’s session-establishing subprotocol, X3DH, and two proposed post-quantum variants of X3DH, both based on a new notion of the split KEM mechanism. Using our new generic model for X3DH, we are able to construct and directly compare the security levels of the three protocols. We find that the protocols have differing levels of authentication and impersonation resistance; namely, the two proposed post-quantum solutions do not reach the levels of authentication of X3DH in the symbolic model. We discuss the reasons for this and offer solutions to mitigate the issue. We also explore and scrutinize the real-life consequences of these vulnerabilities.
IEEE Access•Jan 1, 2026•0 citations