ML-KEM decapsulation failure and IND-CCA security

Short answer: ML-KEM's underlying encryption scheme has a small, non-zero decryption failure probability, and the key encapsulation step built on top of it is a related but separate quantity. A 2024 paper reports a machine-checked EasyCrypt proof of ML-KEM's correctness, including the decryption failure probability, and of its IND-CCA security. The proof also covers two Jasmin implementations that the authors say are constant-time and functionally equivalent to the specification. This is a formal-methods result about the specification and these implementations, not about every product.

What the proof covers

The 2024 paper presents what it calls a formally verified proof of the correctness and IND-CCA security of ML-KEM, the Kyber-based key encapsulation mechanism. The proof is machine-checked in EasyCrypt and has four parts. The authors formalise the correctness, meaning the decryption failure probability, and the IND-CPA security of the Kyber base public-key encryption scheme, following earlier work by Bos and others at Euro S&P 2018. They formalise the relevant variant of the Fujisaki-Okamoto transform in the random oracle model, following closely but not exactly Hofheinz, Hovelmanns and Kiltz at TCC 2017. They then prove that the IND-CCA security of the ML-KEM specification and its correctness as a KEM follow from the earlier results. Finally, they present two formally verified implementations of ML-KEM written in Jasmin, which they say are provably constant-time, functionally equivalent to the specification and, for that reason, inherit the provable security guarantees from the earlier points.

Decryption failure versus decapsulation failure

A crypto.stackexchange answer, which is community commentary and not a standard, explains the difference. The underlying encryption scheme, ML-KEM.PKE, has a decryption failure probability, computed from the error distribution over the polynomial coefficients after decompression. The answer says Table 1 of FIPS 203 reports this value for the encryption layer. The question that prompted the answer found slightly different numbers when using the public security-estimates scripts, for example 2^-139.1 for Kyber512. The answer says the decapsulation failure rate and the decryption failure rate are related but not identical.

ML-KEM decapsulation wraps the encryption scheme using the Fujisaki-Okamoto transform: it re-encrypts the recovered plaintext and compares the result with the original ciphertext. The 2024 paper treats the correctness of ML-KEM as a KEM as a separate statement that it derives from the correctness of the base scheme.

Limits

A proof about a specification and two implementations does not cover other libraries, side channels outside the constant-time model, or deployment. The failure probabilities are extremely small but not zero, and exact values depend on the parameter set.

FAQ

Is decryption failure the same as decapsulation failure?

A community answer says they are related but not identical: the first belongs to the encryption layer, the second to the KEM built on it.

What did the 2024 paper prove?

Correctness, including the decryption failure probability, and IND-CCA security of ML-KEM, machine-checked in EasyCrypt.

Does the proof cover code?

It covers two Jasmin implementations that the authors say are constant-time and functionally equivalent to the specification.

Does it cover every ML-KEM library?

No. It covers the specification and those two implementations.

What does Fujisaki-Okamoto do here?

It turns the IND-CPA secure base encryption scheme into an IND-CCA secure KEM, in the random oracle model according to the paper.