Paper 2026/2787

Symbolic forward secrecy analysis of ML-KEM

Abstract

Post-quantum Key Encapsulation Mechanisms (KEMs) rely on generic transformations to achieve active security. Specifically, ML-KEM (FIPS 203) applies the Fujisaki--Okamoto (FO) transform to a lattice-based public-key encryption scheme, Kyber.CPAPKE, to construct an IND-CCA2 secure key exchange protocol, ML-KEM. While NIST standards and associated special publications discuss guidelines for establishing larger shared keying material using ML-KEM, formal symbolic proofs to evaluate these operational setups remain sparse. This work addresses this gap by conducting a formal symbolic analysis of ML-KEM using \textsf{ProVerif}. First, we verify the core primitive, establishing symbolic proofs for session key confidentiality, key agreement soundness, and Fujisaki--Okamoto implicit rejection fallback secrecy. Second, we examine the temporal security guarantees of ML-KEM under long-term static key leakage. Using \textsf{ProVerif}'s global phase constructs, we demonstrate that standalone static ML-KEM does not preserve Perfect Forward Secrecy (PFS), rendering repeated static encapsulation for additional key share establishment vulnerable to retroactive decapsulation. Lastly, we formally model and verify that deploying ML-KEM with ephemeral key rotation or ratcheting mechanisms mitigates this vulnerability, providing robust forward secrecy and complete session domain separation.