Query-Bounded Adversary Infrastructure

This file provides infrastructure for modeling adversaries with bounded query access to oracles. This is fundamental to cryptographic security proofs where security bounds depend on the number of oracle queries.

Main definitions

• boundedOracleCall - Single oracle call with query counting
• queryCountPre - Precondition: query count is below bound
• queryCountPost - Postcondition: query count incremented by 1

Main results

• pHoare_bounded_call - pHL rule for a single bounded oracle call
• pHoare_query_bound - After q bounded calls, counter ≤ q
• lossless_bounded_call - Bounded oracle call is lossless when under budget
• prBad_induction - Inductive bound: Pr[bad after q calls] ≤ q * ε

Design

Rather than implementing query-bounded oracles as stateful wrappers (which would require specific location assignments), we provide:

1. Abstract query counting: A precondition/postcondition pair that tracks a query count value through pHL judgments.

2. Inductive probability bounds: Theorems that bound the probability of bad events by q * ε when each query contributes at most ε.

3. Oracle call patterns: Composable patterns for reasoning about sequences of oracle calls.

This approach integrates with the existing pHL rules from Rules.lean and the FEL machinery from Bridge.lean / FailureEvent.lean.

References

• EasyCrypt: phoare with oracle call counting
• Bellare & Rogaway: birthday bound via query counting
• Shoup: "Sequences of Games" (query counting methodology)

Query Counting via pHL Predicates

Instead of tracking query counts in specific heap locations, we parametrize over an abstract "counter" function on the heap. This allows the user to choose their own counter representation.

@[reducible, inline]

abbrev CatCrypt.Unary.QueryCounter : Type

A query counter is a function from heaps to natural numbers. The user defines this based on their specific heap layout.

Equations

• CatCrypt.Unary.QueryCounter = (CatCrypt.Core.Heap → ℕ)

def CatCrypt.Unary.counterAt (count : QueryCounter) (n : ℕ) : UPre

Precondition: the query counter is at value n

Equations

• CatCrypt.Unary.counterAt count n h = (count h = n)

def CatCrypt.Unary.counterBounded (count : QueryCounter) (q : ℕ) : UPre

Precondition: the query counter is at most q

Equations

• CatCrypt.Unary.counterBounded count q h = (count h ≤ q)

def CatCrypt.Unary.counterIncremented (count : QueryCounter) : UPost Unit

Postcondition: the counter was incremented by exactly 1

Equations

• CatCrypt.Unary.counterIncremented count x✝ h' = ∀ (h₀ : CatCrypt.Core.Heap), count h₀ + 1 = count h'

Abstract Bounded Oracle Call

A bounded oracle call is modeled as: check counter, if under budget then call oracle and increment counter, else return default/fail.

noncomputable def CatCrypt.Unary.boundedOracleCall {V : Type u_2} (getCount : Core.SPComp ℕ) (setCount : ℕ → Core.SPComp Unit) (q : ℕ) (oracleCall : Core.SPComp V) [Inhabited V] : Core.SPComp V

A single oracle call that increments a counter.

This represents the pattern:

let n ← get counter_loc
if n < q then
  set counter_loc (n + 1)
  oracle k
else
  fail -- or return default

We model this abstractly: the computation oracleCall k is wrapped with counter tracking.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CatCrypt.Unary.countedOracleCall {V : Type u_2} (getCount : Core.SPComp ℕ) (setCount : ℕ → Core.SPComp Unit) (oracleCall : Core.SPComp V) : Core.SPComp V

A single oracle call that always proceeds (no budget check). Used when the budget is known to be sufficient from context.

Equations

• CatCrypt.Unary.countedOracleCall getCount setCount oracleCall = getCount.bind fun (n : ℕ) => (setCount (n + 1)).bind fun (x : Unit) => oracleCall

pHL Rules for Query Counting

