Certified upper bound on ML-KEM-768 error scale in a cryptographic model
Dependency-Aware ROM/CBD Correctness Bounds for ML-KEM-768 at the Heuristic Failure Scale
Cryptography and Security
Summary
ML-KEM-768 is a cryptographic method used to secure information, but sometimes the process to decode messages can fail. The authors provide a mathematically backed upper limit on how often these failures can happen within a specific abstract model. They carefully accounted for complex dependencies in the system, providing a very precise bound that is slightly better than previous estimates. This work does not claim to prove security for a particular real-world implementation but gives a useful theoretical guarantee under certain assumptions.
What this means in practice
- •For cryptographic protocol developers: Use the explicit failure bound to evaluate and design lattice-based key encapsulation methods with better reliability guarantees.
- •For security auditors: Apply the certified upper bound to assess the risk of message recovery errors in systems deploying ML-KEM-768 under honest usage assumptions.
Authors
Aurélie Duriez, Christophe Tommasini
Abstract
We certify an honest-decapsulation failure upper bound for ML-KEM-768 in an explicit random-function/centered-binomial (ROM/CBD) abstraction. Domain-separated public-matrix streams are modeled as independent uniform ring elements and secret/noise polynomials as independent CBD2 primitives; this is not an information-theoretic statement about the fixed SHAKE instantiation of FIPS 203. Recent formal assessments identify rigorous justification of ML-KEM's heuristic decapsulation-failure scale as an open problem; within the explicit ROM/CBD abstraction studied here, we obtain a dependency-preserving certified upper bound at that scale. The analysis preserves dependencies induced by the public matrix and by both ciphertext-compression terms. Its terminal chain has three components: an exact graph-coupled full-ideal reference for the joint c_u/c_v residual; a proper-ideal bivariate Fourier transport whose rare |T|>=3 branch is closed by an exhaustive three-factor anti-concentration replay; and exact bit-specific FIPS decoding events followed only by a 256-coordinate union bound. A formal partial-Fourier lemma makes the spectral-to-total-variation step explicit. The reduced rational certificate satisfies Pr[K' != K] <= P_* <= 2^-164.81, with -log2(P_*) = 164.810716201343121.... The 164.81 threshold is exact but numerically tight: the certified exponent exceeds it by only about 0.0007162 bit, and 164.82 is not certified. The result is an upper bound for an arbitrary message fixed independently of the public and secret randomness, under honest encryption and decapsulation. It is not an exact DFR, not a fixed-SHAKE equivalence theorem, not a new IND-CCA reduction, and not an adaptive delta-correctness result.