Collision resistance of the random oracle

A 101-crypto example exercising the framework. We define the standard collision-resistance game (cr_experiment) parameterised by a query budget q, an init step, and a query step. Two flavours are then obtained by plugging in lazy_* or random_oracle_* (= eager) primitives.

The high-level claims are:

• cr_transfer — the collision probability is identical under lazy and eager random oracle (proved via oracle_loop_wp_lazy_eq_random_oracle).
• cr_lazy_bound — the lazy collision probability is bounded by the birthday bound (q+2)(q+1) / (2 · |output|) (the +2 accounts for the final two collision-check queries).
• cr_eager_bound — the same bound for eager, by cr_transfer.

All results below are fully proved (no sorry): the transfer via the ProgramDenotation.transfer framework, and the birthday bound by a unary wp-expectation induction.

axiom claim_x : Variable input

The CR adversary's two collision claims, stored in state.

axiom claim_x' : Variable input

axiom disjoint_claim_x_ro : GaudisCrypt.disjoint claim_x random_oracle_state

Disjointness: the claim variables don't alias the RO state.

axiom disjoint_claim_x'_ro : GaudisCrypt.disjoint claim_x' random_oracle_state

@[implicit_reducible]

noncomputable instance instDecidableEqOutput_1 : DecidableEq output

Output equality needed for the collision check. We get it for free from classical logic (the rest of the file is noncomputable anyway).

Equations

• instDecidableEqOutput_1 = Classical.decEq output

CR experiment parameterised over an adversary

cr_adv is a parameter (via the variable declaration below), not an axiom. Every cr_experiment-, cr_lazy_bound-, cr_transfer-style definition and theorem in this section takes an arbitrary CR adversary cr_adv : ProgramDenotation state Unit together with h_cr_adv : cr_adv.inFootprint ....

The adversary may set oracle_input (queried each round), may set claim_x and claim_x' (its candidate collision), and may not touch random_oracle_state directly.

noncomputable def cr_loop_body (cr_adv : GaudisCrypt.ProgramDenotation state Unit) (oracle : input → GaudisCrypt.ProgramDenotation state output) : GaudisCrypt.ProgramDenotation state Unit

One round of the CR loop body: the adversary computes, then we run one query on whatever cr_adv placed in oracle_input. Thin alias for the generic oracle_step in RO.lean.

Equations

• cr_loop_body cr_adv oracle = oracle_step cr_adv oracle

noncomputable def cr_loop (cr_adv : GaudisCrypt.ProgramDenotation state Unit) (q : ℕ) (oracle : input → GaudisCrypt.ProgramDenotation state output) : GaudisCrypt.ProgramDenotation state Unit

Run the adversary-and-query loop for q rounds. Thin alias for the generic oracle_loop_n in RO.lean.

Equations

• cr_loop cr_adv q oracle = oracle_loop_n cr_adv q oracle

noncomputable def cr_experiment (cr_adv : GaudisCrypt.ProgramDenotation state Unit) (q : ℕ) (init : GaudisCrypt.ProgramDenotation state Unit) (oracle : input → GaudisCrypt.ProgramDenotation state output) : GaudisCrypt.ProgramDenotation state Bool

The CR experiment parameterised by query budget q, init, and oracle.

