Games
Proved: StealthScheme as an abstract randomized algorithm over VCVio's
ProbComp (mirroring its own AsymmEncAlg idiom); detection completeness and
the false-positive experiment; unlinkability -- recipient anonymity -- as a
hidden-bit game, and the first hop, unlinkAdvantage_eq_branchDistAdvantage:
the advantage IS the advantage of distinguishing an announcement to recipient 1
from one to recipient 0.
Assumed: nothing. The hidden bit selects the RECIPIENT, not the message, so
this is key privacy, not IND-CPA. See docs/announcement-model.md.
ProbComp.boolBiasAdvantage_bind_uniformBool_branch
Bias of a hidden-bit guessing game whose branch is selected by the bit:
the distinguishing advantage between the two branches. (Scoped under PqStealth
so a future upstream lemma of the same name cannot clash; upstream candidate,
see docs/vcvio-upstream.md.)
theorem ProbComp.boolBiasAdvantage_bind_uniformBool_branch {α : Type} (pref : ProbComp α)
(branch : Bool → α → ProbComp Bool) :
(do
let a ← pref
let b ← ($ᵗ Bool)
let z ← branch b a
pure (b == z)).boolBiasAdvantage
= (pref >>= branch true).boolDistAdvantage (pref >>= branch false) := byproof
have h : (do let a ← pref; let b ← ($ᵗ Bool); let z ← branch b a; pure (b == z))
= (do
let a ← pref
let b ← ($ᵗ Bool)
let z ← if b then branch true a else branch false a
pure (b == z)) :=
bind_congr fun a => bind_congr fun b => by cases b <;> rfl
rw [h]
exact ProbComp.boolBiasAdvantage_bind_uniformBool_eq_boolDistAdvantage pref
(branch true) (branch false)ProbComp.boolDistAdvantage_comm
theorem ProbComp.boolDistAdvantage_comm (p q : ProbComp Bool) :
p.boolDistAdvantage q = q.boolDistAdvantage p :=
abs_sub_comm _ _Hidden-bit games with a bit-indexed branch
StealthScheme
A stealth address scheme: key generation, sender-side announcing, and recipient-side detection, all as probabilistic computations.
structure StealthScheme (MetaPub MetaPriv Announcement : Type) where
/-- Recipient key generation: a meta-address and its private counterpart. -/
keygen : ProbComp (MetaPub × MetaPriv)
/-- Sender side: publish an announcement for a recipient's meta-address. -/
announce : MetaPub → ProbComp Announcement
/-- Recipient side: decide whether an announcement is addressed to us. -/
scan : MetaPriv → Announcement → ProbComp BoolThe scheme as an abstract randomized algorithm
CorrectExp
Completeness experiment: announce to a freshly generated recipient, then
scan with that recipient's secret; should return true.
def CorrectExp : ProbComp Bool := do
let (pk, sk) ← S.keygen
let c ← S.announce pk
S.scan sk cPerfectlyComplete
def PerfectlyComplete : Prop := Pr[= true | S.CorrectExp] = 1Detection completeness
FalsePositiveExp
False-positive experiment: two independent recipients, an announcement
addressed to the second, scanned with the first one's private state. true is a
false positive.
def FalsePositiveExp : ProbComp Bool := do
let (_, sk0) ← S.keygen
let (pk1, _) ← S.keygen
let c ← S.announce pk1
S.scan sk0 cfalsePositiveRate
noncomputable def falsePositiveRate : ℝ := (Pr[= true | S.FalsePositiveExp]).toRealSoundWithin
def SoundWithin (ε : ℝ) : Prop := S.falsePositiveRate ≤ εThe false-positive experiment
UnlinkAdv
Unlinkability adversary: given both public meta-addresses and the challenge
announcement, guess which recipient it is for. A function rather than a
two-phase structure — the games are non-adaptive (docs/announcement-model.md).
abbrev UnlinkAdv (MetaPub Announcement : Type) :=
MetaPub → MetaPub → Announcement → ProbComp BoolunlinkSetup
def unlinkSetup : ProbComp (MetaPub × MetaPub) := do
let (pk0, _) ← S.keygen
let (pk1, _) ← S.keygen
pure (pk0, pk1)unlinkBranch
The branch of the unlinkability game selected by the hidden bit: the
challenge announcement goes to recipient b.
def unlinkBranch (b : Bool) (a : MetaPub × MetaPub) : ProbComp Bool := do
let c ← S.announce (if b then a.2 else a.1)
adv a.1 a.2 cUnlinkExp
def UnlinkExp : ProbComp Bool := do
let a ← S.unlinkSetup
let b ← ($ᵗ Bool)
let z ← S.unlinkBranch adv b a
pure (b == z)unlinkAdvantage
noncomputable def unlinkAdvantage : ℝ := (S.UnlinkExp adv).boolBiasAdvantageunlinkAdvantage_eq_branchDistAdvantage
axioms: propext, Classical.choice, Quot.sound · sorry-free ✓
theorem unlinkAdvantage_eq_branchDistAdvantage :
S.unlinkAdvantage adv =
(S.unlinkSetup >>= S.unlinkBranch adv true).boolDistAdvantage
(S.unlinkSetup >>= S.unlinkBranch adv false) :=
ProbComp.boolBiasAdvantage_bind_uniformBool_branch S.unlinkSetup (S.unlinkBranch adv)