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

axiom chal_x_queried_gh :

Variable Bool

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

source

axiom disjoint_chal_x_queried_gh_ro :

GaudisCrypt.disjoint chal_x_queried_gh random_oracle_state

source

axiom disjoint_chal_x_queried_gh_ow_challenge_x :

GaudisCrypt.disjoint chal_x_queried_gh ow_challenge_x

source

axiom disjoint_chal_x_queried_gh_ow_challenge_y :

GaudisCrypt.disjoint chal_x_queried_gh ow_challenge_y

source

axiom disjoint_chal_x_queried_gh_ow_response :

GaudisCrypt.disjoint chal_x_queried_gh ow_response

source

axiom disjoint_chal_x_queried_gh_oracle_input :

GaudisCrypt.disjoint chal_x_queried_gh oracle_input

source

axiom disjoint_chal_x_queried_gh_oracle_output :

GaudisCrypt.disjoint chal_x_queried_gh oracle_output

source

instance instDisjointForallInputOptionOutputStateBoolRandom_oracle_stateChal_x_queried_gh :

GaudisCrypt.disjoint random_oracle_state chal_x_queried_gh

Symmetric instances.

source

instance instDisjointInputStateBoolOw_challenge_xChal_x_queried_gh :

GaudisCrypt.disjoint ow_challenge_x chal_x_queried_gh

source

instance instDisjointOutputStateBoolOw_challenge_yChal_x_queried_gh :

GaudisCrypt.disjoint ow_challenge_y chal_x_queried_gh

source

instance instDisjointInputStateBoolOw_responseChal_x_queried_gh :

GaudisCrypt.disjoint ow_response chal_x_queried_gh

source

instance instDisjointInputStateBoolOracle_inputChal_x_queried_gh :

GaudisCrypt.disjoint oracle_input chal_x_queried_gh

source

instance instDisjointOutputStateBoolOracle_outputChal_x_queried_gh :

GaudisCrypt.disjoint oracle_output chal_x_queried_gh

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

axiom matched_chal_y :

Variable Bool

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

source

axiom disjoint_matched_chal_y_ro :

GaudisCrypt.disjoint matched_chal_y random_oracle_state

source

axiom disjoint_matched_chal_y_chal_x :

GaudisCrypt.disjoint matched_chal_y ow_challenge_x

source

axiom disjoint_matched_chal_y_chal_y :

GaudisCrypt.disjoint matched_chal_y ow_challenge_y

source

axiom disjoint_matched_chal_y_response :

GaudisCrypt.disjoint matched_chal_y ow_response

source

axiom disjoint_matched_chal_y_input :

GaudisCrypt.disjoint matched_chal_y oracle_input

source

axiom disjoint_matched_chal_y_output :

GaudisCrypt.disjoint matched_chal_y oracle_output

source

axiom disjoint_matched_chal_y_chal_x_queried_gh :

GaudisCrypt.disjoint matched_chal_y chal_x_queried_gh

source

instance instDisjointForallInputOptionOutputStateBoolRandom_oracle_stateMatched_chal_y :

GaudisCrypt.disjoint random_oracle_state matched_chal_y

source

instance instDisjointInputStateBoolOw_challenge_xMatched_chal_y :

GaudisCrypt.disjoint ow_challenge_x matched_chal_y

source

instance instDisjointOutputStateBoolOw_challenge_yMatched_chal_y :

GaudisCrypt.disjoint ow_challenge_y matched_chal_y

source

instance instDisjointInputStateBoolOw_responseMatched_chal_y :

GaudisCrypt.disjoint ow_response matched_chal_y

source

instance instDisjointInputStateBoolOracle_inputMatched_chal_y :

GaudisCrypt.disjoint oracle_input matched_chal_y

source

instance instDisjointOutputStateBoolOracle_outputMatched_chal_y :

GaudisCrypt.disjoint oracle_output matched_chal_y

source

instance instDisjointBoolStateChal_x_queried_ghMatched_chal_y :

GaudisCrypt.disjoint chal_x_queried_gh matched_chal_y

