DKSAP

Proved: DKSAP (ERC-5564 scheme 1, the only stealth scheme deployed today) as a StealthScheme, and its detection completeness; given the discrete logs of the PUBLISHED meta-address, an adversary recomputes the recipient's honest stealth spending key EXACTLY -- key recovery, hence universal forgery, with no probability slack; and, on the other side, DKSAP's unlinkability is bounded by two hashed-Diffie-Hellman terms and nothing else, the idealized middle game contributing exactly zero.

Scope of the break, precisely: dksap_key_recovery recovers the scalar that recover computes, and the statement is (recover …) • g = (m • g) + (h (r • (v • g))) • g -- the recovered scalar controls the announced ADDRESS, i.e. the public key. It does NOT say the adversary can produce a signature or otherwise SPEND from it; that needs the discrete-log-to-signing step of the concrete signature scheme, which this module does not model. Call it "key/address recovery modulo the address-hashing step", and do not read it as a signing-key extraction theorem.

Assumed: the discrete-log oracle's answers are hypotheses (no quantum computation is formalized), and hashed-DH is stated, not proved -- exactly as MLWE is on the lattice side. See docs/dksap-asymmetry.md.

`dksap_derivation_agrees`

The Diffie-Hellman step: sender and recipient reach the same scalar because r • (v • g) = v • (r • g). This is the identity the whole scheme rests on, and also the reason the attack works once v is known.

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

theorem dksap_derivation_agrees (g : G) (h : G → F) (m v r : F) :
    (m • g) + (h (r • (v • g))) • g = (m + h (v • (r • g))) • g := by

proof

  rw [add_smul, smul_smul, smul_smul, mul_comm]

DKSAP.lean:45-48 ↗

The group model

`dksap`

DKSAP as a stealth scheme: the announcement is (R, P) = (r • g, M + h(r • V) • g), and the recipient recomputes the scalar as h(v • R). P stands in for the on-chain address, whose hashing is irrelevant here.

def dksap : StealthScheme (G × G) (F × F) (G × G) where
  keygen := do
    let m ← ($ᵗ F)
    let v ← ($ᵗ F)
    pure ((m • g, v • g), (m, v))
  announce MV := do
    let r ← ($ᵗ F)
    pure (r • g, MV.1 + (h (r • MV.2)) • g)
  scan mv Rp := pure (decide (Rp.2 = (mv.1 + h (mv.2 • Rp.1)) • g))

DKSAP.lean:61-70 ↗

`dksap_perfectlyComplete`

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

theorem dksap_perfectlyComplete : (dksap g h).PerfectlyComplete := by

proof

  simp only [StealthScheme.PerfectlyComplete, StealthScheme.CorrectExp, dksap,
    bind_pure_comp, Functor.map_map, bind_assoc, bind_map_left, dksap_derivation_agrees,
    decide_true, probOutput_bind_const, probFailure_of_liftM_PMF, tsub_zero,
    probOutput_map_const, probOutput_pure, ↓reduceIte, mul_one]

DKSAP.lean:74-79 ↗

The scheme

`recover`

What the adversary computes: the spending scalar of the announcement R, from the two recovered discrete logs. No secret of the recipient is used.

def recover (xM xV : F) (R : G) : F := xM + h (xV • R)

DKSAP.lean:93-94 ↗

`dksap_recover_eq_honest`

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

theorem dksap_recover_eq_honest
    (hinj : Function.Injective (fun x : F => x • g))
    (m v xM xV : F) (hM : xM • g = m • g) (hV : xV • g = v • g) (R : G) :
    recover h xM xV R = m + h (v • R) := by

proof

  rw [recover, hinj hM, hinj hV]

DKSAP.lean:98-103 ↗

`dksap_key_recovery`

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

theorem dksap_key_recovery
    (hinj : Function.Injective (fun x : F => x • g))
    (m v r xM xV : F) (hM : xM • g = m • g) (hV : xV • g = v • g) :
    (recover h xM xV (r • g)) • g = (m • g) + (h (r • (v • g))) • g := by

proof

  rw [dksap_recover_eq_honest h g hinj m v xM xV hM hV, dksap_derivation_agrees]

DKSAP.lean:107-112 ↗

Key recovery from the published meta-address

`dksapIdeal`

DKSAP with an idealized sender: the shared scalar is uniform instead of h(r * V). A proof device, not a runnable scheme -- detection cannot work -- used only as the middle game of a hop.

def dksapIdeal : StealthScheme (G × G) (F × F) (G × G) where
  keygen := do
    let m ← ($ᵗ F)
    let v ← ($ᵗ F)
    pure ((m • g, v • g), (m, v))
  announce MV := do
    let r ← ($ᵗ F)
    let s ← ($ᵗ F)
    pure (r • g, MV.1 + s • g)
  scan _ _ := pure false

