Proof obligation for `ind_cca_security` in `LatticeCrypto/MLKEM/Security.lean`

[quangvdao]

A proof in LatticeCrypto/MLKEM/Security.lean contains a sorry.

Goal: Replace the sorry with a complete proof.

Link to the sorry on GitHub

Code Snippet:

The proof composes three reductions:
1. **FO transform** (HHK17 Corollary): IND-CCA of the FO-constructed KEM reduces to
   IND-CPA of K-PKE + PRF security of J + correctness + message entropy.
2. **IND-CPA → MLWE**: Each IND-CPA term reduces to an MLWE advantage.
3. **Concrete parameters**: `ε_msg = 1/|Message| = 2⁻²⁵⁶` and `δ` from FIPS 203 Table 1. -/
theorem ind_cca_security

[alik-eth]

The in-source docstring already flags this as an unsound placeholder; recording it here too. correctnessBound : ℝ is signed; the hypothesis filters it through ENNReal.ofReal (which clamps negatives to 0), but the RHS uses correctnessBound raw via ((2·qHK+3 : ℕ) : ℝ) * correctnessBound. So correctnessBound = -10⁹ satisfies h_correct whenever deltaCorrect 0 does, while making the RHS arbitrarily negative below a nonnegative LHS probability — the bound is false.

Also blocked on FujisakiOkamoto.IND_CCA_bound (Composed.lean), which is itself an unproven placeholder.

Fix: retype correctnessBound : ℝ≥0 (or ℝ≥0∞) identified directly with the K-PKE δ from #213, and land the generic FO bound first. Until then this should stay open with the sorry, not be closed.

[alik-eth]

