ConstructionA

Proved: the auxGen the real scheme uses -- view tag plus hashAddr (pack rho (power2Round (A *ᵥ s' + e' + t))), symmetric primitives bundled uninterpreted as Prims -- so the announcement in the model is the announcement in the spec; the announced key is power2Round of the honest ML-DSA key of the widened secret and an ownership witness for it; auxKeyIndependence vanishes for any auxGen ignoring the public key; and the seeded-MLWE blindingProblem with its reduction adversary.

Assumed / NOT closed: hashAddr ∘ pack as a random oracle (rho sits outside the mask), ExpandIsIdeal, and a bind commutation -- so no advantage inequality is claimed for the blinding hop. See docs/announcement-model.md.

`auxKeyIndependence_eq_zero_of_pk_independent`

The term's meaning, pinned. When auxGen ignores its public-key argument the two computations compared by auxKeyIndependence are equal, so the advantage is 0.

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

theorem auxKeyIndependence_eq_zero_of_pk_independent
    (kem : KEM PK SK C K) (auxGen : K → PK → Aux)
    (adv : StealthScheme.UnlinkAdv PK (C × Aux))
    (h : ∀ (kk : K) (pk pk' : PK), auxGen kk pk = auxGen kk pk') :
    auxKeyIndependence kem auxGen adv = 0 := by

proof

  have key : ((StealthScheme.ofKEMFull kem auxGen).unlinkSetup >>=
        randAuxBranch kem auxGen adv true) =
      (kem.anonSetup >>= kem.anonBranch (adv.cipherOf auxGen) true) := by
    simp only [StealthScheme.unlinkSetup, StealthScheme.ofKEMFull, KEM.anonSetup,
      StealthScheme.UnlinkAdv.cipherOf, randAuxBranch, KEM.anonBranch,
      bind_assoc, pure_bind, if_true]
    refine bind_congr fun x => bind_congr fun y =>
      bind_congr fun c => bind_congr fun kk => ?_
    rw [h kk _ _]
  rw [auxKeyIndependence, key, ProbComp.boolDistAdvantage, sub_self, abs_zero]

ConstructionA.lean:34-49 ↗

`auxKeyIndependence_tagOnly_eq_zero`

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

theorem auxKeyIndependence_tagOnly_eq_zero
    (kem : KEM PK SK C K) (tag : K → Aux)
    (adv : StealthScheme.UnlinkAdv PK (C × Aux)) :
    auxKeyIndependence kem (fun kk _ => tag kk) adv = 0 :=
  auxKeyIndependence_eq_zero_of_pk_independent kem _ adv fun _ _ _ => rfl

ConstructionA.lean:53-58 ↗

1. Positive control for `auxKeyIndependence`

`Prims`

The symmetric primitives of construction A, bundled and uninterpreted, so everything proved holds for every instantiation.

structure Prims (R Rho Bytes T1 Tag Addr K : Type) (k l : ℕ) where
  /-- SHAKE128 expansion of the matrix seed. -/
  expandA : Rho → Matrix (Fin k) (Fin l) R
  /-- The blinding pair `(s', e')` derived from the shared secret. -/
  expandBlind : K → (Fin l → R) × (Fin k → R)
  /-- The high-order part of a stealth key. -/
  power2Round : (Fin k → R) → T1
  /-- `pack_pk`: the seed and the rounded key as bytes. -/
  pack : Rho → T1 → Bytes
  /-- The address hash. -/
  hashAddr : Bytes → Addr
  /-- The view tag derived from the shared secret. -/
  viewTag : K → Tag

ConstructionA.lean:70-83 ↗

`Samplers`

structure Samplers (R Rho : Type) (k l : ℕ) where
  /-- The matrix seed. -/
  sampleRho : ProbComp Rho
  /-- The short secret `s₁`. -/
  sampleS : ProbComp (Fin l → R)
  /-- The short error `s₂`. -/
  sampleE : ProbComp (Fin k → R)

ConstructionA.lean:87-94 ↗

`MetaPub`

The recipient's meta-address: ML-KEM encapsulation key, matrix seed rho, and the FULL-precision spending key t (rounding is only well defined on the unrounded value).

abbrev MetaPub (KEMpk Rho R : Type) (k : ℕ) : Type := KEMpk × Rho × (Fin k → R)

ConstructionA.lean:101-102 ↗

`MetaPriv`

abbrev MetaPriv (KEMsk R : Type) (k l : ℕ) : Type := KEMsk × (Fin l → R) × (Fin k → R)

ConstructionA.lean:105-106 ↗

`auxGen`

The auxiliary data of a construction-A announcement: view tag and stealth address. The address folds in the recipient's own rho and t, which is why auxGen takes the public key.

def auxGen (kk : K) (pk : MetaPub KEMpk Rho R k) : Tag × Addr :=
  (P.viewTag kk,
    P.hashAddr (P.pack pk.2.1 (P.power2Round
      (P.expandA pk.2.1 *ᵥ (P.expandBlind kk).1 + (P.expandBlind kk).2 + pk.2.2))))

ConstructionA.lean:112-116 ↗

`stealthAddr_eq_blinded_pk`

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

theorem stealthAddr_eq_blinded_pk (kk : K) (ek : KEMpk) (rho : Rho)
    (s₁ : Fin l → R) (s₂ : Fin k → R) :
    (auxGen (KEMpk := KEMpk) P kk (ek, rho, P.expandA rho *ᵥ s₁ + s₂)).2 =
      P.hashAddr (P.pack rho (P.power2Round
        (P.expandA rho *ᵥ (s₁ + (P.expandBlind kk).1) + (s₂ + (P.expandBlind kk).2)))) := by

proof

  rw [auxGen, stealth_pk_eq_blinded_keypair (P.expandA rho) s₁ (P.expandBlind kk).1 s₂
    (P.expandBlind kk).2 _ rfl]

ConstructionA.lean:120-127 ↗

`announced_key_isOwnershipWitness`

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

theorem announced_key_isOwnershipWitness (kk : K) (rho : Rho)
    (s₁ : Fin l → R) (s₂ : Fin k → R) :
    IsOwnershipWitness (P.expandA rho)
      (P.expandA rho *ᵥ (P.expandBlind kk).1 + (P.expandBlind kk).2
        + (P.expandA rho *ᵥ s₁ + s₂))
      (s₁ + (P.expandBlind kk).1) (s₂ + (P.expandBlind kk).2) :=
  blinded_is_ownership_witness _ _ _ _ _

ConstructionA.lean:131-138 ↗

2. The announcement

`metaKem`

The composite KEM: an ML-KEM keypair plus the ML-DSA spending keypair, with the meta-address as the public key.

def metaKem (kem : KEM KEMpk KEMsk C K) :
    KEM (MetaPub KEMpk Rho R k) (MetaPriv KEMsk R k l) C K where
  keygen := do
    let (ek, dk) ← kem.keygen
    let rho ← Smp.sampleRho
    let s₁ ← Smp.sampleS
    let s₂ ← Smp.sampleE
    pure ((ek, rho, P.expandA rho *ᵥ s₁ + s₂), (dk, s₁, s₂))
  encaps pk := kem.encaps pk.1
  decaps sk c := kem.decaps sk.1 c

ConstructionA.lean:148-158 ↗

`scheme`

Construction A as a StealthScheme: ML-KEM ciphertext plus view tag plus stealth address, addressed to a full meta-address.

def scheme (kem : KEM KEMpk KEMsk C K) :
    StealthScheme (MetaPub KEMpk Rho R k)
      (MetaPriv KEMsk R k l × MetaPub KEMpk Rho R k) (C × (Tag × Addr)) :=
  StealthScheme.ofKEMFull (metaKem P Smp kem) (auxGen P)

ConstructionA.lean:165-169 ↗

`unlinkAdvantage_metaKem_le`

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

theorem unlinkAdvantage_metaKem_le (kem : KEM KEMpk KEMsk C K)
    (adv : StealthScheme.UnlinkAdv (MetaPub KEMpk Rho R k) (C × (Tag × Addr))) :
    (scheme P Smp kem).unlinkAdvantage adv ≤
      sharedSecretHiding (metaKem P Smp kem) (auxGen P) adv true
        + auxKeyIndependence (metaKem P Smp kem) (auxGen P) adv
        + (metaKem P Smp kem).anonAdvantage (adv.cipherOf (auxGen P))
        + sharedSecretHiding (metaKem P Smp kem) (auxGen P) adv false :=
  unlinkAdvantage_ofKEMFull_le _ _ adv

ConstructionA.lean:179-187 ↗

3. The KEM whose public key is a meta-address

`blindingProblem`

Seeded decision-MLWE: given (rho, y), decide whether y = expandA rho *ᵥ s + e for short (s, e) or y is uniform. An instance of VCVio's LearningWithErrors.Problem.

def blindingProblem : LearningWithErrors.Problem Rho (Fin l → R) (Fin k → R) where
  sampleChallenge := Smp.sampleRho
  sampleSecret := Smp.sampleS
  sampleError := Smp.sampleE
  noiseless := fun s rho => P.expandA rho *ᵥ s
  sampleUniform := $ᵗ (Fin k → R)

ConstructionA.lean:204-210 ↗

`realJoint`

The real joint draw the blinding argument is about: one shared secret, its view tag and its blinding pair. ExpandIsIdeal says this is the ideal draw below; naming both computations keeps the idealization statements free of nested do-blocks and lets downstream lemmas cite the object instead of re-spelling it.

def realJoint (P : Prims R Rho Bytes T1 Tag Addr K k l) :
    ProbComp (Tag × (Fin l → R) × (Fin k → R)) := do
  let kk ← ($ᵗ K)
  let tg := P.viewTag kk
  let s' := (P.expandBlind kk).1
  let e' := (P.expandBlind kk).2
  pure (tg, s', e')

ConstructionA.lean:219-226 ↗

`idealJoint`

def idealJoint (Smp : Samplers R Rho k l) (sampleTag : ProbComp Tag) :
    ProbComp (Tag × (Fin l → R) × (Fin k → R)) := do
  let tg ← sampleTag
  let s' ← Smp.sampleS
  let e' ← Smp.sampleE
  pure (tg, s', e')

ConstructionA.lean:229-235 ↗

`BlindExpandIdealizationBound`

def BlindExpandIdealizationBound (epsilonBlindExpand : ℝ≥0∞) : Prop :=
  ∀ (D : Tag × (Fin l → R) × (Fin k → R) → ProbComp Bool),
    ProbComp.boolDistAdvantage (realJoint P >>= D)
      (idealJoint Smp sampleTag >>= D) ≤ epsilonBlindExpand.toReal

ConstructionA.lean:240-244 ↗

`ExpandIsIdeal`

def ExpandIsIdeal : Prop :=
  ∀ x : Tag × (Fin l → R) × (Fin k → R),
    Pr[= x | realJoint P] = Pr[= x | idealJoint Smp sampleTag]
 
omit [CommRing R] [SampleableType R] in

ConstructionA.lean:248-252 ↗

`blindExpandIdealizationBound_zero_of_expandIsIdeal`

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

theorem blindExpandIdealizationBound_zero_of_expandIsIdeal
    (h : ExpandIsIdeal P Smp sampleTag) :
    BlindExpandIdealizationBound P Smp sampleTag 0 := by

proof

  intro D
  have hpr : Pr[= true | (realJoint P >>= D)] =
      Pr[= true | (idealJoint Smp sampleTag >>= D)] :=
    probOutput_congr rfl (by rw [evalDist_bind, evalDist_bind, evalDist_ext h])
  simp only [ProbComp.boolDistAdvantage, hpr, sub_self, abs_zero,
    ENNReal.toReal_zero]
  exact le_rfl

ConstructionA.lean:258-268 ↗

`mlweAdvOfUnlinkAdv`

def mlweAdvOfUnlinkAdv (kem : KEM KEMpk KEMsk C K)
    (adv : StealthScheme.UnlinkAdv (MetaPub KEMpk Rho R k) (C × (Tag × Addr))) :
    LearningWithErrors.Adversary (blindingProblem P Smp) :=
  fun chal => do
    let (ek0, _) ← kem.keygen
    let rho0 ← Smp.sampleRho
    let s₁ ← Smp.sampleS
    let s₂ ← Smp.sampleE
    let (ek1, _) ← kem.keygen
    let s₁' ← Smp.sampleS
    let s₂' ← Smp.sampleE
    let t₁ := P.expandA chal.1 *ᵥ s₁' + s₂'
    let (c, _) ← kem.encaps ek1
    let tg ← sampleTag
    adv (ek0, rho0, P.expandA rho0 *ᵥ s₁ + s₂) (ek1, chal.1, t₁)
      (c, (tg, P.hashAddr (P.pack chal.1 (P.power2Round (chal.2 + t₁)))))

ConstructionA.lean:272-288 ↗

`idealAux_indep_of_t`

The middle-game independence lemma. A uniform mask absorbs the offset, so the blinding does erase t. Note what is NOT quantified over: rho, which enters outside the mask and therefore has to be shared between the two sides.

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

theorem idealAux_indep_of_t (cont : Tag × Addr → ProbComp Bool) (tg : Tag)
    (rho : Rho) (t t' : Fin k → R) (z : Bool) :
    Pr[= z | (do let u ← ($ᵗ (Fin k → R))
                 cont (tg, P.hashAddr (P.pack rho (P.power2Round (u + t)))))] =
      Pr[= z | (do let u ← ($ᵗ (Fin k → R))
                   cont (tg, P.hashAddr (P.pack rho (P.power2Round (u + t')))))] := by

proof

  rw [probOutput_bind_add_right_uniform (Fin k → R) t
      (fun v => cont (tg, P.hashAddr (P.pack rho (P.power2Round v)))) z,
    probOutput_bind_add_right_uniform (Fin k → R) t'
      (fun v => cont (tg, P.hashAddr (P.pack rho (P.power2Round v)))) z]

ConstructionA.lean:299-309 ↗

ConstructionA

1. Positive control for auxKeyIndependence

2. The announcement

3. The KEM whose public key is a meta-address

1. Positive control for `auxKeyIndependence`