OneWayness GameHop: Definitions #

This module collects the game definitions used in the game-hopping proof of one-wayness for a random-oracle adversary:

ow_game_0 — the original OW experiment (eager RO).
ow_game_1 — equivalent to Game 0 but with y sampled and pre-programmed explicitly. Connected to Game 0 by ow_game_0_eq_ow_game_1 (Hop 0→1).
ow_game_1_tracked, ow_game_2_tracked — versions of Game 1 and Game 2 using lazy_query_tracked instead of lazy_query so the chal_x_queried_gh flag tracks whether chal_x was ever queried.

Plus the tracking flags and collector variables with their disjointness axioms / instances:

chal_x_queried_gh : Variable Bool — tracks whether the adv queried chal_x.
matched_chal_y : Variable Bool — tracks whether chal_y was returned.
queries_input : Variable (List input) — adversary's query list.
queries_output : Variable (List output) — RO's response list.

This module also defines lazy_query_tracked (the flag-flipping variant of lazy_query) which is shared by Game 1 and Game 2.

Game 0 — the original OW experiment #

This is exactly ow_experiment ow_adv q lazy_init lazy_query. We give it a new name here for clarity in the game-hopping chain.

source

noncomputable def ow_game_0 (ow_adv : GaudisCrypt.ProgramDenotation state Unit) (q : ℕ) :

GaudisCrypt.ProgramDenotation state Bool

Equations

ow_game_0 ow_adv q = ow_experiment ow_adv q lazy_init lazy_query

Instances For

Game 1 — explicit y sampling #

lazy_query x on an empty cache at x unfolds to "sample y uniform, write (x ↦ y) into RO, return y". Game 1 makes this explicit: sample y separately and write it into RO manually. Same distribution as Game 0.

source

noncomputable def ow_game_1 (ow_adv : GaudisCrypt.ProgramDenotation state Unit) (q : ℕ) :

GaudisCrypt.ProgramDenotation state Bool

Equations

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

Instances For

Hop 0 → 1: program equality #

ow_game_0 = ow_game_1 (no probabilistic content; just unfolding lazy_query x on an RO state where x is not cached).

source

theorem lazy_query_on_totally_empty_RO (inp : input) (σ : state) (h_empty : random_oracle_state.get σ = fun (x : input) => none) (F : output × state → ENNReal) :

(lazy_query inp).wp F σ = (do let y ← GaudisCrypt.ProgramDenotation.uniform GaudisCrypt.ProgramDenotation.set random_oracle_state fun (k : input) => if k = inp then some y else none pure y).wp F σ

On a state whose entire RO is fun _ => none (i.e., immediately after lazy_init), lazy_query inp is wp-equivalent to "sample a fresh y, insert (inp ↦ y) into the RO, return y".

source

theorem ow_game_0_eq_ow_game_1 (ow_adv : GaudisCrypt.ProgramDenotation state Unit) (q : ℕ) :

ow_game_0 ow_adv q = ow_game_1 ow_adv q

Hop 1 → 2: up-to-bad #

P[Game 1 wins] ≤ P[Game 2 wins] + P[bad in Game 1], where bad = "adversary queries the oracle at chal_x at some point in the loop or in the verification step."

The strategy:

Augment both games with a tracking flag chal_x_queried_gh that gets set to true whenever a lazy_query is invoked at input chal_x.
Show the tracked games are wp-equivalent to the untracked games on posts that ignore the flag (ProgramDenotation.wp_conditional_set_disjoint_no_op_footprint).
Show the tracked Game 1 and tracked Game 2 are identical until bad: their wp's agree on posts that vanish whenever the flag is true.
Apply ProgramDenotation.up_to_bad to derive Game 1_tracked.wp G ≤ Game 2_tracked.wp G + Game 1_tracked.wp (G | bad).
Strip tracking to obtain the corresponding statement for the un-tracked games.

source

instance instIsGlobalVarBoolChal_x_queried_ghMk :

chal_x_queried_gh.IsGlobalVar { name := "chal_x_queried_gh", type := Bool, nonempty := ⋯, key := 591631538543112835044201471496796222888401557337706049032565236488427516503197119205646226087805028, keyCorrect := ⋯ }

source

noncomputable def chal_x_queried_gh :

GaudisCrypt.Lens Bool GaudisCrypt.VariableAssignment