Proposal: redesign ind_cca_security (#215)

Status of the current statement (LatticeCrypto/MLKEM/Security.lean:174): false-as-stated, as the in-source WARNING and the earlier comment record — correctnessBound : ℝ is signed, h_correct filters it through ENNReal.ofReal (clamps negatives to 0), the RHS uses it raw, so correctnessBound = -10⁹ sinks the RHS below a nonnegative probability. Cross-checking current code surfaces two further defects the on-issue analysis did not flag: (1) qHK : ℕ is a free parameter with no query-count hypothesis on the adversary — at qHK = 0 the statement claims a constant bound for unbounded-query adversaries, false even after retyping; the same defect sits in the generic FujisakiOkamoto.IND_CCA_bound (Composed.lean:125) and UTransform.IND_CCA_bound. (2) The theorem is about foKEMScheme (the two-RO HHK17 U-transform with kdInput m c = m), which is not the FIPS ML-KEM wrapper in KEM.lean (single G(m ‖ H(ek)), key bound to the ek-hash) — the docstring half-acknowledges this; the redesign should name the gap. And the ∃-quantified mlwe has the same prover-chosen-witness vacuity as #214.

1. Corrected statement shape

All slack terms nonnegative and pinned to their sources; adversary query-bounded; MLWE instances pinned to #214's definitions:

theorem ind_cca_security (qHK : ℕ)
    (adv : (foKEMScheme …).IND_CCA_Adversary)
    (hq : adv.MakesAtMostQueries qHK) :   -- new; precedents: INDCPA/Oracle.lean:49, TTransform.lean:253
    ∃ (B₁ : Adversary (mlkemMLWEKeys …)) (B₂ : Adversary (mlkemMLWEEnc …))
      (prfAdv : PRFScheme.PRFAdversary (KPKE.Ciphertext …) SharedSecret),
      (foKEMScheme …).IND_CCA_Advantage (twoRORuntime …) adv ≤
        2 * |advantage (mlkemMLWEKeys …) B₁| + 2 * |advantage (mlkemMLWEEnc …) B₂|
        + prfAdvantage (prfJ …) prfAdv
        + ((2*qHK + 3 : ℕ) : ℝ) * (kpkeDeltaBad … + εK + εE).toReal     -- δ from #213, a definition
        + 2 * ((2*qHK + 2 : ℕ) : ℝ) * ((Fintype.card Message : ℝ)⁻¹)    -- ε_msg = 2⁻²⁵⁶ by computation, not hypothesis

kpkeDeltaBad is #213's explicit failure-probability expression (ℝ≥0∞, provably ≤ 1), so the sign bug is structurally impossible; ε_msg becomes a computed cardinality (Message = Bytes 32, card 2²⁵⁶) with the old h_epsMsg shape retired.

2. Composition structure and the FO boundary

This theorem should stay a composition: FO bound × (#214 IND-CPA→MLWE) × (#213 δ). The generic FO input, FujisakiOkamoto.IND_CCA_bound, is itself an unsound placeholder and is owner-blocked under #189/#190/#191 (free negative-real slacks there too, plus the missing query hypothesis noted above). This proposal does not expand into fixing those — it only requires that whatever corrected generic bound lands exposes: nonneg δ/ε_msg parameters, a MakesAtMostQueries-style hypothesis, and per-reduction ∃-adversaries (already the case). Until then #215 keeps its honest sorry against the corrected statement, which is independently landable and stops the current false shape from becoming a proof target.

3. Named idealizations and certificates

• Inherited from Proof obligation for kpke_delta_correct in LatticeCrypto/MLKEM/Security.lean #213/Proof obligation for kpke_ind_cpa_security in LatticeCrypto/MLKEM/Security.lean #214: sampleNTTIdealization εA, keyDerivationReplacement εK, coinsDerivationReplacement εE — quantified-distinguisher Props with inspectable content and the feat(MLDSA): EUF-CMA via CMA→NMA over the short-secret MLWE model (#228) #467 caveat (unrestricted quantifiers satisfiable only at large ε for deterministic prims; computational reading pending feat(OracleComp): oracle strategies as dynamical systems, oracle machines, and TM-grounded poly-time adversaries #460; precedents expandAIdealization/expandSReplacement, SecurityNMA.lean:484/:320).
• New here: a two-RO/single-RO bridge assumption if the owner wants the theorem to speak about the FIPS wrapper: gEncapsIdealization relating G(m ‖ H(ek)) (one prims.gEncaps call producing both coins and key) to the two independent ROs of twoRORuntime — or alternatively restate over FujisakiOkamoto.singleRO, which exists precisely for this. Owner decision; either way the gap gets a name instead of a docstring aside.
• Certificate gate (feat(MLDSA): EUF-CMA via CMA→NMA over the short-secret MLWE model (#228) #467 keygenShort_generable precedent): hq is inhabited by any concrete bounded adversary (ship one example); the prfJ scheme and pinned problems are definitions; failing the gate today: the ∃-quantified mlwe and the signed correctnessBound+h_correct pair (satisfiable only through the ofReal clamp — i.e., satisfiable because of the bug).

4. Honest scoping and out of scope

• In scope: the corrected statement (types, pinning, query bound, computed ε_msg); the composition proof once the generic FO bound is fixed; the named single-RO bridge decision.
• Out of scope: proving the generic FO/HHK17 bounds (Proof obligation for OW_PCVA_bound in VCVio/CryptoFoundations/FujisakiOkamoto/TTransform.lean #189/Proof obligation for IND_CCA_Advantage_composeWithKDM_le in VCVio/CryptoFoundations/FujisakiOkamoto/UTransform.lean #190/Proof obligation for IND_CCA_bound in VCVio/CryptoFoundations/FujisakiOkamoto/Composed.lean #191 — separately blocked on owner statement fixes); implicit-rejection PRF internals beyond the prfJ interface; QROM (all of this is classical ROM); cost model (feat(OracleComp): oracle strategies as dynamical systems, oracle machines, and TM-grounded poly-time adversaries #460). No ML-DSA-style provable obstruction found for the implicit-rejection structure itself, but the two-RO-vs-FIPS-G mismatch in §3 is the analogous "disclose it, don't paper over it" item.
• Landing order: (a) restate with corrected types + pinned instances + query hypothesis (immediate, independent); (b) Proof obligation for kpke_delta_correct in LatticeCrypto/MLKEM/Security.lean #213(c) and Proof obligation for kpke_ind_cpa_security in LatticeCrypto/MLKEM/Security.lean #214(b) land their definitions this consumes; (c) generic FO fix (other issues, owner); (d) the composition proof.

https://claude.ai/code/session_01DaNGD9nDo3Grwk58nsjS77