DKSAPOracle
Proved: the key-recovery attack as an OracleComp (unifSpec + (G →ₒ F)) making
EXACTLY two oracle queries whatever the number of announcements it is handed
(≤ 2 and not ≤ 1), and its correctness when the oracle is simulated by a
genuine discrete-log function; and, on the positive side, DKSAP restated over
the same interface with the hash as a LAZY RANDOM ORACLE, the idealized RO game
proved perfectly unlinkable, and the RO unlinkability advantage bounded by the
two bad-query probabilities — identical-until-bad closed against VCVio's
programming-oracle engine (ROMUpToBad).
Assumed: the CDH reduction from the bad event is defined (cdhOfUnlinkAdvRO,
logging through VCVio's appendInputLog) but its advantage inequality
dksapROBadProb ≤ q_H · Adv_CDH is open: it needs a query bound on the
adversary and the fact that the flag fires with the same probability in the
programmed and in the tracking run. See the "Oracle attack" and "DDH/ROM bound"
sections of docs/dksap-asymmetry.md.
scalarSpec
Uniform sampling plus one oracle taking a group element to a scalar. VCVio's
+ on specs, so unifSpec ⊂ₒ scalarSpec F G and ProbComp lifts in.
abbrev scalarSpec (F G : Type) : OracleSpec (ℕ ⊕ G) := unifSpec + (G →ₒ F)scalarQuery
def scalarQuery (y : G) : OracleComp (scalarSpec F G) F :=
(scalarSpec F G).query (Sum.inr y)The oracle interface
dlogAttack
The attack on a published meta-address (M, V): two oracle queries, then
recover on every announcement in l. No query depends on l.
def dlogAttack (h : G → F) (MV : G × G) (l : List (G × G)) :
OracleComp (scalarSpec F G) (List F) := do
let xM ← scalarQuery (F := F) MV.1
let xV ← scalarQuery (F := F) MV.2
pure (l.map fun RP => recover h xM xV RP.1)dlogAttack_isTotalQueryBound
axioms: propext, Classical.choice, Quot.sound · sorry-free ✓
theorem dlogAttack_isTotalQueryBound (h : G → F) (MV : G × G) (l : List (G × G)) :
IsTotalQueryBound (dlogAttack h MV l) 2 :=
⟨by norm_num, fun _ => ⟨by norm_num, fun _ => trivial⟩⟩dlogAttack_not_isTotalQueryBound_one
axioms: propext, Classical.choice, Quot.sound · sorry-free ✓
theorem dlogAttack_not_isTotalQueryBound_one (h : G → F) (MV : G × G) (l : List (G × G)) :
¬ IsTotalQueryBound (dlogAttack h MV l) 1 := fun hb =>
absurd (hb.2 (0 : F)).1 (by norm_num)dlogImpl
noncomputable def dlogImpl (dlog : G → F) : QueryImpl (scalarSpec F G) ProbComp
| Sum.inl n => $[0..n]
| Sum.inr y => pure (dlog y)simulateQ_dlogAttack
theorem simulateQ_dlogAttack (dlog : G → F) (h : G → F) (MV : G × G) (l : List (G × G)) :
simulateQ (dlogImpl dlog) (dlogAttack h MV l)
= pure (l.map fun RP => recover h (dlog MV.1) (dlog MV.2) RP.1) := byproof
simp only [dlogAttack, scalarQuery, add_apply_inr, bind_pure_comp, simulateQ_bind,
simulateQ_query, OracleQuery.input_query, OracleQuery.cont_query, dlogImpl, map_pure, id_eq,
simulateQ_map]dksapAnnounce
def dksapAnnounce (g : G) (h : G → F) (m v r : F) : G × G :=
(r • g, (m • g) + (h (r • (v • g))) • g)dksapAnnounce_mem_announce_support
axioms: propext, Classical.choice, Quot.sound · sorry-free ✓
theorem dksapAnnounce_mem_announce_support [SampleableType F] [DecidableEq G]
(g : G) (h : G → F) (m v r : F) :
dksapAnnounce g h m v r ∈ support ((dksap g h).announce (m • g, v • g)) := byproof
simp only [dksap, dksapAnnounce, support_bind, support_pure, Set.mem_iUnion,
Set.mem_singleton_iff, exists_prop]
exact ⟨r, mem_support_uniformSample F, rfl⟩dlogAttack_key_recovery
axioms: propext, Quot.sound · sorry-free ✓
theorem dlogAttack_key_recovery (g : G)
(hinj : Function.Injective (fun x : F => x • g))
(dlog : G → F) (hdlog : ∀ y : G, dlog y • g = y) (h : G → F) (m v : F)
(l : List (G × G)) :
simulateQ (dlogImpl dlog) (dlogAttack h (m • g, v • g) l)
= pure (l.map fun RP => m + h (v • RP.1)) := byproof
rw [simulateQ_dlogAttack]
congr 1
exact List.map_congr_left fun RP _ =>
dksap_recover_eq_honest h g hinj m v _ _ (hdlog (m • g)) (hdlog (v • g)) RP.1dlogAttack_forall_key_recovery
axioms: propext, Quot.sound · sorry-free ✓
theorem dlogAttack_forall_key_recovery (g : G)
(hinj : Function.Injective (fun x : F => x • g))
(dlog : G → F) (hdlog : ∀ y : G, dlog y • g = y) (h : G → F) (m v : F)
(rs : List F) :
List.Forall (fun r : F =>
(recover h (dlog (m • g)) (dlog (v • g)) (r • g)) • g
= (dksapAnnounce g h m v r).2) rs := byproof
rw [List.forall_iff_forall_mem]
exact fun r _ =>
dksap_key_recovery h g hinj m v r _ _ (hdlog (m • g)) (hdlog (v • g))The discrete-log attack, with a real oracle and a query bound
dksapRomImpl
The ROM implementation: uniform queries pass through, hash queries are lazily sampled and cached.
noncomputable def dksapRomImpl (F G : Type) [SampleableType F] [DecidableEq G] :
QueryImpl (scalarSpec F G) (StateT ((G →ₒ F).QueryCache) ProbComp) :=
unifFwdImpl (G →ₒ F) + OracleSpec.randomOracle (spec := (G →ₒ F))dksapRomImpl_eq_roImpl
theorem dksapRomImpl_eq_roImpl : dksapRomImpl F G = roImpl (G →ₒ F) := rfldksapRomImpl_run'_liftM_bind
theorem dksapRomImpl_run'_liftM_bind {α β : Type} (oa : ProbComp α)
(rest : α → StateT ((G →ₒ F).QueryCache) ProbComp β)
(s : (G →ₒ F).QueryCache) :
(simulateQ (dksapRomImpl F G) (liftM oa) >>= rest).run' s
= oa >>= fun x => (rest x).run' s :=
roSim.run'_liftM_bind _ oa rest sdksapRomImpl_run'_scalarQuery_bind
theorem dksapRomImpl_run'_scalarQuery_bind (Z : G)
(rest : F → StateT ((G →ₒ F).QueryCache) ProbComp Bool)
(cache : (G →ₒ F).QueryCache) (hc : cache Z = none) :
(simulateQ (dksapRomImpl F G) (scalarQuery (F := F) Z) >>= rest).run' cache
= ($ᵗ F) >>= fun s => (rest s).run' (QueryCache.cacheQuery cache Z s) := byproof
have hstep : (simulateQ (dksapRomImpl F G) (scalarQuery (F := F) Z) :
StateT ((G →ₒ F).QueryCache) ProbComp F)
= OracleSpec.randomOracle (spec := (G →ₒ F)) Z := by
simp only [dksapRomImpl, scalarQuery, add_apply_inr, simulateQ_query, OracleQuery.input_query,
OracleQuery.cont_query, QueryImpl.add_apply_inr, QueryImpl.withCaching_apply, map_bind, id_map]
rw [hstep]
simp only [StateT.run'_eq]
rw [StateT.run_bind, QueryImpl.withCaching_run_none (m := ProbComp) uniformSampleImpl hc]
simp only [uniformSampleImpl, map_eq_bind_pure_comp, bind_assoc, Function.comp_apply, pure_bind]UnlinkAdvRO
RO-model unlinkability adversary: both meta-addresses, the challenge announcement, and oracle access to the hash.
abbrev UnlinkAdvRO (F G : Type) :=
(G × G) → (G × G) → (G × G) → OracleComp (scalarSpec F G) BooldksapROKeys
Two independent DKSAP recipients, public halves only. No oracle query.
def dksapROKeys (g : G) : ProbComp ((G × G) × (G × G)) := do
let m0 ← ($ᵗ F); let v0 ← ($ᵗ F); let m1 ← ($ᵗ F); let v1 ← ($ᵗ F)
pure (((m0 • g, v0 • g) : G × G), ((m1 • g, v1 • g) : G × G))dksapROSetup
def dksapROSetup (g : G) : OracleComp (scalarSpec F G) ((G × G) × (G × G)) :=
liftM (dksapROKeys F g)advRunAt
noncomputable def advRunAt (adv : UnlinkAdvRO F G) (a : (G × G) × (G × G)) (c : G × G)
(cache : (G →ₒ F).QueryCache) : ProbComp Bool :=
(simulateQ (dksapRomImpl F G) (adv a.1 a.2 c)).run' cachedksapROBranch
def dksapROBranch (g : G) (adv : UnlinkAdvRO F G) (b : Bool)
(a : (G × G) × (G × G)) : OracleComp (scalarSpec F G) Bool := do
let r ← liftM ($ᵗ F)
let s ← scalarQuery (F := F) (r • (if b then a.2 else a.1).2)
adv a.1 a.2 (r • g, (if b then a.2 else a.1).1 + s • g)dksapROIdealBranch
def dksapROIdealBranch (g : G) (adv : UnlinkAdvRO F G) (b : Bool)
(a : (G × G) × (G × G)) : OracleComp (scalarSpec F G) Bool := do
let r ← liftM ($ᵗ F)
let s ← liftM ($ᵗ F)
adv a.1 a.2 (r • g, (if b then a.2 else a.1).1 + s • g)dksapRORun
noncomputable def dksapRORun (g : G) (adv : UnlinkAdvRO F G) (b : Bool) : ProbComp Bool :=
(simulateQ (dksapRomImpl F G) (dksapROSetup g >>= dksapROBranch g adv b)).run' ∅dksapROIdealRun
noncomputable def dksapROIdealRun (g : G) (adv : UnlinkAdvRO F G) (b : Bool) : ProbComp Bool :=
(simulateQ (dksapRomImpl F G) (dksapROSetup g >>= dksapROIdealBranch g adv b)).run' ∅dksapROIdealRun_eq
Peeling: keygen and the two scalars are ordinary sampling, so the ideal game is the adversary run on an announcement built from a uniform scalar.
theorem dksapROIdealRun_eq (g : G) (adv : UnlinkAdvRO F G) (b : Bool) :
dksapROIdealRun g adv b =
dksapROKeys F g >>= fun a => ($ᵗ F) >>= fun r => ($ᵗ F) >>= fun s =>
advRunAt adv a (r • g, (if b then a.2 else a.1).1 + s • g) ∅ := byproof
unfold dksapROIdealRun dksapROSetup dksapROIdealBranch advRunAt
simp only [simulateQ_bind]
rw [dksapRomImpl_run'_liftM_bind]
refine bind_congr fun a => ?_
rw [dksapRomImpl_run'_liftM_bind]
refine bind_congr fun r => ?_
rw [dksapRomImpl_run'_liftM_bind]dksapROIdeal_boolDistAdvantage_eq_zero
axioms: propext, Classical.choice, Quot.sound · sorry-free ✓
theorem dksapROIdeal_boolDistAdvantage_eq_zero (g : G) (adv : UnlinkAdvRO F G)
(hbij : Function.Bijective (fun x : F => x • g)) :
(dksapROIdealRun g adv true).boolDistAdvantage (dksapROIdealRun g adv false) = 0 := byproof
rw [ProbComp.boolDistAdvantage]
refine abs_eq_zero.mpr (sub_eq_zero.mpr ?_)
congr 1
rw [dksapROIdealRun_eq, dksapROIdealRun_eq, probOutput_bind_eq_tsum,
probOutput_bind_eq_tsum]
refine tsum_congr fun a => ?_
congr 1
simp only [if_true, Bool.false_eq_true, if_false]
exact dksapIdeal_branch_indep g hbij a.1.1 a.2.1 (fun c => advRunAt adv a c ∅) trueunlinkAdvantageRO
Unlinkability advantage of DKSAP in the random-oracle model.
noncomputable def unlinkAdvantageRO (g : G) (adv : UnlinkAdvRO F G) : ℝ :=
(dksapRORun g adv true).boolDistAdvantage (dksapRORun g adv false)hashedDHRO
noncomputable def hashedDHRO (g : G) (adv : UnlinkAdvRO F G) (b : Bool) : ℝ :=
(dksapRORun g adv b).boolDistAdvantage (dksapROIdealRun g adv b)dksap_unlinkAdvantageRO_le_hashedDHRO
axioms: propext, Classical.choice, Quot.sound · sorry-free ✓
theorem dksap_unlinkAdvantageRO_le_hashedDHRO (g : G) (adv : UnlinkAdvRO F G)
(hbij : Function.Bijective (fun x : F => x • g)) :
unlinkAdvantageRO g adv ≤ hashedDHRO g adv true + hashedDHRO g adv false := byproof
unfold unlinkAdvantageRO hashedDHRO
rw [ProbComp.boolDistAdvantage_comm (dksapRORun g adv false)]
calc (dksapRORun g adv true).boolDistAdvantage (dksapRORun g adv false)
≤ (dksapRORun g adv true).boolDistAdvantage (dksapROIdealRun g adv true) +
(dksapROIdealRun g adv true).boolDistAdvantage (dksapRORun g adv false) :=
ProbComp.boolDistAdvantage_triangle _ _ _
_ ≤ (dksapRORun g adv true).boolDistAdvantage (dksapROIdealRun g adv true) +
((dksapROIdealRun g adv true).boolDistAdvantage (dksapROIdealRun g adv false) +
(dksapROIdealRun g adv false).boolDistAdvantage (dksapRORun g adv false)) := by
gcongr
exact ProbComp.boolDistAdvantage_triangle _ _ _
_ = _ := by rw [dksapROIdeal_boolDistAdvantage_eq_zero g adv hbij, zero_add]dksapRORun_eq
The real game is the ideal game run against a cache already programmed at the DH point: the announce query is the first one, so it hits an empty cache.
axioms: propext, Classical.choice, Quot.sound · sorry-free ✓
theorem dksapRORun_eq (g : G) (adv : UnlinkAdvRO F G) (b : Bool) :
dksapRORun g adv b =
dksapROKeys F g >>= fun a => ($ᵗ F) >>= fun r => ($ᵗ F) >>= fun s =>
advRunAt adv a (r • g, (if b then a.2 else a.1).1 + s • g)
(QueryCache.cacheQuery ∅ (r • (if b then a.2 else a.1).2) s) := byproof
unfold dksapRORun dksapROSetup dksapROBranch advRunAt
simp only [simulateQ_bind]
rw [dksapRomImpl_run'_liftM_bind]
refine bind_congr fun a => ?_
rw [dksapRomImpl_run'_liftM_bind]
refine bind_congr fun r => ?_
exact dksapRomImpl_run'_scalarQuery_bind _ _ ∅ rfldksapROPrefix
def dksapROPrefix (g : G) : ProbComp (((G × G) × (G × G)) × F × F) :=
dksapROKeys F g >>= fun a => ($ᵗ F) >>= fun r => ($ᵗ F) >>= fun s => pure (a, r, s)dksapROAdvRun
def dksapROAdvRun (g : G) (adv : UnlinkAdvRO F G) (b : Bool)
(x : ((G × G) × (G × G)) × F × F) : OracleComp (scalarSpec F G) Bool :=
adv x.1.1 x.1.2 (x.2.1 • g, (if b then x.1.2 else x.1.1).1 + x.2.2 • g)dksapRODHPoint
def dksapRODHPoint (b : Bool) (x : ((G × G) × (G × G)) × F × F) : G :=
x.2.1 • (if b then x.1.2 else x.1.1).2dksapROBad
noncomputable def dksapROBad (g : G) (adv : UnlinkAdvRO F G) (b : Bool) : ProbComp Bool :=
badQueryGame (dksapROPrefix g) (dksapROAdvRun g adv b) (dksapRODHPoint b) (fun x => x.2.2)dksapROBadProb
noncomputable def dksapROBadProb (g : G) (adv : UnlinkAdvRO F G) (b : Bool) : ℝ :=
(Pr[= true | dksapROBad g adv b]).toRealhashedDHRO_le_dksapROBadProb
axioms: propext, Classical.choice, Quot.sound · sorry-free ✓
theorem hashedDHRO_le_dksapROBadProb (g : G) (adv : UnlinkAdvRO F G) (b : Bool) :
hashedDHRO g adv b ≤ dksapROBadProb g adv b := byproof
have h := boolDistAdvantage_run'_cacheQuery_run'_empty_le (dksapROPrefix g)
(dksapROAdvRun g adv b) (dksapRODHPoint b) (fun x => x.2.2)
have hreal : dksapRORun g adv b =
dksapROPrefix g >>= fun x => (simulateQ (roImpl (G →ₒ F)) (dksapROAdvRun g adv b x)).run'
((∅ : (G →ₒ F).QueryCache).cacheQuery (dksapRODHPoint b x) x.2.2) := by
rw [dksapRORun_eq]
simp only [dksapROPrefix, dksapROAdvRun, dksapRODHPoint, advRunAt, dksapRomImpl_eq_roImpl,
bind_assoc, pure_bind]
have hideal : dksapROIdealRun g adv b =
dksapROPrefix g >>= fun x =>
(simulateQ (roImpl (G →ₒ F)) (dksapROAdvRun g adv b x)).run' ∅ := by
rw [dksapROIdealRun_eq]
simp only [dksapROPrefix, dksapROAdvRun, advRunAt, dksapRomImpl_eq_roImpl, bind_assoc, pure_bind]
unfold hashedDHRO dksapROBadProb dksapROBad
rw [hreal, hideal]
exact hdksap_unlinkAdvantageRO_le_badProb
axioms: propext, Classical.choice, Quot.sound · sorry-free ✓
theorem dksap_unlinkAdvantageRO_le_badProb (g : G) (adv : UnlinkAdvRO F G)
(hbij : Function.Bijective (fun x : F => x • g)) :
unlinkAdvantageRO g adv ≤ dksapROBadProb g adv true + dksapROBadProb g adv false :=
(dksap_unlinkAdvantageRO_le_hashedDHRO g adv hbij).trans
(add_le_add (hashedDHRO_le_dksapROBadProb g adv true)
(hashedDHRO_le_dksapROBadProb g adv false))loggingROImpl
A random oracle that also logs the queried points, so the reduction can
return one of them: VCVio's appendInputLog (a preInsert) over the lazy
random oracle, with uniform queries forwarded.
noncomputable def loggingROImpl (F G : Type) [SampleableType F] [DecidableEq G] :
QueryImpl (scalarSpec F G)
(StateT (List G) (StateT ((G →ₒ F).QueryCache) ProbComp)) :=
(HasQuery.toQueryImpl (spec := unifSpec) (m := ProbComp)).liftTarget
(StateT (List G) (StateT ((G →ₒ F).QueryCache) ProbComp)) +
QueryImpl.appendInputLog (OracleSpec.randomOracle (spec := (G →ₒ F)))cdhOfUnlinkAdvRO
noncomputable def cdhOfUnlinkAdvRO (adv : UnlinkAdvRO F G) (b : Bool) :
DiffieHellman.CDHAdversary F G := fun g A B => do
let mT ← ($ᵗ F); let mO ← ($ᵗ F); let vO ← ($ᵗ F); let s ← ($ᵗ F)
let pkT : G × G := (mT • g, B)
let pkO : G × G := (mO • g, vO • g)
let z ← ((simulateQ (loggingROImpl F G)
(adv (if b then pkO else pkT) (if b then pkT else pkO) (A, mT • g + s • g))).run []).run' ∅
let i ← ($[0..z.2.length - 1])
pure (z.2.getD i.val 0)