DKSAP.lean:125-135 ↗

DKSAP under a classical adversary

`dksapIdeal_announce_indep`

With a uniform scalar, announcing to M1 and to M0 are the same computation: substitute s ↦ d + s for d the discrete log of M1 - M0.

theorem dksapIdeal_announce_indep
    (hbij : Function.Bijective (fun x : F => x • g))
    (M0 M1 : G) (cont : G → ProbComp Bool) (z : Bool) :
    Pr[= z | ($ᵗ F) >>= fun s => cont (M1 + s • g)] =
      Pr[= z | ($ᵗ F) >>= fun s => cont (M0 + s • g)] := by

proof

  obtain ⟨d, hd⟩ := hbij.surjective (M1 - M0)
  simp only at hd
  have key : ∀ s : F, M0 + (d + s) • g = M1 + s • g := by
    intro s
    rw [add_smul, ← add_assoc, hd, add_sub_cancel]
  have hbij' : Function.Bijective (fun s : F => d + s) := (Equiv.addLeft d).bijective
  calc Pr[= z | ($ᵗ F) >>= fun s => cont (M1 + s • g)]
      = Pr[= z | ($ᵗ F) >>= fun s => (fun s' => cont (M0 + s' • g)) (d + s)] := by
        simp only [key]
    _ = Pr[= z | ($ᵗ F) >>= fun s' => cont (M0 + s' • g)] :=
        probOutput_bind_bijective_uniform_cross F (fun s : F => d + s) hbij'
          (fun s' => cont (M0 + s' • g)) z

DKSAP.lean:142-159 ↗

`dksapIdeal_branch_indep`

theorem dksapIdeal_branch_indep
    (hbij : Function.Bijective (fun x : F => x • g))
    (M0 M1 : G) (cont : G × G → ProbComp Bool) (z : Bool) :
    Pr[= z | ($ᵗ F) >>= fun r => ($ᵗ F) >>= fun s => cont (r • g, M1 + s • g)] =
      Pr[= z | ($ᵗ F) >>= fun r => ($ᵗ F) >>= fun s => cont (r • g, M0 + s • g)] := by

proof

  have inner := fun (r : F) =>
    dksapIdeal_announce_indep g hbij M0 M1 (fun P => cont (r • g, P)) z
  simp only [probOutput_bind_eq_tsum] at inner ⊢
  exact tsum_congr fun r => by rw [inner r]

DKSAP.lean:161-170 ↗

`dksapIdeal_unlinkAdvantage_eq_zero`

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

theorem dksapIdeal_unlinkAdvantage_eq_zero
    (hbij : Function.Bijective (fun x : F => x • g)) :
    (dksapIdeal F g).unlinkAdvantage adv = 0 := by

proof

  rw [StealthScheme.unlinkAdvantage_eq_branchDistAdvantage, ProbComp.boolDistAdvantage]
  refine abs_eq_zero.mpr (sub_eq_zero.mpr ?_)
  congr 1
  simp only [probOutput_bind_eq_tsum]
  refine tsum_congr fun a => ?_
  congr 1
  simp only [StealthScheme.unlinkBranch, dksapIdeal, bind_assoc, pure_bind,
    if_true, Bool.false_eq_true, if_false]
  exact dksapIdeal_branch_indep g hbij _ _ _ _

DKSAP.lean:174-186 ↗

The idealized scheme is perfectly unlinkable

`hashedDH`

Hashed-DH advantage on branch b: real h(r * V) versus uniform. The classical assumption the scheme rests on, and exactly what a discrete-log oracle destroys.

noncomputable def hashedDH (b : Bool) : ℝ :=
  ((dksap g h).unlinkSetup >>= (dksap g h).unlinkBranch adv b).boolDistAdvantage
    ((dksapIdeal F g).unlinkSetup >>= (dksapIdeal F g).unlinkBranch adv b)

DKSAP.lean:202-205 ↗

The two hops

`dksap_unlinkAdvantage_le_hashedDH`

DKSAP's unlinkability is two hashed-DH gaps, the idealized middle game contributing exactly zero. hashedDH is itself a game distance; it is bounded by VCVio's named DDH and entropy-smoothing advantages below (hashedDH_le_ddh_add_es). Read alongside dksap_key_recovery: the same scheme is sound classically and totally broken given a discrete-log oracle.

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

theorem dksap_unlinkAdvantage_le_hashedDH
    (hbij : Function.Bijective (fun x : F => x • g)) :
    (dksap g h).unlinkAdvantage adv ≤ hashedDH g h adv true + hashedDH g h adv false := by