Run the adversary for q rounds, then read its claim (x, x'), query the oracle at both, and report whether (x ≠ x') ∧ (y = y').

Equations

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

Phase 2 — Transfer (lazy = eager)

The output of cr_experiment is RO-invariant (it only depends on state variables disjoint from random_oracle_state), so the dist of the result bit agrees under lazy and eager RO.

Building blocks for cr_transfer via the ProgramDenotation.transfer framework.

theorem cr_transfer (cr_adv : GaudisCrypt.ProgramDenotation state Unit) (h_cr_adv : cr_adv.inFootprint (GaudisCrypt.Lens.footprint random_oracle_state)ᶜ) (q : ℕ) (σ₀ : state) : (do let bσ ← cr_experiment cr_adv q lazy_init lazy_query σ₀ pure bσ.1) = do let bσ ← cr_experiment cr_adv q random_oracle_init random_oracle_query σ₀ pure bσ.1

Transfer theorem: The marginal distribution of the result bit is identical under lazy and eager random oracle.

Phase 3 — Birthday bound on the lazy CR experiment

The proof is decomposed into helper lemmas and a top-level composition. The composition cr_lazy_bound itself is proved — no sorry — modulo the two helpers.

• cr_true_implies_collision_wp (bookkeeping): if the experiment's result bit is true, then the final state has a collision. This is a structural / support-analysis fact: cr_experiment writes lazy_query x and lazy_query x' into the RO table before returning decide (x ≠ x' ∧ y = y'), so a true return implies RO[x] = RO[x'] = some y with x ≠ x'.

• cr_collision_birthday_bound (the real probability work): the expected collision indicator is bounded by (q+2)(q+1) / (2·N). This is the actual birthday argument — a union bound over pairs of distinct queried inputs, each pair colliding with probability ≤ 1/N because lazy_query yields uniform fresh samples.

def has_collision (σ : state) : Prop

A state has a "collision": two distinct inputs both have cached RO values, and those cached values are equal.

Equations

• has_collision σ = ∃ (x : input) (x' : input), x ≠ x' ∧ ∃ (y : output), random_oracle_state.get σ x = some y ∧ random_oracle_state.get σ x' = some y

@[implicit_reducible]

noncomputable instance instDecidablePredStateHas_collision : DecidablePred has_collision

Equations

• instDecidablePredStateHas_collision x✝ = Classical.propDecidable (has_collision x✝)

noncomputable def collision_indicator (σ : state) : ENNReal

0/1-valued collision indicator on state.

Equations

• collision_indicator σ = if has_collision σ then 1 else 0

Helper: lazy_query postcondition strengthening

theorem lazy_query_wp_strengthen {x : input} {σ : state} {I : output → state → Prop} [DecidablePred fun (yσ : output × state) => I yσ.1 yσ.2] (h_cache : ∀ (y_cache : output), random_oracle_state.get σ x = some y_cache → I y_cache σ) (h_fresh : ∀ (value : output), random_oracle_state.get σ x = none → I value (random_oracle_state.set (fun (x' : input) => if x' = x then some value else random_oracle_state.get σ x') σ)) (F : output × state → ENNReal) : (lazy_query x).wp F σ = (lazy_query x).wp (fun (yσ : output × state) => if I yσ.1 yσ.2 then F yσ else 0) σ

lazy_query support strengthening: if an invariant I : output → state → Prop holds at every state reachable from lazy_query x σ — namely, on the cached output (when the entry is cached) and on every fresh-sample post-state (when not cached) — then strengthening the postcondition with if I then F else 0 leaves the wp value unchanged.

theorem lazy_query_wp_writes_output (x : input) (F : output × state → ENNReal) (σ : state) : (lazy_query x).wp F σ = (lazy_query x).wp (fun (yσ : output × state) => if random_oracle_state.get yσ.2 x = some yσ.1 then F yσ else 0) σ

lazy_query writes its output: integrating any F against lazy_query x σ is the same as integrating F restricted to states where RO[x] = some (returned y).

theorem lazy_query_wp_preserves_disjoint {α : Type} [DecidableEq α] (v : Variable α) [GaudisCrypt.disjoint v random_oracle_state] (x : input) (F : output × state → ENNReal) (σ : state) : (lazy_query x).wp F σ = (lazy_query x).wp (fun (yσ : output × state) => if v.get yσ.2 = v.get σ then F yσ else 0) σ

lazy_query preserves disjoint state: querying doesn't change the value of any variable disjoint from random_oracle_state.

theorem lazy_query_wp_preserves_other_RO (x x' : input) (h_neq : x' ≠ x) (F : output × state → ENNReal) (σ : state) : (lazy_query x).wp F σ = (lazy_query x).wp (fun (yσ : output × state) => if random_oracle_state.get yσ.2 x' = random_oracle_state.get σ x' then F yσ else 0) σ

lazy_query preserves other RO entries: querying x doesn't change RO[x'] for x' ≠ x.

theorem cr_true_implies_collision_wp (cr_adv : GaudisCrypt.ProgramDenotation state Unit) (q : ℕ) (σ₀ : state) : (cr_experiment cr_adv q lazy_init lazy_query).wp (fun (bσ : Bool × state) => if bσ.1 = true then 1 else 0) σ₀ ≤ (cr_experiment cr_adv q lazy_init lazy_query).wp (fun (bσ : Bool × state) => collision_indicator bσ.2) σ₀

Bookkeeping helper: at every state in the support of cr_experiment cr_adv q lazy_init lazy_query, if the result bit is true then the state has a collision. Stated at the wp level so it composes with the birthday bound below.

Proof plan (~80-100 lines; helpers all in place):

1. Goal after simp only [cr_experiment, wp_bind, wp_get, wp_pure]: wp-tower with both lazy_query calls visible. Call the inner state parameters σ₂ (after cr_loop), σ₅ (after first lazy_query), σ₆ (after second).

2. Apply lazy_query_wp_writes_output to the first lazy_query (returning y from x_v = claim_x.get σ₂). This strengthens the postcondition of lazy_query x_v with RO[x_v] = some y at σ₅.

3. Apply lazy_query_wp_writes_output to the second lazy_query (y' ← lazy_query x'_v). Postcondition gains RO[x'_v] = some y' at σ₆.

4. Apply lazy_query_wp_preserves_other_RO to the second lazy_query with x = x'_v, x' = x_v (under x_v ≠ x'_v): RO[x_v] preserved from σ₅ to σ₆, so still = some y at σ₆.

5. Apply lazy_query_wp_preserves_disjoint to both lazy_query calls for claim_x and claim_x'. These give us claim_x.get σ₆ = x_v and claim_x'.get σ₆ = x'_v.

6. At the leaf, with all invariants strengthened into the post: result = decide (x_v ≠ x'_v ∧ y = y') = true ⟹ claim_x.get σ₆ = x_v ≠ x'_v = claim_x'.get σ₆, and RO[x_v] = some y = some y' = RO[x'_v] at σ₆. So has_collision σ₆ with witnesses (x_v, x'_v, y).

7. The strengthened post is pointwise ≤ collision_indicator σ₆; apply MeasureTheory.lintegral_mono propagated outward through each wp_bind layer.

Birthday-bound decomposition

The proof is decomposed into:

• RO_size — counts the cached entries of the random oracle.
• lazy_query_collision_step (Layer A) — each query bumps the collision probability by at most RO_size σ / N. Core probability content.
• lazy_query_RO_size_step (Layer B, proved) — each query's expected RO_size grows by at most 1. Combinatorial.
• cr_loop_birthday_step (Layer C) — combining A and B over cr_loop k: after k queries the collision bump is at most the triangular sum k * (2 * RO_size σ + k - 1) / (2N).
• cr_collision_birthday_bound (Layer D, proved modulo A & C) — combines cr_loop q with the two final queries.

noncomputable def RO_size (σ : state) : ℕ

The number of cached entries in the random oracle state.

Equations

• RO_size σ = {x : input | (random_oracle_state.get σ x).isSome = true}.card

Layer A and its sublemmas

lazy_query_collision_step (Layer A): each lazy_query bumps the collision probability by at most RO_size σ / N. The fresh-sample case is a union bound: each uniform sample collides with at most RO_size σ existing entries (each with probability 1/N). Decomposed into 5 helpers below.

noncomputable def inducing_set (x : input) (σ : state) : Finset output

The Finset of output values that a fresh sample at x could collide with: values that already appear in the RO at some other input.

Equations

• inducing_set x σ = Finset.image (fun (x' : input) => (random_oracle_state.get σ x').getD default) ({x' ∈ Finset.univ.erase x | (random_oracle_state.get σ x').isSome = true})

theorem mem_inducing_set_iff (x : input) (σ : state) (y : output) : y ∈ inducing_set x σ ↔ ∃ (x' : input), x' ≠ x ∧ random_oracle_state.get σ x' = some y

Membership characterization.

theorem inducing_set_card_le_RO_size (x : input) (σ : state) : (inducing_set x σ).card ≤ RO_size σ

The inducing set has at most RO_size σ elements.

theorem lazy_query_collision_step (x : input) (σ : state) : (lazy_query x).wp (fun (yσ : output × state) => collision_indicator yσ.2) σ ≤ collision_indicator σ + ↑(RO_size σ) / ↑(Fintype.card output)

theorem lazy_query_RO_size_step (x : input) (σ : state) : (lazy_query x).wp (fun (yσ : output × state) => ↑(RO_size yσ.2)) σ ≤ ↑(RO_size σ) + 1

Layer B: the expected RO_size after one lazy_query is at most one more than before. (Tight: in the cached branch, equal; in the fresh branch, exactly +1.) Reduced to the generic lazy_query_wp_step with pointwise bad-event 1.

theorem RO_size_of_get_eq {σ σ' : state} (h : random_oracle_state.get σ' = random_oracle_state.get σ) : RO_size σ' = RO_size σ

RO_size factors through the RO content: equal RO maps give equal sizes.

theorem cr_adv_wp_RO_size (cr_adv : GaudisCrypt.ProgramDenotation state Unit) (h_cr_adv : cr_adv.inFootprint (GaudisCrypt.Lens.footprint random_oracle_state)ᶜ) (σ : state) : cr_adv.wp (fun (yσ : Unit × state) => ↑(RO_size yσ.2)) σ ≤ ↑(RO_size σ)

cr_adv doesn't touch the RO, so its expected RO_size is preserved.

theorem RO_size_set_disjoint {α : Type} (v : Variable α) [GaudisCrypt.disjoint v random_oracle_state] (x : α) (σ : state) : RO_size (v.set x σ) = RO_size σ

Setting a variable disjoint from random_oracle_state doesn't change RO_size.

theorem cr_loop_body_wp_RO_size (cr_adv : GaudisCrypt.ProgramDenotation state Unit) (h_cr_adv : cr_adv.inFootprint (GaudisCrypt.Lens.footprint random_oracle_state)ᶜ) (σ : state) : (cr_loop_body cr_adv lazy_query).wp (fun (yσ : Unit × state) => ↑(RO_size yσ.2)) σ ≤ ↑(RO_size σ) + 1

One iteration of cr_loop_body bumps RO_size by at most 1 in expectation. Reduced to the generic oracle_step_wp_indicator_bump_const.

theorem cr_loop_RO_size_step (cr_adv : GaudisCrypt.ProgramDenotation state Unit) (h_cr_adv : cr_adv.inFootprint (GaudisCrypt.Lens.footprint random_oracle_state)ᶜ) (k : ℕ) (σ : state) : (cr_loop cr_adv k lazy_query).wp (fun (yσ : Unit × state) => ↑(RO_size yσ.2)) σ ≤ ↑(RO_size σ) + ↑k

Layer B-iterated: expected RO_size after cr_loop k grows by at most k. Needed by Layer D to bound the size at intermediate points. Reduced to the generic oracle_loop_n_wp_linear_bound with c = 1.

Collision-side helpers (mirror of the RO_size helpers above)

theorem collision_indicator_of_get_eq {σ σ' : state} (h : random_oracle_state.get σ' = random_oracle_state.get σ) : collision_indicator σ' = collision_indicator σ

collision_indicator factors through the RO content.

theorem cr_adv_wp_collision (cr_adv : GaudisCrypt.ProgramDenotation state Unit) (h_cr_adv : cr_adv.inFootprint (GaudisCrypt.Lens.footprint random_oracle_state)ᶜ) (σ : state) : cr_adv.wp (fun (yσ : Unit × state) => collision_indicator yσ.2) σ ≤ collision_indicator σ

cr_adv doesn't touch the RO, so the collision indicator is preserved in expectation.

theorem collision_indicator_set_disjoint {α : Type} (v : Variable α) [GaudisCrypt.disjoint v random_oracle_state] (x : α) (σ : state) : collision_indicator (v.set x σ) = collision_indicator σ

Setting a variable disjoint from random_oracle_state doesn't change collision_indicator.

theorem cr_loop_body_wp_collision (cr_adv : GaudisCrypt.ProgramDenotation state Unit) (h_cr_adv : cr_adv.inFootprint (GaudisCrypt.Lens.footprint random_oracle_state)ᶜ) (σ : state) : (cr_loop_body cr_adv lazy_query).wp (fun (yσ : Unit × state) => collision_indicator yσ.2) σ ≤ collision_indicator σ + ↑(RO_size σ) / ↑(Fintype.card output)

One iteration of cr_loop_body bumps the collision indicator by at most RO_size σ / N (in expectation). Reduced to the generic oracle_step_wp_indicator_bump.

theorem cr_loop_birthday_step (cr_adv : GaudisCrypt.ProgramDenotation state Unit) (h_cr_adv : cr_adv.inFootprint (GaudisCrypt.Lens.footprint random_oracle_state)ᶜ) (k : ℕ) (σ : state) : (cr_loop cr_adv k lazy_query).wp (fun (yσ : Unit × state) => collision_indicator yσ.2) σ ≤ collision_indicator σ + ↑k * (2 * ↑(RO_size σ) + ↑k - 1) / (2 * ↑(Fintype.card output))

Layer C: the cumulative collision bound after cr_loop k queries. Triangular sum of Layer A across the loop.

Proof plan (induction on k):

• Base k=0: cr_loop 0 = pure, no bump.
• Step k+1: cr_loop_body bumps collision by ≤ RO_size σ / N (helper above). Then by IH at post-body state σ' (with RO_size σ' ≤ RO_size σ + 1 in expectation), the rest adds at most k(2*(RO_size σ + 1) + k - 1)/(2N) = k(2RO_size σ + k + 1)/(2N). Combined: RO_size σ/N + k(2RO_size σ + k + 1)/(2N) = (k+1)(2*RO_size σ + k)/(2N), matching the bound at level k+1.

lazy_init zeroing

theorem lazy_init_RO_size (σ₀ : state) : RO_size (random_oracle_state.set (fun (x : input) => none) σ₀) = 0

After lazy_init, the RO is empty: RO_size = 0.

theorem lazy_init_collision_indicator (σ₀ : state) : collision_indicator (random_oracle_state.set (fun (x : input) => none) σ₀) = 0

After lazy_init, no collision exists.

theorem cr_collision_birthday_bound (cr_adv : GaudisCrypt.ProgramDenotation state Unit) (h_cr_adv : cr_adv.inFootprint (GaudisCrypt.Lens.footprint random_oracle_state)ᶜ) (q : ℕ) (σ₀ : state) : (cr_experiment cr_adv q lazy_init lazy_query).wp (fun (bσ : Bool × state) => collision_indicator bσ.2) σ₀ ≤ (↑q + 2) * (↑q + 1) / (2 * ↑(Fintype.card output))

Layer D — cr_collision_birthday_bound: composition of A, B, C.

After lazy_init, RO_size = 0. After cr_loop q, by Layer C the bound is q(q-1)/(2N). The two final queries add at most (q + (q+1))/N (via Layer A applied twice). Total: (q+2)(q+1)/(2N).

theorem cr_lazy_bound (cr_adv : GaudisCrypt.ProgramDenotation state Unit) (h_cr_adv : cr_adv.inFootprint (GaudisCrypt.Lens.footprint random_oracle_state)ᶜ) (q : ℕ) (σ₀ : state) : (cr_experiment cr_adv q lazy_init lazy_query).wp (fun (bσ : Bool × state) => if bσ.1 = true then 1 else 0) σ₀ ≤ (↑q + 2) * (↑q + 1) / (2 * ↑(Fintype.card output))

Birthday bound for the lazy CR experiment. Proved by composing the bookkeeping lemma with the probability bound.

theorem cr_transfer_wp_of_bit (cr_adv : GaudisCrypt.ProgramDenotation state Unit) (h_cr_adv : cr_adv.inFootprint (GaudisCrypt.Lens.footprint random_oracle_state)ᶜ) (q : ℕ) (σ₀ : state) (G : Bool → ENNReal) : (cr_experiment cr_adv q lazy_init lazy_query).wp (fun (bσ : Bool × state) => G bσ.1) σ₀ = (cr_experiment cr_adv q random_oracle_init random_oracle_query).wp (fun (bσ : Bool × state) => G bσ.1) σ₀

Transfer of cr_transfer from the SubProb marginal level to the wp level, for postconditions that depend only on the result bit bσ.1. This bridges Phase 2 and Phase 3 for cr_eager_bound. Thin wrapper over the generic ProgramDenotation.wp_eq_of_marginal_eq.

theorem cr_eager_bound (cr_adv : GaudisCrypt.ProgramDenotation state Unit) (h_cr_adv : cr_adv.inFootprint (GaudisCrypt.Lens.footprint random_oracle_state)ᶜ) (q : ℕ) (σ₀ : state) : (cr_experiment cr_adv q random_oracle_init random_oracle_query).wp (fun (bσ : Bool × state) => if bσ.1 = true then 1 else 0) σ₀ ≤ (↑q + 2) * (↑q + 1) / (2 * ↑(Fintype.card output))

Birthday bound for the eager (true random oracle) game, obtained by transferring cr_lazy_bound via cr_transfer.

theorem loop_n_lazy_query_collision_bound (A : GaudisCrypt.ProgramDenotation state Unit) (hA : A.inFootprint (GaudisCrypt.Lens.footprint random_oracle_state)ᶜ) (q : ℕ) (σ₀ : state) : (do lazy_init GaudisCrypt.loop_n q (oracle_step A lazy_query)).wp (fun (yσ : Unit × state) => collision_indicator yσ.2) σ₀ ≤ ↑q * (↑q - 1) / (2 * ↑(Fintype.card output))

Generic lazy-oracle collision bound. For any adversary A that only touches the random-oracle state, after lazy_init and q query rounds (each round runs A, then answers one lazy_query), the probability that the oracle map contains a collision is at most q(q−1)/2N.

This is the birthday framework loop_n_birthday_bound instantiated at the RO collision/size potentials, with lazy_init zeroing both. Unlike cr_collision_birthday_bound (which carries two extra challenge queries, giving (q+2)(q+1)/2N), this is the clean q(q−1)/2N for the bare q-round loop — the Pr[bad] input to the PRP/PRF switching lemma.