Migrating to Hybrid Cryptography in Practice: The TutaCrypt Protocol and Its Security

In this work, we study the hybrid key establishment protocol TutaCrypt as a concrete case of post-quantum cryptographic migration in practice. The protocol was developed by the end-to-end encrypted email provider Tuta and has been deployed to more than ten million users worldwide. We present the protocol in a form that enables rigorous cryptographic analysis and define two Bellare–Rogaway-style security models that precisely characterize the provided security guarantees. The two models capture that the security properties achieved in the pre-quantum setting are slightly stronger than in the post-quantum setting. We then give reduction-based security proofs that clarify under which assumptions the construction achieves security, and how its guarantees degrade if either the classical or the post-quantum component is compromised. Our results illustrate how formally grounded cryptographic models can capture real-world migration strategies and hybrid deployments. Such analyses help to understand the security properties of deployed cryptographic systems and help move cryptographic migration from best practice toward principled, verifiable design.