proof

  rw [StealthScheme.unlinkAdvantage_eq_branchDistAdvantage]
  unfold hashedDH
  rw [ProbComp.boolDistAdvantage_comm
    ((dksap g h).unlinkSetup >>= (dksap g h).unlinkBranch adv false)]
  set Pt := (dksap g h).unlinkSetup >>= (dksap g h).unlinkBranch adv true
  set Pf := (dksap g h).unlinkSetup >>= (dksap g h).unlinkBranch adv false
  set It := (dksapIdeal F g).unlinkSetup >>=
    (dksapIdeal F g).unlinkBranch adv true
  set If := (dksapIdeal F g).unlinkSetup >>=
    (dksapIdeal F g).unlinkBranch adv false
  have hzero : It.boolDistAdvantage If = 0 := by
    rw [← StealthScheme.unlinkAdvantage_eq_branchDistAdvantage]
    exact dksapIdeal_unlinkAdvantage_eq_zero g adv hbij
  calc Pt.boolDistAdvantage Pf
      ≤ Pt.boolDistAdvantage It + It.boolDistAdvantage Pf :=
        ProbComp.boolDistAdvantage_triangle Pt It Pf
    _ ≤ Pt.boolDistAdvantage It + (It.boolDistAdvantage If + If.boolDistAdvantage Pf) := by
        gcongr
        exact ProbComp.boolDistAdvantage_triangle It If Pf
    _ = Pt.boolDistAdvantage It + If.boolDistAdvantage Pf := by
        rw [hzero, zero_add]

DKSAP.lean:213-237 ↗

The classical security statement

`ddhReductionDKSAP`

The DDH reduction on branch b: the challenge A is the target's viewing key, B the ephemeral key, T the point to hash; the remaining keys are drawn in the order mT, mO, vO.

def ddhReductionDKSAP (b : Bool) : DiffieHellman.DDHAdversary F G := fun g A B T => do
  let mT ← ($ᵗ F); let mO ← ($ᵗ F); let vO ← ($ᵗ F)
  let pkT : G × G := (mT • g, A)
  let pkO : G × G := (mO • g, vO • g)
  adv (if b then pkO else pkT) (if b then pkT else pkO) (B, mT • g + h T • g)

DKSAP.lean:257-262 ↗

`dksapDHGame`

def dksapDHGame (b : Bool) : ProbComp Bool := do
  let vT ← ($ᵗ F); let r ← ($ᵗ F); let c ← ($ᵗ F)
  let mT ← ($ᵗ F); let mO ← ($ᵗ F); let vO ← ($ᵗ F)
  let pkT : G × G := (mT • g, vT • g)
  let pkO : G × G := (mO • g, vO • g)
  adv (if b then pkO else pkT) (if b then pkT else pkO) (r • g, mT • g + h (c • g) • g)

DKSAP.lean:266-272 ↗

`esReductionDKSAP`

def esReductionDKSAP (b : Bool) : Fin 1 × F → ProbComp Bool := fun x => do
  let vT ← ($ᵗ F); let r ← ($ᵗ F)
  let mT ← ($ᵗ F); let mO ← ($ᵗ F); let vO ← ($ᵗ F)
  let pkT : G × G := (mT • g, vT • g)
  let pkO : G × G := (mO • g, vO • g)
  adv (if b then pkO else pkT) (if b then pkT else pkO) (r • g, mT • g + x.2 • g)

DKSAP.lean:276-282 ↗

`evalDist_unlinkBranch_dksap_eq_ddhExpReal`

theorem evalDist_unlinkBranch_dksap_eq_ddhExpReal [DecidableEq G] (b : Bool) :
    𝒟[(dksap g h).unlinkSetup >>= (dksap g h).unlinkBranch adv b] =
      𝒟[DiffieHellman.ddhExpReal g (ddhReductionDKSAP h adv b)] := by

proof

  cases b
  · simp only [StealthScheme.unlinkSetup, StealthScheme.unlinkBranch, dksap, ddhReductionDKSAP,
      DiffieHellman.ddhExpReal, bind_assoc, pure_bind, Bool.false_eq_true, if_false, smul_smul]
    rw [evalDist_bind_bind_swap]
    refine evalDist_bind_congr' _ fun v0 => ?_
    rw [evalDist_pull₄]
    refine evalDist_bind_congr' _ fun r => evalDist_bind_congr' _ fun m0 =>
      evalDist_bind_congr' _ fun m1 => evalDist_bind_congr' _ fun v1 => ?_
    rw [mul_comm r v0]
  · simp only [StealthScheme.unlinkSetup, StealthScheme.unlinkBranch, dksap, ddhReductionDKSAP,
      DiffieHellman.ddhExpReal, bind_assoc, pure_bind, if_true, smul_smul]
    rw [evalDist_pull₄]
    refine evalDist_bind_congr' _ fun v1 => ?_
    rw [evalDist_pull₄]
    refine evalDist_bind_congr' _ fun r => ?_
    rw [evalDist_pull₃]
    refine evalDist_bind_congr' _ fun m1 => evalDist_bind_congr' _ fun m0 =>
      evalDist_bind_congr' _ fun v0 => ?_
    rw [mul_comm r v1]

