AnonymityFromSPR

Proved: anonymity is bounded by the two per-branch SPR advantages -- hop through a game whose challenge ciphertext comes from a key-independent simulator, hence carries no information about the hidden bit -- and, chaining into unlinkAdvantage_ofKEMFull_le, the full decomposition of stealth unlinkability into five named advantages with no unnamed slack.

Assumed: the SPR terms are decomposed in SPRTwoHop into two MLWE hops (both identities proved) plus two named residual terms (primitive idealization, simulator gap); lifting to ANO-CCA must track ML-KEM's implicit-rejection FO transform. Neither VCVio nor FIPS 203 supplies anonymity → MLWE. See docs/spr-two-hop.md.

`simBranch`

The anonymity experiment's branch with a simulated (key-independent) challenge ciphertext.

def simBranch (sim : ProbComp C) (adv : StealthScheme.UnlinkAdv PK C)
    (a : PK × PK) : ProbComp Bool := do
  let c ← sim
  adv a.1 a.2 c

AnonymityFromSPR.lean:33-37 ↗

`sprAdv`

noncomputable def sprAdv (kem : KEM PK SK C K) (sim : ProbComp C)
    (adv : StealthScheme.UnlinkAdv PK C) (b : Bool) : ℝ :=
  (kem.anonSetup >>= kem.anonBranch adv b).boolDistAdvantage
    (kem.anonSetup >>= simBranch sim adv)

AnonymityFromSPR.lean:41-45 ↗

`anonAdvantage_le_sprAdv`

axioms: propext, Classical.choice, Quot.sound · sorry-free ✓

theorem anonAdvantage_le_sprAdv (kem : KEM PK SK C K) (sim : ProbComp C)
    (adv : StealthScheme.UnlinkAdv PK C) :
    kem.anonAdvantage adv ≤ kem.sprAdv sim adv true + kem.sprAdv sim adv false := by

proof

  rw [KEM.anonAdvantage_eq_branchDistAdvantage, KEM.sprAdv, KEM.sprAdv,
    ProbComp.boolDistAdvantage_comm (kem.anonSetup >>= kem.anonBranch adv false)]
  exact ProbComp.boolDistAdvantage_triangle _ _ _

AnonymityFromSPR.lean:49-55 ↗

The simulated branch and per-branch SPR advantages

`unlinkAdvantage_ofKEMFull_le_full_decomposition`

Full-chain unlinkability bound. The complete announcement decomposes into five named advantages with no unnamed slack: the whole reduction skeleton of the scheme's privacy.

axioms: propext, Classical.choice, Quot.sound · sorry-free ✓

theorem unlinkAdvantage_ofKEMFull_le_full_decomposition
    (kem : KEM PK SK C K) (auxGen : K → PK → Aux) (sim : ProbComp C)
    (adv : StealthScheme.UnlinkAdv PK (C × Aux)) :
    (StealthScheme.ofKEMFull kem auxGen).unlinkAdvantage adv ≤
      sharedSecretHiding kem auxGen adv true
      + auxKeyIndependence kem auxGen adv
      + (kem.sprAdv sim (adv.cipherOf auxGen) true
         + kem.sprAdv sim (adv.cipherOf auxGen) false)
      + sharedSecretHiding kem auxGen adv false := by

proof

  calc (StealthScheme.ofKEMFull kem auxGen).unlinkAdvantage adv
      ≤ sharedSecretHiding kem auxGen adv true
        + auxKeyIndependence kem auxGen adv
        + kem.anonAdvantage (adv.cipherOf auxGen)
        + sharedSecretHiding kem auxGen adv false :=
        unlinkAdvantage_ofKEMFull_le kem auxGen adv
    _ ≤ sharedSecretHiding kem auxGen adv true
        + auxKeyIndependence kem auxGen adv
        + (kem.sprAdv sim (adv.cipherOf auxGen) true
           + kem.sprAdv sim (adv.cipherOf auxGen) false)
        + sharedSecretHiding kem auxGen adv false := by
        gcongr
        exact kem.anonAdvantage_le_sprAdv sim (adv.cipherOf auxGen)

AnonymityFromSPR.lean:65-87 ↗