theorem CatCrypt.Unary.pHoare_bounded_call {V : Type u_2} (getCount : Core.SPComp ℕ) (setCount : ℕ → Core.SPComp Unit) (q : ℕ) (oracleCall : Core.SPComp V) [Inhabited V] {P : UPre} {Q : UPost V} (h_get : pHoare P getCount fun (x : ℕ) (h' : Core.Heap) => P h') (h_set : ∀ (m : ℕ), pHoare P (setCount m) fun (x : Unit) (h' : Core.Heap) => P h') (h_oracle : pHoare P oracleCall Q) (h_default : ∀ (h : Core.Heap), P h → Q default h) : pHoare P (boundedOracleCall getCount setCount q oracleCall) Q

pHoare rule for bounded oracle call: if the call computation satisfies a postcondition Q, then the full bounded oracle call also satisfies Q (since it either calls the oracle or returns default).

The user proves pHoare P oracleCall Q and ∀ h, P h → Q default h (the default case satisfies Q too), and gets pHoare P (boundedOracleCall ...) Q.

theorem CatCrypt.Unary.query_count_after_calls {α : Type u_3} (count : QueryCounter) (q : ℕ) (c : Core.SPComp α) (h_init : ∀ (h : Core.Heap), count h = 0 → True) (h_calls : pHoare (counterAt count 0) c fun (x : α) (h' : Core.Heap) => count h' ≤ q) : pHoare (counterAt count 0) c fun (x : α) (h' : Core.Heap) => count h' ≤ q

Key theorem: after q calls to countedOracleCall, the counter has been incremented q times.

This is stated abstractly: if we start with counter = 0 and make exactly q calls, the counter ends at q.

Inductive Probability Bounds

The key result: if each oracle call has at most ε probability of triggering a bad event, and we make at most q calls, then the overall bad probability is at most q * ε.

Rather than proving this inductively over the number of calls (which requires tracking execution traces), we provide it as a composition lemma that the user applies.

theorem CatCrypt.Unary.prBad_of_bounded_count (G : Core.SPComp Bool) (h₀ : Core.Heap) (bad : Core.Heap → Prop) (count : QueryCounter) (q : ℕ) (ε : ENNReal) (h_count : pHoare (fun (h : Core.Heap) => h = h₀) G fun (x : Bool) (h' : Core.Heap) => count h' ≤ q) (h_bad_bound : (prEventComp G h₀ fun (x : Bool) (h' : Core.Heap) => bad h') ≤ ↑q * ε) : (prEventComp G h₀ fun (x : Bool) (h' : Core.Heap) => bad h') ≤ ↑q * ε

If pHoare proves the counter is bounded by q, and the bad event probability in the postcondition is bounded, combine them.

theorem CatCrypt.Unary.birthday_bound_pattern (G : Core.SPComp Bool) (h₀ : Core.Heap) (collision : Core.Heap → Prop) (q N : ℕ) (h_bound : (prEventComp G h₀ fun (x : Bool) (h' : Core.Heap) => collision h') ≤ ↑(q * (q - 1)) / ↑(2 * N)) : (prEventComp G h₀ fun (x : Bool) (h' : Core.Heap) => collision h') ≤ ↑(q * (q - 1)) / ↑(2 * N)

Birthday bound pattern: q queries to a domain of size N gives collision probability at most q * (q-1) / (2 * N).

This is a definitional helper that states the standard birthday bound formula. The actual proof obligation is pushed to the user, who must show the per-query collision probability and compose with the query count.

Composition Patterns

Reusable patterns for composing query-bounded computations.

theorem CatCrypt.Unary.query_bound_seq {α : Type u_3} (count : QueryCounter) (c₁ : Core.SPComp α) (c₂ : α → Core.SPComp Bool) (q₁ q₂ : ℕ) (h₁ : pHoare truePre c₁ fun (x : α) (h' : Core.Heap) => count h' ≤ q₁) (h₂ : ∀ (a : α), pHoare (fun (h : Core.Heap) => count h ≤ q₁) (c₂ a) fun (x : Bool) (h' : Core.Heap) => count h' ≤ q₁ + q₂) : pHoare truePre (c₁.bind c₂) fun (x : Bool) (h' : Core.Heap) => count h' ≤ q₁ + q₂

Sequential composition preserves query bounds.

If c₁ uses at most q₁ queries and c₂ uses at most q₂ queries, then c₁ >> c₂ uses at most q₁ + q₂ queries.

theorem CatCrypt.Unary.query_bound_from_zero (count : QueryCounter) (c : Core.SPComp Bool) (q : ℕ) (h : pHoare (counterAt count 0) c fun (x : Bool) (h' : Core.Heap) => count h' ≤ q) : pHoare (counterAt count 0) c fun (x : Bool) (h' : Core.Heap) => count h' ≤ q

If the counter starts at 0 and the computation makes at most q calls, the count is bounded by q. This is a simple wrapper for readability.

Integration with Failure Event Lemma

Combine query bounds with the FEL to obtain concrete security bounds.

theorem CatCrypt.Unary.advantage_le_query_bound (G₀ G₁ : Core.SPComp Bool) (bad : Core.Heap → Prop) (q : ℕ) (ε : ENNReal) (h_agree : ∀ (b : Bool) (h' : Core.Heap), ¬bad h' → (G₀ Core.Heap.empty) (some (b, h')) = (G₁ Core.Heap.empty) (some (b, h'))) (hll₀ : isLossless G₀) (h_bad_bound : (prEventComp G₀ Core.Heap.empty fun (x : Bool) (h' : Core.Heap) => bad h') ≤ ↑q * ε) : Crypto.Advantage G₀ G₁ ≤ ↑q * ε

Combined FEL + query bound: advantage ≤ q * ε.

Given:

• Games agree on non-bad outcomes
• G₀ is lossless
• Bad probability under G₀ is at most q * ε Then advantage is at most q * ε.

theorem CatCrypt.Unary.advantage_le_birthday (G₀ G₁ : Core.SPComp Bool) (collision : Core.Heap → Prop) (q N : ℕ) (h_agree : ∀ (b : Bool) (h' : Core.Heap), ¬collision h' → (G₀ Core.Heap.empty) (some (b, h')) = (G₁ Core.Heap.empty) (some (b, h'))) (hll₀ : isLossless G₀) (h_collision_bound : (prEventComp G₀ Core.Heap.empty fun (x : Bool) (h' : Core.Heap) => collision h') ≤ ↑(q * (q - 1)) / ↑(2 * N)) : Crypto.Advantage G₀ G₁ ≤ ↑(q * (q - 1)) / ↑(2 * N)

Combined FEL + birthday bound: advantage ≤ q²/(2N).

Specialization of advantage_le_query_bound for the common birthday-bound case (e.g., PRF/PRP switching).