X3DH

Audience: This post is intended for security researchers, cryptographers, and engineers with a deep interest in the technical underpinnings of secure messaging protocols. It assumes familiarity with modern cryptographic primitives, end-to-end encryption (E2EE), forward secrecy concepts, post-compromise security, post-quantum cryptography, formal verification tools (like ProVerif and Tamarin), secure software development practices, and related operational considerations (such as reproducible builds and user verification methods). Scope: This analysis reflects the state of the Signal Protocol as of late 2024. It covers foundational concepts such as the Double Ratchet and X3DH, the introduction of PQXDH (Post-Quantum X3DH), formal verification efforts, platform-specific memory-hardening techniques, hardware-backed key management, user verification methods (Safety Numbers), multi-device session handling, ephemeral messages, security boundaries, supply chain security considerations, known implementation pitfalls, and potential future evolutions (including references to MLS). While comprehensive, this post should be supplemented by the latest official specifications, recent academic research, code-level audits, benchmark results, formal verification artifacts, and community analyses. ...