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.
Tuta
All GNU social JP content and data are available under the