Up-to-Bad Game Kit: Guessing Bound and Value-Carrying Output Games

Protocol-agnostic machinery for oracle-rejection and up-to-bad arguments, on top of the failure-event query bound prBad_induction (Unary/QueryBound).

Main results

• prTrue_uniform_mem / prTrue_uniform_mem_le — a uniform group element lands in a fixed set with probability |S|/|G| (at most n/|G|). The guessing bound behind a q-query union.
• prTrue_bind_le — a bind returns true with probability at most ε when every reachable continuation does (weighted-average bound).
• prEvent_sample_bind — bad-event mass of a uniform sample as the average, over the sampled value, of the continuation's bad mass.
• gameOut / gameOut_apply / gameOut_iub_general — a game whose Bool output is a function F : W → Bool of an arbitrary shared state W. Two such games with outputs agreeing on every non-bad state are identical-until-bad (IdenticalUntilBad), so an up-to-bad advantage bound covers a distinguisher reading any value carried in W, not only a leak indicator.

theorem CatCrypt.Unary.prEvent_sample_bind {G : Type} [Fintype G] [Nonempty G] [DecidableEq G] {β : Type} (k : G → Core.SPComp β) (h₀ : Core.Heap) (E : β → Core.Heap → Prop) : prEvent ((Core.SPComp.sample G).bind k h₀) E = ∑ v : G, (↑(Fintype.card G))⁻¹ * prEvent (k v h₀) E

Bad-event mass of a uniform sample followed by a continuation: the average, over the sampled value, of the continuation's bad-event mass.

Guessing bound

theorem CatCrypt.Unary.prTrue_uniform_mem {G : Type} [Fintype G] [Nonempty G] [DecidableEq G] (S : Finset G) (h₀ : Core.Heap) : Crypto.prTrue ((Core.SPComp.sample G).bind fun (v : G) => Core.SPComp.pure (decide (v ∈ S))) h₀ = ↑S.card / ↑(Fintype.card G)

A uniform group element lands in a fixed set S with probability |S|/|G|.

theorem CatCrypt.Unary.prTrue_uniform_mem_le {G : Type} [Fintype G] [Nonempty G] [DecidableEq G] (S : Finset G) (n : ℕ) (hS : S.card ≤ n) (h₀ : Core.Heap) : Crypto.prTrue ((Core.SPComp.sample G).bind fun (v : G) => Core.SPComp.pure (decide (v ∈ S))) h₀ ≤ ↑n / ↑(Fintype.card G)

A uniform group element lands in a set of size at most n with probability at most n/|G|. The union bound behind a q-query oracle-rejection term.

theorem CatCrypt.Unary.prTrue_bind_le {α : Type} (c : Core.SPComp α) (f : α → Core.SPComp Bool) (h₀ : Core.Heap) (ε : ENNReal) (hf : ∀ (a : α) (h : Core.Heap), (c h₀) (some (a, h)) ≠ 0 → Crypto.prTrue (f a) h ≤ ε) : Crypto.prTrue (c.bind f) h₀ ≤ ε

Weighted-average bind bound: if every reachable continuation returns true with probability at most ε, so does the whole bind.

Value-carrying output games

noncomputable def CatCrypt.Unary.gameOut {W : Type} (shared : Core.SPComp W) (F : W → Bool) : Core.SPComp Bool

A game whose Bool output is a function F of the shared state produced by shared.

Equations

• CatCrypt.Unary.gameOut shared F = shared.bind fun (w : W) => CatCrypt.Core.SPComp.pure (F w)

theorem CatCrypt.Unary.gameOut_apply {W : Type} (shared : Core.SPComp W) (F : W → Bool) (b : Bool) (h h' : Core.Heap) : (gameOut shared F h) (some (b, h')) = ∑' (w : W), (shared h) (some (w, h')) * if F w = b then 1 else 0

Output-apply: the mass on (b, h') is the shared-state mass reaching h' weighted by whether F yields b.

theorem CatCrypt.Unary.gameOut_iub_general {W : Type} (shared : Core.SPComp W) (F₀ F₁ badP : W → Bool) (hFF : ∀ (w : W), badP w = false → F₀ w = F₁ w) : Crypto.BadEvent.IdenticalUntilBad (gameOut shared F₀) (gameOut shared F₁) (gameOut shared badP)

Up-to-bad for arbitrary outputs. Two games with outputs F₀, F₁ agreeing on every non-bad state (badP w = false) are identical-until-bad. F₀/F₁ may read a value carried in W, so this covers a distinguisher using that value, not only the bad indicator.