Fresh tracking flag for the game-hopping proof (separate from QueryHit's chal_x_queried to avoid cross-contamination).

Equations

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

Instances For

source

theorem disjoint_chal_x_queried_gh_ro :

chal_x_queried_gh.Disjoint random_oracle_state

source

theorem disjoint_chal_x_queried_gh_ow_challenge_x :

chal_x_queried_gh.Disjoint ow_challenge_x

source

theorem disjoint_chal_x_queried_gh_ow_challenge_y :

chal_x_queried_gh.Disjoint ow_challenge_y

source

theorem disjoint_chal_x_queried_gh_ow_response :

chal_x_queried_gh.Disjoint ow_response

source

theorem disjoint_chal_x_queried_gh_oracle_input :

chal_x_queried_gh.Disjoint oracle_input

source

theorem disjoint_chal_x_queried_gh_oracle_output :

chal_x_queried_gh.Disjoint oracle_output

source

noncomputable def lazy_query_tracked (inp : input) :

GaudisCrypt.ProgramDenotation state output

A lazy_query that also sets chal_x_queried_gh to true if the input equals chal_x. The tracked games use this in place of lazy_query. Defined via explicit >>= to avoid Lean's do-notation join-point macro on the if branch.

Equations

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

Instances For

Output-side matched flag for the Game 2 reduction #

The reduction Game 2 wins ≤ guess(output, q+1) matched tracks "some lazy_query returned chal_y" via a fresh flag matched_chal_y. Game 2's win event implies this flag is set: the final lazy_query_tracked returns y_check = chal_y, which sets the flag.

This is the standard cryptographic factorization where the matching event is captured by a dedicated flag, exposing it as a guess_experiment instance.

source

instance instIsGlobalVarBoolMatched_chal_yMk :

matched_chal_y.IsGlobalVar { name := "matched_chal_y", type := Bool, nonempty := ⋯, key := 497090213979999097269279505642886367906600992254961721271251819160921180955869294, keyCorrect := ⋯ }

source

noncomputable def matched_chal_y :

GaudisCrypt.Lens Bool GaudisCrypt.VariableAssignment

Matched flag for the output-side guess (against chal_y).

Equations

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

Instances For

source

theorem disjoint_matched_chal_y_ro :

matched_chal_y.Disjoint random_oracle_state

source

theorem disjoint_matched_chal_y_chal_x :

matched_chal_y.Disjoint ow_challenge_x

source

theorem disjoint_matched_chal_y_chal_y :

matched_chal_y.Disjoint ow_challenge_y

source

theorem disjoint_matched_chal_y_response :

matched_chal_y.Disjoint ow_response

source

theorem disjoint_matched_chal_y_input :

matched_chal_y.Disjoint oracle_input

source

theorem disjoint_matched_chal_y_output :

matched_chal_y.Disjoint oracle_output

source

theorem disjoint_matched_chal_y_chal_x_queried_gh :

matched_chal_y.Disjoint chal_x_queried_gh

source

instance instIsGlobalVarListInputQueries_inputMk :

queries_input.IsGlobalVar { name := "queries_input", type := List input, nonempty := ⋯, key := 427890336944210892864940756239465376254891241977580946207644200197340659826, keyCorrect := ⋯ }

source

noncomputable def queries_input :

GaudisCrypt.Lens (List input) GaudisCrypt.VariableAssignment

Queries list for the input-side collector (Game 1 bad reduction). Records adversary's inputs across loop iterations.

Equations

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

Instances For

source

instance instIsGlobalVarListOutputQueries_outputMk :

queries_output.IsGlobalVar { name := "queries_output", type := List output, nonempty := ⋯, key := 476717759073588686289223177868809398395024665074198397264579418271829119622054002, keyCorrect := ⋯ }

source

noncomputable def queries_output :

GaudisCrypt.Lens (List output) GaudisCrypt.VariableAssignment

Queries list for the output-side collector (Game 2 wins reduction). Records lazy_query_tracked outputs across loop iterations.

Equations

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

Instances For

source

theorem disjoint_queries_input_chal_x_queried_gh :

queries_input.Disjoint chal_x_queried_gh

source

theorem disjoint_queries_input_ro :

queries_input.Disjoint random_oracle_state

source

theorem disjoint_queries_input_chal_x :

queries_input.Disjoint ow_challenge_x

source

theorem disjoint_queries_input_chal_y :

queries_input.Disjoint ow_challenge_y

source

theorem disjoint_queries_input_response :

queries_input.Disjoint ow_response

source

theorem disjoint_queries_input_oracle_input :

queries_input.Disjoint oracle_input

source

theorem disjoint_queries_input_oracle_output :

queries_input.Disjoint oracle_output

source

theorem disjoint_queries_output_matched_chal_y :

queries_output.Disjoint matched_chal_y

source

theorem disjoint_queries_output_ro :

queries_output.Disjoint random_oracle_state

source

theorem disjoint_queries_output_chal_x :

queries_output.Disjoint ow_challenge_x

source

theorem disjoint_queries_output_chal_y :

queries_output.Disjoint ow_challenge_y

source

theorem disjoint_queries_output_response :

queries_output.Disjoint ow_response

source

theorem disjoint_queries_output_oracle_input :

queries_output.Disjoint oracle_input

source

theorem disjoint_queries_output_oracle_output :

queries_output.Disjoint oracle_output

source

theorem disjoint_queries_output_chal_x_queried_gh :

queries_output.Disjoint chal_x_queried_gh

source

noncomputable def ow_game_1_tracked (ow_adv : GaudisCrypt.ProgramDenotation state Unit) (q : ℕ) :

GaudisCrypt.ProgramDenotation state Bool

Tracked Game 1: same as ow_game_1, but every lazy_query is replaced by lazy_query_tracked so the chal_x_queried_gh flag tracks whether the adversary ever queried chal_x.

Equations