One-wayness of the random oracle

A 101-crypto example mirroring CollisionResistance.lean. The OW game:

1. Sample challenge input x ← uniform.
2. Compute y := oracle(x) and publish y via ow_challenge_y.
3. Run the adversary ow_adv for q rounds with oracle access; the adversary writes its candidate preimage to ow_response.
4. Check whether oracle(ow_response) = y.

The high-level claims:

• ow_transfer — the win-bit distribution is identical under lazy and eager RO.
• ow_lazy_bound — the lazy win probability is at most 2(q + 1) / |output| (the standard linear bound: (q+1)/|output| from a useful_preimage union bound over the q loop queries and 1 final query, plus (q+1)/|input| ≤ (q+1)/|output| for the chance the adversary's response happens to equal the uniformly random ow_challenge_x).
• ow_eager_bound — the same bound, via ow_transfer.

The bound is linear in q (not quadratic like CR's birthday bound), because each lazy_query has at most 1 / |output| chance of producing the fixed challenge value y.

axiom ow_challenge_y : Variable output

The challenge value y published to the adversary (= oracle(x) for a random x).

axiom ow_challenge_x : Variable input

The original challenge input x (kept in state for the bound analysis).

axiom ow_response : Variable input

The adversary's response: its candidate preimage of the challenge.

axiom disjoint_ow_challenge_y_ro : GaudisCrypt.disjoint ow_challenge_y random_oracle_state

Disjointness: game-specific variables don't alias the random oracle.

axiom disjoint_ow_challenge_x_ro : GaudisCrypt.disjoint ow_challenge_x random_oracle_state

axiom disjoint_ow_response_ro : GaudisCrypt.disjoint ow_response random_oracle_state

axiom disjoint_oracle_input_ow_challenge_y : GaudisCrypt.disjoint oracle_input ow_challenge_y

Game-specific variables are disjoint from the loop's scratch variables. Needed so that ow_loop_body's ProgramDenotation.get oracle_input / ProgramDenotation.set oracle_output / random_oracle_state operations preserve ow_challenge_y (and similarly for ow_response).

axiom disjoint_oracle_output_ow_challenge_y : GaudisCrypt.disjoint oracle_output ow_challenge_y

axiom disjoint_ro_ow_challenge_y : GaudisCrypt.disjoint random_oracle_state ow_challenge_y

axiom disjoint_oracle_input_ow_challenge_x : GaudisCrypt.disjoint oracle_input ow_challenge_x

axiom disjoint_oracle_output_ow_challenge_x : GaudisCrypt.disjoint oracle_output ow_challenge_x

axiom disjoint_ro_ow_challenge_x : GaudisCrypt.disjoint random_oracle_state ow_challenge_x

axiom disjoint_ow_challenge_y_ow_challenge_x : GaudisCrypt.disjoint ow_challenge_y ow_challenge_x

axiom disjoint_oracle_input_ow_response : GaudisCrypt.disjoint oracle_input ow_response

axiom disjoint_oracle_output_ow_response : GaudisCrypt.disjoint oracle_output ow_response

axiom disjoint_ro_ow_response : GaudisCrypt.disjoint random_oracle_state ow_response

axiom disjoint_ow_response_ow_challenge_x : GaudisCrypt.disjoint ow_response ow_challenge_x

axiom disjoint_ow_response_ow_challenge_y : GaudisCrypt.disjoint ow_response ow_challenge_y

Game definition (parameterized over the adversary)

noncomputable def ow_loop_body (ow_adv : GaudisCrypt.ProgramDenotation state Unit) (oracle : input → GaudisCrypt.ProgramDenotation state output) : GaudisCrypt.ProgramDenotation state Unit

One round of the OW loop body: the adversary computes (and writes oracle_input), then we run one oracle query. Thin alias for the generic oracle_step in RO.lean (same shape as cr_loop_body).

Equations

• ow_loop_body ow_adv oracle = oracle_step ow_adv oracle

noncomputable def ow_loop (ow_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

• ow_loop ow_adv q oracle = oracle_loop_n ow_adv q oracle

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

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

Sample x, set y := oracle(x), publish y, run adversary for q rounds, read the adversary's response, and check whether oracle(response) = y.

Equations

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

Phase 2 — Transfer (lazy = eager)

Mirrors cr_transfer from CollisionResistance.lean.

theorem ow_transfer (ow_adv : GaudisCrypt.ProgramDenotation state Unit) (h_ow_adv : ow_adv.inFootprint (GaudisCrypt.Lens.footprint random_oracle_state)ᶜ) (q : ℕ) (σ₀ : state) : (do let bσ ← ow_experiment ow_adv q lazy_init lazy_query σ₀ pure bσ.1) = do let bσ ← ow_experiment ow_adv q random_oracle_init random_oracle_query σ₀ pure bσ.1

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

Phase 3 — Bookkeeping: win implies preimage in RO

State predicate: at the end of the experiment, if result = true, then RO[ow_response] = some ow_challenge_y. This is the OW analog of cr_true_implies_collision_wp.

def is_preimage (σ : state) : Prop

The "is a preimage" state predicate: RO σ (ow_response σ) = some (ow_challenge_y σ).

Equations

• is_preimage σ = (random_oracle_state.get σ (ow_response.get σ) = some (ow_challenge_y.get σ))

@[implicit_reducible]

noncomputable instance instDecidablePredStateIs_preimage : DecidablePred is_preimage

Equations

• instDecidablePredStateIs_preimage x✝ = Classical.propDecidable (is_preimage x✝)

noncomputable def preimage_indicator (σ : state) : ENNReal

0/1-valued indicator that ow_response is a preimage of ow_challenge_y in the random oracle.

Equations

• preimage_indicator σ = if is_preimage σ then 1 else 0

theorem ow_true_implies_preimage_wp (ow_adv : GaudisCrypt.ProgramDenotation state Unit) (h_ow_adv_chal_y : ow_adv.inFootprint (GaudisCrypt.Lens.footprint ow_challenge_y)ᶜ) (q : ℕ) (σ₀ : state) : (ow_experiment ow_adv q lazy_init lazy_query).wp (fun (bσ : Bool × state) => if bσ.1 = true then 1 else 0) σ₀ ≤ (ow_experiment ow_adv q lazy_init lazy_query).wp (fun (bσ : Bool × state) => preimage_indicator bσ.2) σ₀

Bookkeeping: if the experiment's result bit is true, then the final random oracle has ow_response as a preimage of ow_challenge_y.

Phase 4 — Probability bound on preimage_indicator

The bookkeeping lemma reduces P[win] to P[preimage_indicator at end], which we now bound by 2(q + 1) / |output| (the standard linear OW bound). Decomposed into layers analogous to CR's Layer A–D, but with a linear bound instead of quadratic (since each lazy_query has at most 1/|output| chance of producing the fixed challenge value, rather than RO_size/|output|).

Layer A_OW (per-query bound): each lazy_query bumps the expected "useful preimage" indicator by at most 1/|output|. The "useful preimage" is a preimage of ow_challenge_y other than ow_challenge_x — i.e., a preimage the adversary actually "found" rather than the trivially-cached challenge entry.

Layer C_OW (loop accumulation): by induction on q, ow_loop q bumps the useful_preimage indicator by ≤ q / |output|.

Layer D_OW (full composition): decompose preimage ≤ useful_preimage + [resp = ow_challenge_x ∧ preimage], where:

• E[useful_preimage] ≤ (q+1)/|output|: the loop contributes q/|output| (Layer C_OW); the final lazy_query resp contributes 1/|output| (Layer A_OW); the initial lazy_query x_orig contributes 0 because x_orig = ow_challenge_x (tight self-step).
• E[[resp = ow_challenge_x ∧ preimage]] ≤ (q+1)/|input|: the standard "guessing the secret" bound — ow_challenge_x is uniform over input, and the adversary can identify it only by lazy_querying it among q+1 total queries.

Total: 2(q+1)/|output|, using |input| ≥ |output|.

axiom card_input_ge_output : Fintype.card output ≤ Fintype.card input

Standard hash-function assumption: the input space is at least as large as the output space.

Definitions: useful_preimage

A useful preimage is a preimage of ow_challenge_y other than the trivially cached ow_challenge_x. We track this separately because:

• lazy_query x' bumps useful_preimage by exactly [x' ≠ ow_challenge_x ∧ fresh-sample = ow_challenge_y] (at most 1/|output| in expectation).
• useful_preimage depends only on random_oracle_state, ow_challenge_x, ow_challenge_y — variables disjoint from the adversary's range — so the adversary cannot affect it directly.

def useful_preimage (σ : state) : Prop

Equations

• useful_preimage σ = ∃ (x' : input), x' ≠ ow_challenge_x.get σ ∧ random_oracle_state.get σ x' = some (ow_challenge_y.get σ)

@[implicit_reducible]

noncomputable instance instDecidableUseful_preimage (σ : state) : Decidable (useful_preimage σ)

Equations

• instDecidableUseful_preimage σ = Classical.propDecidable (useful_preimage σ)

noncomputable def useful_preimage_indicator (σ : state) : ENNReal

Equations

• useful_preimage_indicator σ = if useful_preimage σ then 1 else 0

theorem preimage_le_useful_or_resp_eq_chal_x (σ : state) : preimage_indicator σ ≤ useful_preimage_indicator σ + if ow_response.get σ = ow_challenge_x.get σ ∧ is_preimage σ then 1 else 0

Structural decomposition: preimage implies either the response is the trivially cached challenge input, or there's a useful preimage.

Layer A_OW: per-query bump for useful_preimage_indicator

Layer C_OW: loop accumulation

Layer D_OW: full bound

theorem ow_experiment_useful_preimage_bound (ow_adv : GaudisCrypt.ProgramDenotation state Unit) (h_ow_adv : ow_adv.inFootprint (GaudisCrypt.Lens.footprint random_oracle_state)ᶜ) (h_ow_adv_chal_y : ow_adv.inFootprint (GaudisCrypt.Lens.footprint ow_challenge_y)ᶜ) (h_ow_adv_chal_x : ow_adv.inFootprint (GaudisCrypt.Lens.footprint ow_challenge_x)ᶜ) (q : ℕ) (σ₀ : state) : (ow_experiment ow_adv q lazy_init lazy_query).wp (fun (bσ : Bool × state) => useful_preimage_indicator bσ.2) σ₀ ≤ (↑q + 1) / ↑(Fintype.card output)

The expected useful_preimage_indicator at the end of the experiment is at most (q+1)/|output|: the initial lazy_query on ow_challenge_x adds nothing (handled by lazy_query_useful_preimage_step_self), the loop adds at most q/|output| (Layer C_OW), and the final lazy_query on the adversary's response adds at most 1/|output| (Layer A_OW).

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

Transfer of ow_transfer from the SubProb marginal level to the wp level, for postconditions that depend only on the result bit. Thin wrapper over the generic ProgramDenotation.wp_eq_of_marginal_eq.

The OW lazy/eager bounds (ow_lazy_bound, ow_eager_bound) and their intermediate ow_preimage_bound are proved in PlonkLean/RO/QueryHit.lean, which provides the deferred-sampling infrastructure needed to close the [resp = ow_challenge_x ∧ is_preimage] bound without axioms.