BlindingROM
Proved: hashAddr ∘ pack as VCVio's lazily sampled randomOracle over
unifSpec + (Bytes →ₒ Addr); the fresh-query lemma (from the empty cache the
announced address is a UNIFORM Addr whatever was hashed — what kills the rho
dependence idealAux_indep_of_t could not remove); blindGameRO_eq; and the
degenerate identical-until-bad case, no address query ⇒ advantage 0.
Proved in addition: identical-until-bad (blindingAdvantageRO_le_blindBadProb),
against VCVio's programming-oracle engine via ROMUpToBad.
Closed downstream: the bound on Pr[bad] (blindBadProb ≤ qH · β) is
BlindingEntropy.blindBadProb_le_queryBound, under a query bound on the
adversary and the point-mass hypothesis BlindPointMassBound.
Assumed / NOT closed: that blindGameRO is auxKeyIndependence after the
mask hop (a standalone abstraction, NOT identified with it here). See
docs/announcement-model.md.
addrSpec
Oracle interface of the ROM model: uniform sampling plus the address hash.
@[reducible] def addrSpec (Bytes Addr : Type) := unifSpec + (Bytes →ₒ Addr)ROMComp
abbrev ROMComp (Bytes Addr : Type) := OracleComp (addrSpec Bytes Addr)hashAddrRO
One address-oracle query: the ROM stand-in for hashAddr (pack …).
def hashAddrRO (x : Bytes) : ROMComp Bytes Addr Addr :=
(addrSpec Bytes Addr).query (Sum.inr x)romImpl
The lazily sampled address oracle, over transparent uniform sampling: the generic
roImpl of ROMUpToBad at the hash spec Bytes →ₒ Addr.
noncomputable def romImpl :
QueryImpl (addrSpec Bytes Addr) (StateT ((Bytes →ₒ Addr).QueryCache) ProbComp) :=
roImpl (Bytes →ₒ Addr)simulateQ_romImpl_liftComp
axioms: propext, Classical.choice, Quot.sound · sorry-free ✓
theorem simulateQ_romImpl_liftComp {β : Type} (ob : ProbComp β) :
simulateQ (romImpl (Bytes := Bytes) (Addr := Addr)) (liftComp ob (addrSpec Bytes Addr)) =
(liftM ob : StateT ((Bytes →ₒ Addr).QueryCache) ProbComp β) := byproof
simp only [romImpl, roImpl, unifFwdImpl, liftComp_eq_liftM, QueryImpl.simulateQ_add_liftM_left,
simulateQ_liftTarget, QueryImpl.simulateQ_toQueryImpl]run_hashAddrRO_empty
axioms: propext, Classical.choice, Quot.sound · sorry-free ✓
theorem run_hashAddrRO_empty {α : Type} (x : Bytes) (f : Addr → ROMComp Bytes Addr α) :
(simulateQ romImpl (hashAddrRO x >>= f)).run ∅ =
(do let a ← ($ᵗ Addr)
(simulateQ romImpl (f a)).run ((∅ : (Bytes →ₒ Addr).QueryCache).cacheQuery x a)) := byproof
simp only [romImpl, roImpl, hashAddrRO, add_apply_inr, simulateQ_bind, simulateQ_query,
OracleQuery.input_query, OracleQuery.cont_query, QueryImpl.add_apply_inr,
QueryImpl.withCaching_apply, uniformSampleImpl, QueryCache.cacheQuery, map_bind, id_map,
bind_assoc, StateT.run_bind, StateT.run_get, pure_bind, QueryCache.empty_apply,
StateT.run_monadLift, monadLift_self, bind_pure_comp, StateT.run_modifyGet, Functor.map_map,
bind_map_left]1. The oracle interface
BlindAdvRO
A ROM adversary against the blinding term: it sees the auxiliary data and may query the address oracle itself.
abbrev BlindAdvRO (Tag Addr Bytes : Type) := Tag × Addr → ROMComp Bytes Addr BoolblindTraceRO
noncomputable def blindTraceRO (P : Prims R Rho Bytes T1 Tag Addr K k l) (tg : Tag)
(rho : Bool → Rho) (t : Bool → (Fin k → R)) (adv : BlindAdvRO Tag Addr Bytes) (b : Bool) :
ProbComp ((Fin k → R) × Bool × (Bytes →ₒ Addr).QueryCache) := do
let u ← ($ᵗ (Fin k → R))
let z ← (simulateQ romImpl
(hashAddrRO (P.pack (rho b) (P.power2Round (u + t b))) >>= fun a => adv (tg, a))).run ∅
pure (u, z)blindGameRO
noncomputable def blindGameRO (P : Prims R Rho Bytes T1 Tag Addr K k l) (tg : Tag)
(rho : Bool → Rho) (t : Bool → (Fin k → R)) (adv : BlindAdvRO Tag Addr Bytes) (b : Bool) :
ProbComp Bool := do
let w ← blindTraceRO P tg rho t adv b
pure w.2.1blindingAdvantageRO
noncomputable def blindingAdvantageRO (P : Prims R Rho Bytes T1 Tag Addr K k l) (tg : Tag)
(rho : Bool → Rho) (t : Bool → (Fin k → R)) (adv : BlindAdvRO Tag Addr Bytes) : ℝ :=
(blindGameRO P tg rho t adv true).boolDistAdvantage (blindGameRO P tg rho t adv false)blindGameRO_eq
axioms: propext, Classical.choice, Quot.sound · sorry-free ✓
theorem blindGameRO_eq (P : Prims R Rho Bytes T1 Tag Addr K k l) (tg : Tag)
(rho : Bool → Rho) (t : Bool → (Fin k → R)) (adv : BlindAdvRO Tag Addr Bytes) (b : Bool) :
blindGameRO P tg rho t adv b =
(do let u ← ($ᵗ (Fin k → R))
let a ← ($ᵗ Addr)
(simulateQ romImpl (adv (tg, a))).run'
((∅ : (Bytes →ₒ Addr).QueryCache).cacheQuery
(P.pack (rho b) (P.power2Round (u + t b))) a)) := byproof
simp only [blindGameRO, blindTraceRO, bind_assoc, pure_bind, run_hashAddrRO_empty]
refine bind_congr fun u => bind_congr fun a => ?_
simp only [StateT.run', map_eq_bind_pure_comp, Function.comp_def, StateT.run]blindingAdvantageRO_eq_zero_of_no_query
axioms: propext, Classical.choice, Quot.sound · sorry-free ✓
theorem blindingAdvantageRO_eq_zero_of_no_query
(P : Prims R Rho Bytes T1 Tag Addr K k l) (tg : Tag)
(rho : Bool → Rho) (t : Bool → (Fin k → R)) (adv : Tag × Addr → ProbComp Bool) :
blindingAdvantageRO P tg rho t (fun x => liftComp (adv x) (addrSpec Bytes Addr)) = 0 := byproof
have key : ∀ b : Bool,
blindGameRO P tg rho t (fun x => liftComp (adv x) (addrSpec Bytes Addr)) b =
(do let _u ← ($ᵗ (Fin k → R)); let a ← ($ᵗ Addr); adv (tg, a)) := by
intro b
simp only [blindGameRO, blindTraceRO, bind_assoc, pure_bind,
run_hashAddrRO_empty, simulateQ_romImpl_liftComp]
refine bind_congr fun _ => bind_congr fun a => ?_
simp only [StateT.run, liftM, monadLift, MonadLift.monadLift, StateT.lift, bind_assoc,
pure_bind, bind_pure]
rw [blindingAdvantageRO, key true, key false, ProbComp.boolDistAdvantage, sub_self, abs_zero]2. The blinding game in the ROM
blindPrefix
The shared prefix of both branches: the mask and the (uniform) announced address.
noncomputable def blindPrefix : ProbComp ((Fin k → R) × Addr) := do
let u ← ($ᵗ (Fin k → R))
let a ← ($ᵗ Addr)
pure (u, a)blindPoint
def blindPoint (P : Prims R Rho Bytes T1 Tag Addr K k l) (rho : Bool → Rho)
(t : Bool → (Fin k → R)) (b : Bool) (x : (Fin k → R) × Addr) : Bytes :=
P.pack (rho b) (P.power2Round (x.1 + t b))blindBadQuery
noncomputable def blindBadQuery (P : Prims R Rho Bytes T1 Tag Addr K k l) (tg : Tag)
(rho : Bool → Rho) (t : Bool → (Fin k → R)) (adv : BlindAdvRO Tag Addr Bytes) (b : Bool) :
ProbComp Bool :=
badQueryGame (blindPrefix (R := R) (k := k) (Addr := Addr)) (fun x => adv (tg, x.2))
(blindPoint P rho t b) (fun x => x.2)blindBadProb
noncomputable def blindBadProb (P : Prims R Rho Bytes T1 Tag Addr K k l) (tg : Tag)
(rho : Bool → Rho) (t : Bool → (Fin k → R)) (adv : BlindAdvRO Tag Addr Bytes) (b : Bool) :
ℝ :=
(Pr[= true | blindBadQuery P tg rho t adv b]).toRealblindGameROFree
noncomputable def blindGameROFree (tg : Tag) (adv : BlindAdvRO Tag Addr Bytes) :
ProbComp Bool :=
blindPrefix (R := R) (k := k) >>= fun x => (simulateQ romImpl (adv (tg, x.2))).run' ∅boolDistAdvantage_blindGameRO_blindGameROFree_le
theorem boolDistAdvantage_blindGameRO_blindGameROFree_le
(P : Prims R Rho Bytes T1 Tag Addr K k l) (tg : Tag)
(rho : Bool → Rho) (t : Bool → (Fin k → R)) (adv : BlindAdvRO Tag Addr Bytes) (b : Bool) :
ProbComp.boolDistAdvantage (blindGameRO P tg rho t adv b)
(blindGameROFree (R := R) (k := k) tg adv) ≤ blindBadProb P tg rho t adv b := byproof
have h := boolDistAdvantage_run'_cacheQuery_run'_empty_le
(blindPrefix (R := R) (k := k) (Addr := Addr)) (fun x => adv (tg, x.2))
(blindPoint P rho t b) (fun x => x.2)
have hgame : blindGameRO P tg rho t adv b =
blindPrefix >>= fun x => (simulateQ (roImpl (Bytes →ₒ Addr)) (adv (tg, x.2))).run'
((∅ : (Bytes →ₒ Addr).QueryCache).cacheQuery (blindPoint P rho t b x) x.2) := by
rw [blindGameRO_eq]
simp only [blindPrefix, blindPoint, romImpl, bind_assoc, pure_bind]
unfold blindBadProb blindBadQuery blindGameROFree
rw [hgame]
exact hblindingAdvantageRO_le_blindBadProb
axioms: propext, Classical.choice, Quot.sound · sorry-free ✓
theorem blindingAdvantageRO_le_blindBadProb (P : Prims R Rho Bytes T1 Tag Addr K k l)
(tg : Tag) (rho : Bool → Rho) (t : Bool → (Fin k → R)) (adv : BlindAdvRO Tag Addr Bytes) :
blindingAdvantageRO P tg rho t adv ≤
blindBadProb P tg rho t adv true + blindBadProb P tg rho t adv false := byproof
unfold blindingAdvantageRO
calc ProbComp.boolDistAdvantage (blindGameRO P tg rho t adv true)
(blindGameRO P tg rho t adv false)
≤ ProbComp.boolDistAdvantage (blindGameRO P tg rho t adv true)
(blindGameROFree (R := R) (k := k) tg adv) +
ProbComp.boolDistAdvantage (blindGameROFree (R := R) (k := k) tg adv)
(blindGameRO P tg rho t adv false) :=
ProbComp.boolDistAdvantage_triangle _ _ _
_ ≤ blindBadProb P tg rho t adv true + blindBadProb P tg rho t adv false := by
gcongr
· exact boolDistAdvantage_blindGameRO_blindGameROFree_le P tg rho t adv true
· rw [ProbComp.boolDistAdvantage_comm]
exact boolDistAdvantage_blindGameRO_blindGameROFree_le P tg rho t adv falsemlweAdvOfBlindAdvRO
The ROM reduction, type-checked. Simulating the address oracle inside,
a ROM blinding adversary is an ordinary seeded-MLWE distinguisher: the challenge
seed becomes recipient 1's rho and the challenge vector the mask.
noncomputable def mlweAdvOfBlindAdvRO (P : Prims R Rho Bytes T1 Tag Addr K k l)
(Smp : Samplers R Rho k l) (tg : Tag) (t : Fin k → R)
(adv : BlindAdvRO Tag Addr Bytes) :
LearningWithErrors.Adversary (blindingProblem P Smp) :=
fun chal =>
(simulateQ romImpl
(hashAddrRO (P.pack chal.1 (P.power2Round (chal.2 + t))) >>=
fun a => adv (tg, a))).run' ∅