SharedSecretHiding

Proved: each shared-secret-hiding term of unlinkAdvantage_ofKEMFull_le is the bias of a real-or-random guessing game, and that bias EQUALS KEMScheme.IND_CPA_Advantage of the explicit reduction adversary indCpaAdv against the KEM itself. The two experiments draw the same independent samples in different orders, with one draw unused on one branch; bind is a syntactic constructor, so this holds after evalDist rather than on the nose, which is all an advantage sees. Hence unlinkAdvantage_ofKEMFull_le_indCpa.

Assumed: nothing. Bounding KEMScheme.IND_CPA_Advantage for ML-KEM by MLWE is the missing upstream lemma recorded in MLKEM.lean. See docs/spr-two-hop.md.

`indCpaAdv`

IND-CPA reduction adversary for branch b: the challenge key is embedded as recipient b, the other recipient is generated by the reduction, and the state carries both keys so the auxiliary data can be rebuilt from the challenge key.

def indCpaAdv (b : Bool) : kem.IND_CPA_Adversary where
  State := PK × PK
  preChallenge pk := do
    let (pk', _) ← kem.keygen
    pure (if b then (pk', pk) else (pk, pk'))
  postChallenge s cStar k := adv s.1 s.2 (cStar, auxGen k (if b then s.2 else s.1))

SharedSecretHiding.lean:35-41 ↗

The concrete VCVio IND-CPA reduction adversary

`evalDist_bind_pull_front`

An independent draw may be pulled to the front of a two-step prefix (the dependent-prefix form of Reorder.evalDist_pull₃).

theorem evalDist_bind_pull_front {α β δ ζ : Type}
    (oa : ProbComp α) (ob : α → ProbComp β) (od : ProbComp δ)
    (k : α → β → δ → ProbComp ζ) :
    𝒟[(do let a ← oa; let b ← ob a; let d ← od; k a b d)] =
      𝒟[(do let d ← od; let a ← oa; let b ← ob a; k a b d)] := by

proof

  calc 𝒟[(do let a ← oa; let b ← ob a; let d ← od; k a b d)]
      = 𝒟[(do let a ← oa; let d ← od; let b ← ob a; k a b d)] := by
        refine evalDist_bind_congr' _ fun a => ?_
        exact evalDist_bind_bind_swap (ob a) od fun b d => k a b d
    _ = 𝒟[(do let d ← od; let a ← oa; let b ← ob a; k a b d)] :=
        evalDist_bind_bind_swap oa od _

SharedSecretHiding.lean:51-62 ↗

`boolBiasAdvantage_congr`

theorem boolBiasAdvantage_congr {p q : ProbComp Bool} (h : 𝒟[p] = 𝒟[q]) :
    p.boolBiasAdvantage = q.boolBiasAdvantage := by

proof

  simp only [ProbComp.boolBiasAdvantage, probOutput_def, h]

SharedSecretHiding.lean:64-67 ↗

Distribution-level bridges

`rorNormalForm`

Normal form of the branch-b reduction game: hidden bit, keypair 0, keypair 1, the challenge encapsulation to recipient b, then the idealized shared secret -- drawn on both branches of the hidden bit.

noncomputable def rorNormalForm (b : Bool) : ProbComp Bool := do
  let hb ← ($ᵗ Bool)
  let pk0 ← kem.keygen
  let pk1 ← kem.keygen
  let ck ← kem.encaps (if b then pk1.1 else pk0.1)
  let kRand ← ($ᵗ K)
  let z ← adv pk0.1 pk1.1
    (ck.1, auxGen (if hb then ck.2 else kRand) (if b then pk1.1 else pk0.1))
  pure (hb == z)

SharedSecretHiding.lean:78-87 ↗

`indCpaGame_eq_evalDist_normalForm`

theorem indCpaGame_eq_evalDist_normalForm (b : Bool) :
    KEMScheme.IND_CPA_Game ProbCompRuntime.probComp (indCpaAdv kem auxGen adv b) =
      𝒟[rorNormalForm kem auxGen adv b] := by

proof

  cases b with
  | true =>
    have hgame : KEMScheme.IND_CPA_Game ProbCompRuntime.probComp
        (indCpaAdv kem auxGen adv true) =
        𝒟[(do
          let pk1 ← kem.keygen
          let pk0 ← kem.keygen
          let hb ← ($ᵗ Bool)
          let ck ← kem.encaps pk1.1
          let kRand ← ($ᵗ K)
          let z ← adv pk0.1 pk1.1 (ck.1, auxGen (if hb then ck.2 else kRand) pk1.1)
          pure (hb == z) : ProbComp Bool)] := by
      simp only [KEMScheme.IND_CPA_Game, indCpaAdv, bind_assoc, pure_bind,
        ProbCompRuntime.probComp, ProbCompRuntime.liftProbComp, ProbCompLift.id]
      rfl
    rw [hgame, evalDist_bind_bind_swap kem.keygen kem.keygen
      (fun pk1 pk0 => do
        let hb ← ($ᵗ Bool)
        let ck ← kem.encaps pk1.1
        let kRand ← ($ᵗ K)
        let z ← adv pk0.1 pk1.1 (ck.1, auxGen (if hb then ck.2 else kRand) pk1.1)
        pure (hb == z))]
    exact evalDist_bind_pull_front kem.keygen (fun _ => kem.keygen) ($ᵗ Bool)
      (fun pk0 pk1 hb => do
        let ck ← kem.encaps pk1.1
        let kRand ← ($ᵗ K)
        let z ← adv pk0.1 pk1.1 (ck.1, auxGen (if hb then ck.2 else kRand) pk1.1)
        pure (hb == z))
  | false =>
    have hgame : KEMScheme.IND_CPA_Game ProbCompRuntime.probComp
        (indCpaAdv kem auxGen adv false) =
        𝒟[(do
          let pk0 ← kem.keygen
          let pk1 ← kem.keygen
          let hb ← ($ᵗ Bool)
          let ck ← kem.encaps pk0.1
          let kRand ← ($ᵗ K)
          let z ← adv pk0.1 pk1.1 (ck.1, auxGen (if hb then ck.2 else kRand) pk0.1)
          pure (hb == z) : ProbComp Bool)] := by
      simp only [KEMScheme.IND_CPA_Game, indCpaAdv, bind_assoc, pure_bind,
        ProbCompRuntime.probComp, ProbCompRuntime.liftProbComp, ProbCompLift.id]
      rfl
    rw [hgame]
    exact evalDist_bind_pull_front kem.keygen (fun _ => kem.keygen) ($ᵗ Bool)
      (fun pk0 pk1 hb => do
        let ck ← kem.encaps pk0.1
        let kRand ← ($ᵗ K)
        let z ← adv pk0.1 pk1.1 (ck.1, auxGen (if hb then ck.2 else kRand) pk0.1)
        pure (hb == z))

SharedSecretHiding.lean:91-143 ↗

The hiding terms ARE VCVio IND-CPA advantages

`rorGame`

The shared-secret real-or-random game on branch b: real secret or fresh random key, from the SAME public key on both sides. Orientation is VCVio's -- the REAL secret sits on hidden bit true, for both values of b.

noncomputable def rorGame (b : Bool) : ProbComp Bool := do
  let hb ← ($ᵗ Bool)
  let z ← if hb then
      (StealthScheme.ofKEMFull kem auxGen).unlinkSetup >>=
        (StealthScheme.ofKEMFull kem auxGen).unlinkBranch adv b
    else
      (StealthScheme.ofKEMFull kem auxGen).unlinkSetup >>=
        randAuxBranch kem auxGen adv b
  pure (hb == z)

SharedSecretHiding.lean:151-160 ↗