IND-security of the hashed one-time pad

The encryption Enc(k, m) = H(k) ⊕ m with H a random oracle and key k ← input is left-or-right indistinguishable: an adversary making at most q oracle queries cannot tell an encryption of m₀ from one of m₁, beyond its chance of querying the key:

|Pr[A : guess | enc m₀] − Pr[A : guess | enc m₁]| ≤ 2 (q + 1) / |input|

Proof, by game hopping

The challenger samples the key k, computes H(k) (a fresh uniform value on the empty cache), publishes the ciphertext c = H(k) ⊕ m_b, then runs the adversary's query loop. The two worlds differ only in m_b.

• Preprogramming (enc_game_eq_pre): H(k) on the empty oracle is a fresh uniform written into RO[k], exposing the sample that the OTP coupling acts on.
• One-time-pad coupling + up-to-bad (enc_game_relE): couple the key samples by identity and the masks by the bijection hk ↦ hk + (m₀ − m₁), so the published ciphertexts coincide (hk + m₀ = (hk + m₀ − m₁) + m₁). The two runs then differ only at RO[k] — exactly the OW up-to-bad invariant InvUB k hk — so the shared loop body relates by the OW core body_relE, and the guesses agree until the adversary queries k.
• Bad bound (enc_bad_bound): Pr[adversary queries k] ≤ (q+1)/|input|, a deferred-sampling reduction to the guess_experiment framework, in three steps: enc_pre_bad_eq_nopre (dropping the RO[k] preprogramming is invisible — relE.bad_eq), enc_nopre_bad_le_gexp (reindex the mask to a fresh ciphertext so m drops out, sum_comm, tail monotonicity enc_tail_mono), and gexp_env_c_bound (the guess-experiment bound, reusing OW's game_1_correspondence).

We reuse ow_challenge_x as the key register and chal_x_queried_gh as the "queried the key" flag, so lazy_query_tracked and the entire OW up-to-bad core (body_relE, InvUB, …) apply verbatim.

Result

enc_ind_secure (fully proved, no sorry): for a q-query adversary, Pr[A guesses ∣ enc m₀] ≤ Pr[A guesses ∣ enc m₁] + (q+1)/|input|. By symmetry in m₀, m₁, |Pr₀ − Pr₁| ≤ (q+1)/|input|. The whole proof is game hopping in the relational calculus, reusing the OW up-to-bad core and guess-experiment framework wholesale.

axiom outputCommGroup : AddCommGroup output

A commutative group structure on the output type, modelling the one-time-pad mask (e.g. bitwise XOR). Axiomatized on the opaque output, consistent with its other instances.

axiom chal_c : Variable output

The published ciphertext, readable by the adversary.

axiom guess_var : Variable Bool

The adversary's guess bit.

axiom disjoint_chal_c_ro : GaudisCrypt.disjoint chal_c random_oracle_state

axiom disjoint_chal_c_chal_x : GaudisCrypt.disjoint chal_c ow_challenge_x

axiom disjoint_chal_c_flag : GaudisCrypt.disjoint chal_c chal_x_queried_gh

axiom disjoint_chal_c_oracle_input : GaudisCrypt.disjoint chal_c oracle_input

axiom disjoint_chal_c_oracle_output : GaudisCrypt.disjoint chal_c oracle_output

axiom disjoint_guess_ro : GaudisCrypt.disjoint guess_var random_oracle_state

axiom disjoint_guess_chal_x : GaudisCrypt.disjoint guess_var ow_challenge_x

axiom disjoint_guess_flag : GaudisCrypt.disjoint guess_var chal_x_queried_gh

axiom disjoint_guess_chal_c : GaudisCrypt.disjoint guess_var chal_c

instance instDisjointForallInputOptionOutputStateRandom_oracle_stateChal_c : GaudisCrypt.disjoint random_oracle_state chal_c

instance instDisjointInputStateOutputOw_challenge_xChal_c : GaudisCrypt.disjoint ow_challenge_x chal_c

instance instDisjointBoolStateOutputChal_x_queried_ghChal_c : GaudisCrypt.disjoint chal_x_queried_gh chal_c

instance instDisjointInputStateOutputOracle_inputChal_c : GaudisCrypt.disjoint oracle_input chal_c

instance instDisjointOutputStateOracle_outputChal_c : GaudisCrypt.disjoint oracle_output chal_c

instance instDisjointForallInputOptionOutputStateBoolRandom_oracle_stateGuess_var : GaudisCrypt.disjoint random_oracle_state guess_var

instance instDisjointInputStateBoolOw_challenge_xGuess_var : GaudisCrypt.disjoint ow_challenge_x guess_var

instance instDisjointBoolStateChal_x_queried_ghGuess_var : GaudisCrypt.disjoint chal_x_queried_gh guess_var

instance instDisjointOutputStateBoolChal_cGuess_var : GaudisCrypt.disjoint chal_c guess_var

noncomputable def enc_game (enc_adv : GaudisCrypt.ProgramDenotation state Unit) (m : output) (q : ℕ) : GaudisCrypt.ProgramDenotation state Bool

The IND game: sample key, compute H(key) (the challenger's own, untracked query), publish H(key) ⊕ m, initialize the "queried the key" flag, run the adversary's tracked query loop, read its guess. The result bit is the adversary's guess.

Equations

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

noncomputable def enc_game_pre (enc_adv : GaudisCrypt.ProgramDenotation state Unit) (m : output) (q : ℕ) : GaudisCrypt.ProgramDenotation state Bool

The preprogrammed form: H(key) on the empty oracle is a fresh uniform sample written into RO[key].

Equations

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

The win indicator and bad event

Stage 1: indistinguishability up to the bad event

The two encryption worlds, after preprogramming, are related by one relE judgment whose post is encPost. The loop reuses the OW up-to-bad body coupling body_relE verbatim.

theorem enc_game_pre_relE (enc_adv : GaudisCrypt.ProgramDenotation state Unit) (h_RO : enc_adv.inFootprint (GaudisCrypt.Lens.footprint random_oracle_state)ᶜ) (h_flag : enc_adv.inFootprint (GaudisCrypt.Lens.footprint chal_x_queried_gh)ᶜ) (h_cx : enc_adv.inFootprint (GaudisCrypt.Lens.footprint ow_challenge_x)ᶜ) (h_mass : ∀ (σ : state), enc_adv.wp (fun (x : Unit × state) => 1) σ = 1) (m₀ m₁ : output) (q : ℕ) : (enc_game_pre enc_adv m₀ q).relE (enc_game_pre enc_adv m₁ q) Eq encPost✝

The game-level coupling: the two preprogrammed worlds relate at encPost — flags agree, and on good runs the guesses agree. Peels the shared prefix (lazy_init, key sample, set key) and applies the OTP tail.

The preprogramming mini-hop

theorem enc_game_wp_eq_pre (enc_adv : GaudisCrypt.ProgramDenotation state Unit) (m : output) (q : ℕ) (F : Bool × state → ENNReal) (σ : state) : (enc_game enc_adv m q).wp F σ = (enc_game_pre enc_adv m q).wp F σ

H(key) on the empty oracle is a fresh uniform written into RO[key]: enc_game and enc_game_pre have equal wp.

Stage 1 result: indistinguishability up to the bad event

theorem enc_guess_le_pre (enc_adv : GaudisCrypt.ProgramDenotation state Unit) (h_RO : enc_adv.inFootprint (GaudisCrypt.Lens.footprint random_oracle_state)ᶜ) (h_flag : enc_adv.inFootprint (GaudisCrypt.Lens.footprint chal_x_queried_gh)ᶜ) (h_cx : enc_adv.inFootprint (GaudisCrypt.Lens.footprint ow_challenge_x)ᶜ) (h_mass : ∀ (σ : state), enc_adv.wp (fun (x : Unit × state) => 1) σ = 1) (m₀ m₁ : output) (q : ℕ) (σ : state) : (enc_game_pre enc_adv m₀ q).wp (fun (bσ : Bool × state) => if bσ.1 = true then 1 else 0) σ ≤ (enc_game_pre enc_adv m₁ q).wp (fun (bσ : Bool × state) => if bσ.1 = true then 1 else 0) σ + (enc_game_pre enc_adv m₀ q).wp (fun (bσ : Bool × state) => if chal_x_queried_gh.get bσ.2 = true then if bσ.1 = true then 1 else 0 else 0) σ

One-sided up-to-bad bound: the guess probability in world m₀ is at most that in world m₁ plus the chance the adversary queries the key. (enc_game_pre-level; the mini-hop transfers it to enc_game.)

theorem enc_guess_le (enc_adv : GaudisCrypt.ProgramDenotation state Unit) (h_RO : enc_adv.inFootprint (GaudisCrypt.Lens.footprint random_oracle_state)ᶜ) (h_flag : enc_adv.inFootprint (GaudisCrypt.Lens.footprint chal_x_queried_gh)ᶜ) (h_cx : enc_adv.inFootprint (GaudisCrypt.Lens.footprint ow_challenge_x)ᶜ) (h_mass : ∀ (σ : state), enc_adv.wp (fun (x : Unit × state) => 1) σ = 1) (m₀ m₁ : output) (q : ℕ) (σ : state) : (enc_game enc_adv m₀ q).wp (fun (bσ : Bool × state) => if bσ.1 = true then 1 else 0) σ ≤ (enc_game enc_adv m₁ q).wp (fun (bσ : Bool × state) => if bσ.1 = true then 1 else 0) σ + (enc_game enc_adv m₀ q).wp (fun (bσ : Bool × state) => if chal_x_queried_gh.get bσ.2 = true then 1 else 0) σ

Indistinguishability up to the bad event (at the enc_game level). The guess probability in world m₀ exceeds that in world m₁ by at most the chance the adversary queries the key.

Stage 2: bounding the bad event

Pr[adversary queries the key] ≤ (q+1)/|input|. We drop the RO[key] preprogramming (the runs are identical until the key is queried), reindex the mask to a fresh independent ciphertext, and bound by a guess_experiment built from the OW body_game_1/final_game_1 — for which game_1_correspondence already supplies the schema inequality.

noncomputable def enc_game_nopre (enc_adv : GaudisCrypt.ProgramDenotation state Unit) (m : output) (q : ℕ) : GaudisCrypt.ProgramDenotation state Bool

The game with H(key) not preprogrammed into RO[key]: a lazy query to the key would sample fresh. Identical to enc_game_pre until the key is queried (the bad event).

Equations

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

theorem enc_pre_bad_eq_nopre (enc_adv : GaudisCrypt.ProgramDenotation state Unit) (h_RO : enc_adv.inFootprint (GaudisCrypt.Lens.footprint random_oracle_state)ᶜ) (h_flag : enc_adv.inFootprint (GaudisCrypt.Lens.footprint chal_x_queried_gh)ᶜ) (h_cx : enc_adv.inFootprint (GaudisCrypt.Lens.footprint ow_challenge_x)ᶜ) (h_mass : ∀ (σ : state), enc_adv.wp (fun (x : Unit × state) => 1) σ = 1) (m : output) (q : ℕ) (σ : state) : (enc_game_pre enc_adv m q).wp (fun (bσ : Bool × state) => if chal_x_queried_gh.get bσ.2 = true then 1 else 0) σ = (enc_game_nopre enc_adv m q).wp (fun (bσ : Bool × state) => if chal_x_queried_gh.get bσ.2 = true then 1 else 0) σ

Dropping the preprogramming is invisible to the bad event. The two games differ only by set RO[key], so they sit at InvUB, and their bad flags agree (relE.bad_eq).

noncomputable def env_c : GaudisCrypt.ProgramDenotation state Unit

The env of the bad-event guess experiment: lazy oracle, then publish a fresh uniform ciphertext (the mask reindex makes m disappear).

Equations

• env_c = do lazy_init let c ← GaudisCrypt.ProgramDenotation.uniform GaudisCrypt.ProgramDenotation.set chal_c c

theorem gexp_env_c_bound (enc_adv : GaudisCrypt.ProgramDenotation state Unit) (h_flag : enc_adv.inFootprint (GaudisCrypt.Lens.footprint chal_x_queried_gh)ᶜ) (h_cx : enc_adv.inFootprint (GaudisCrypt.Lens.footprint ow_challenge_x)ᶜ) (h_qi : enc_adv.inFootprint (GaudisCrypt.Lens.footprint queries_input)ᶜ) (q : ℕ) (σ : state) : (guess_experiment env_c GaudisCrypt.ProgramDenotation.uniform ow_challenge_x chal_x_queried_gh (body_game_1 enc_adv) final_game_1 q).wp (fun (bσ : Bool × state) => if bσ.1 = true then 1 else 0) σ ≤ (↑q + 1) / ↑(Fintype.card input)

The guess-experiment bound for the bad event: the adversary hits the uniform key with probability ≤ (q+1)/|input|. Reuses OW's game_1_correspondence (env-generic) + the generic interim bound.

theorem enc_nopre_bad_le_gexp (enc_adv : GaudisCrypt.ProgramDenotation state Unit) (m : output) (q : ℕ) (σ : state) : (enc_game_nopre enc_adv m q).wp (fun (bσ : Bool × state) => if chal_x_queried_gh.get bσ.2 = true then 1 else 0) σ ≤ (guess_experiment env_c GaudisCrypt.ProgramDenotation.uniform ow_challenge_x chal_x_queried_gh (body_game_1 enc_adv) final_game_1 q).wp (fun (bσ : Bool × state) => if bσ.1 = true then 1 else 0) σ

The lazy-run bad event is bounded by the guess-experiment matched event: reindex the mask to a fresh ciphertext (m drops out), commute the sums, and apply the tail bound termwise.

theorem enc_bad_bound (enc_adv : GaudisCrypt.ProgramDenotation state Unit) (h_RO : enc_adv.inFootprint (GaudisCrypt.Lens.footprint random_oracle_state)ᶜ) (h_flag : enc_adv.inFootprint (GaudisCrypt.Lens.footprint chal_x_queried_gh)ᶜ) (h_cx : enc_adv.inFootprint (GaudisCrypt.Lens.footprint ow_challenge_x)ᶜ) (h_mass : ∀ (σ : state), enc_adv.wp (fun (x : Unit × state) => 1) σ = 1) (h_qi : enc_adv.inFootprint (GaudisCrypt.Lens.footprint queries_input)ᶜ) (m : output) (q : ℕ) (σ : state) : (enc_game enc_adv m q).wp (fun (bσ : Bool × state) => if chal_x_queried_gh.get bσ.2 = true then 1 else 0) σ ≤ (↑q + 1) / ↑(Fintype.card input)

The bad-event bound: Pr[adversary queries the key] ≤ (q+1)/|input|. Mini-hop → drop preprogramming → guess-experiment bound.

The headline theorem

theorem enc_ind_secure (enc_adv : GaudisCrypt.ProgramDenotation state Unit) (h_RO : enc_adv.inFootprint (GaudisCrypt.Lens.footprint random_oracle_state)ᶜ) (h_flag : enc_adv.inFootprint (GaudisCrypt.Lens.footprint chal_x_queried_gh)ᶜ) (h_cx : enc_adv.inFootprint (GaudisCrypt.Lens.footprint ow_challenge_x)ᶜ) (h_qi : enc_adv.inFootprint (GaudisCrypt.Lens.footprint queries_input)ᶜ) (h_mass : ∀ (σ : state), enc_adv.wp (fun (x : Unit × state) => 1) σ = 1) (m₀ m₁ : output) (q : ℕ) (σ : state) : (enc_game enc_adv m₀ q).wp (fun (bσ : Bool × state) => if bσ.1 = true then 1 else 0) σ ≤ (enc_game enc_adv m₁ q).wp (fun (bσ : Bool × state) => if bσ.1 = true then 1 else 0) σ + (↑q + 1) / ↑(Fintype.card input)

IND-security of the hashed one-time pad. The adversary's guess probability in the m₀ world exceeds that in the m₁ world by at most (q+1)/|input| (its chance of querying the key). Symmetric in m₀, m₁, so |Pr₀ − Pr₁| ≤ (q+1)/|input|.