DKSAP.lean:284-306 ↗

`evalDist_ddhExpRand_eq_dksapDHGame`

theorem evalDist_ddhExpRand_eq_dksapDHGame (b : Bool) :
    𝒟[DiffieHellman.ddhExpRand g (ddhReductionDKSAP h adv b)] = 𝒟[dksapDHGame g h adv b] := by

proof

  simp only [DiffieHellman.ddhExpRand, ddhReductionDKSAP, dksapDHGame]

DKSAP.lean:308-311 ↗

`evalDist_dksapDHGame_eq_esReal`

theorem evalDist_dksapDHGame_eq_esReal (b : Bool) :
    𝒟[dksapDHGame g h adv b] =
      𝒟[EntropySmoothing.realExp F g (fun (_ : Fin 1) => h) (esReductionDKSAP g adv b)] := by

proof

  simp only [EntropySmoothing.realExp, esReductionDKSAP, dksapDHGame]
  rw [evalDist_uniformSample_bind_const, evalDist_pull₃]

DKSAP.lean:313-318 ↗

`evalDist_esIdeal_eq_unlinkBranch_dksapIdeal`

theorem evalDist_esIdeal_eq_unlinkBranch_dksapIdeal (b : Bool) :
    𝒟[EntropySmoothing.idealExp (HK := Fin 1) (M := F) (esReductionDKSAP g adv b)] =
      𝒟[(dksapIdeal F g).unlinkSetup >>= (dksapIdeal F g).unlinkBranch adv b] := by

proof

  simp only [EntropySmoothing.idealExp, esReductionDKSAP, StealthScheme.unlinkSetup,
    StealthScheme.unlinkBranch, dksapIdeal, bind_assoc, pure_bind]
  rw [evalDist_uniformSample_bind_const]
  symm
  cases b
  · simp only [Bool.false_eq_true, if_false]
    rw [evalDist_pull₆]
    refine evalDist_bind_congr' _ fun s => ?_
    rw [evalDist_bind_bind_swap]
    refine evalDist_bind_congr' _ fun v0 => ?_
    rw [evalDist_pull₄]
  · simp only [if_true]
    rw [evalDist_pull₆]
    refine evalDist_bind_congr' _ fun s => ?_
    rw [evalDist_pull₄]
    refine evalDist_bind_congr' _ fun v1 => ?_
    rw [evalDist_pull₄]
    refine evalDist_bind_congr' _ fun r => ?_
    rw [evalDist_pull₃]

DKSAP.lean:320-342 ↗

`hashedDH_le_ddh_add_es`

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

theorem hashedDH_le_ddh_add_es [DecidableEq G] (b : Bool) :
    hashedDH g h adv b ≤
      DiffieHellman.ddhDistAdvantage g (ddhReductionDKSAP h adv b) +
        EntropySmoothing.advantage F g (fun (_ : Fin 1) => h) (esReductionDKSAP g adv b) := by

proof

  unfold hashedDH DiffieHellman.ddhDistAdvantage EntropySmoothing.advantage
    ProbComp.boolDistAdvantage
  rw [probOutput_congr rfl (evalDist_unlinkBranch_dksap_eq_ddhExpReal g h adv b),
    ← probOutput_congr rfl (evalDist_esIdeal_eq_unlinkBranch_dksapIdeal g adv b),
    probOutput_congr rfl (evalDist_ddhExpRand_eq_dksapDHGame g h adv b),
    probOutput_congr rfl (evalDist_dksapDHGame_eq_esReal g h adv b)]
  exact abs_sub_le _ _ _

DKSAP.lean:346-357 ↗

`dksap_unlinkAdvantage_le_ddh_add_es`

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

theorem dksap_unlinkAdvantage_le_ddh_add_es [DecidableEq G]
    (hbij : Function.Bijective (fun x : F => x • g)) :
    (dksap g h).unlinkAdvantage adv ≤
      (DiffieHellman.ddhDistAdvantage g (ddhReductionDKSAP h adv true) +
          EntropySmoothing.advantage F g (fun (_ : Fin 1) => h) (esReductionDKSAP g adv true)) +
        (DiffieHellman.ddhDistAdvantage g (ddhReductionDKSAP h adv false) +
          EntropySmoothing.advantage F g (fun (_ : Fin 1) => h) (esReductionDKSAP g adv false)) :=
  (dksap_unlinkAdvantage_le_hashedDH g h adv hbij).trans
    (add_le_add (hashedDH_le_ddh_add_es g h adv true) (hashedDH_le_ddh_add_es g h adv false))

DKSAP.lean:360-369 ↗