source

axiom queries_input :

Variable (List input)

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

source

axiom queries_output :

Variable (List output)

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

source

axiom disjoint_queries_input_chal_x_queried_gh :

GaudisCrypt.disjoint queries_input chal_x_queried_gh

source

axiom disjoint_queries_input_ro :

GaudisCrypt.disjoint queries_input random_oracle_state

source

axiom disjoint_queries_input_chal_x :

GaudisCrypt.disjoint queries_input ow_challenge_x

source

axiom disjoint_queries_input_chal_y :

GaudisCrypt.disjoint queries_input ow_challenge_y

source

axiom disjoint_queries_input_response :

GaudisCrypt.disjoint queries_input ow_response

source

axiom disjoint_queries_input_oracle_input :

GaudisCrypt.disjoint queries_input oracle_input

source

axiom disjoint_queries_input_oracle_output :

GaudisCrypt.disjoint queries_input oracle_output

source

axiom disjoint_queries_output_matched_chal_y :

GaudisCrypt.disjoint queries_output matched_chal_y

source

axiom disjoint_queries_output_ro :

GaudisCrypt.disjoint queries_output random_oracle_state

source

axiom disjoint_queries_output_chal_x :

GaudisCrypt.disjoint queries_output ow_challenge_x

source

axiom disjoint_queries_output_chal_y :

GaudisCrypt.disjoint queries_output ow_challenge_y

source

axiom disjoint_queries_output_response :

GaudisCrypt.disjoint queries_output ow_response

source

axiom disjoint_queries_output_oracle_input :

GaudisCrypt.disjoint queries_output oracle_input

source

axiom disjoint_queries_output_oracle_output :

GaudisCrypt.disjoint queries_output oracle_output

source

axiom disjoint_queries_output_chal_x_queried_gh :

GaudisCrypt.disjoint queries_output chal_x_queried_gh

source

instance instDisjointBoolStateListInputChal_x_queried_ghQueries_input :

GaudisCrypt.disjoint chal_x_queried_gh queries_input

source

instance instDisjointForallInputOptionOutputStateListRandom_oracle_stateQueries_input :

GaudisCrypt.disjoint random_oracle_state queries_input

source

instance instDisjointInputStateListOw_challenge_xQueries_input :

GaudisCrypt.disjoint ow_challenge_x queries_input

source

instance instDisjointOutputStateListInputOw_challenge_yQueries_input :

GaudisCrypt.disjoint ow_challenge_y queries_input

source

instance instDisjointInputStateListOw_responseQueries_input :

GaudisCrypt.disjoint ow_response queries_input

source

instance instDisjointInputStateListOracle_inputQueries_input :

GaudisCrypt.disjoint oracle_input queries_input

source

instance instDisjointOutputStateListInputOracle_outputQueries_input :

GaudisCrypt.disjoint oracle_output queries_input

source

instance instDisjointBoolStateListOutputMatched_chal_yQueries_output :

GaudisCrypt.disjoint matched_chal_y queries_output

source

instance instDisjointForallInputOptionOutputStateListRandom_oracle_stateQueries_output :

GaudisCrypt.disjoint random_oracle_state queries_output

source

instance instDisjointInputStateListOutputOw_challenge_xQueries_output :

GaudisCrypt.disjoint ow_challenge_x queries_output

source

instance instDisjointOutputStateListOw_challenge_yQueries_output :

GaudisCrypt.disjoint ow_challenge_y queries_output

source

instance instDisjointInputStateListOutputOw_responseQueries_output :

GaudisCrypt.disjoint ow_response queries_output

source

instance instDisjointInputStateListOutputOracle_inputQueries_output :

GaudisCrypt.disjoint oracle_input queries_output

source

instance instDisjointOutputStateListOracle_outputQueries_output :

GaudisCrypt.disjoint oracle_output queries_output

source

instance instDisjointBoolStateListOutputChal_x_queried_ghQueries_output :

GaudisCrypt.disjoint chal_x_queried_gh queries_output

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