Deferred-sampling infrastructure for one-wayness #
This file provides the infrastructure to close the
ow_experiment_resp_eq_chal_x_bound lemma without axioms.
The standard cryptographic argument:
P[adv's output = chal_x in lazy game]
≤ P[adv ever queried chal_x] (bad event)
+ P[adv's output = chal_x ∧ ¬queried] (good event)
≤ q/|input| (Layer A_obs union bound)
+ 1/|input| (conditional independence on good event)
= (q+1)/|input|
Strategy #
Tracking variable
chal_x_queried : Variable Boolrecords whether any adversary lazy_query input has equalledow_challenge_xso far. The experiment (not adv) maintains this — adv cannot read or write it directly.Tracked experiment
ow_experiment_trackedis the same asow_experimentbut with the tracking variable updated in each loop iteration. Observable behavior (the win bit, the preimage condition) is unchanged.Equivalence:
ow_experiment.wp F σ = ow_experiment_tracked.wp F σfor anyFthat doesn't readchal_x_queried.Layer A_obs: per-iteration,
E[chal_x_queried becomes true] ≤ 1/|input|(viawp_shift_input_probon(chal_x.footprint)ᶜ).Layer C_obs: by induction,
E[chal_x_queried at end of ow_loop q] ≤ q/|input|.Conditional independence: on
¬chal_x_queried_at_end, adv's view is independent ofchal_x, so the final lazy_query's hit at chal_x has probability1/|input|.Composition: bound
[resp = chal_x ∧ preimage]by combining 5+6.
Tracking variable for whether the adversary has queried ow_challenge_x
via oracle_input in any loop iteration so far.
Initialized to false at the start of the tracked experiment, set to
true by the experiment (not the adversary) whenever it observes
oracle_input.get = ow_challenge_x.get at the moment of a lazy_query
in ow_loop_body.
Disjointness axioms for chal_x_queried #
Symmetric disjoint instances.
Tracked loop body and experiment #
The tracked version of ow_loop_body updates chal_x_queried whenever
the adversary's chosen oracle_input matches ow_challenge_x. This is
done by the experiment (it reads ow_challenge_x), not by adv.
One round of the tracked OW loop body. After adv sets oracle_input
and the experiment computes the oracle response, we additionally check
whether oracle_input = ow_challenge_x and update chal_x_queried.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Run the tracked loop for q rounds.
Equations
- ow_loop_tracked ow_adv 0 x✝ = pure ()
- ow_loop_tracked ow_adv n.succ x✝ = do ow_loop_body_tracked ow_adv x✝ ow_loop_tracked ow_adv n x✝
Instances For
The tracked OW experiment: like ow_experiment but with chal_x_queried
initialized to false at start and updated by ow_loop_body_tracked.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equivalence with the original experiment #
For post-conditions F that don't read chal_x_queried, the original
ow_experiment and ow_experiment_tracked have the same wp. The extra
ProgramDenotation.set chal_x_queried _ steps in the tracked version only modify a
variable that's disjoint from everything F reads.
A post-condition F : Bool × state → ENNReal "ignores chal_x_queried"
iff its value doesn't depend on chal_x_queried.get. Formally:
for any state, replacing chal_x_queried's value doesn't change F.
Equations
Instances For
The "preimage win" post-condition (which is what we care about for OW)
doesn't depend on chal_x_queried.
The "lazy_query then set oracle_output" rest of ow_loop_body is in
(chal_x_queried.footprint)ᶜ. Specialization of the generic
lazy_query_then_set_oracle_output_inFootprint_compl in RO.lean.
Specialization for ow_challenge_x.
The conditional set chal_x_queried step is a no-op for posts that
ignore chal_x_queried, provided the rest is in (chal_x_queried.footprint)ᶜ.
Thin wrapper over ProgramDenotation.wp_conditional_set_disjoint_no_op_footprint.
A helper combining get ow_challenge_x with the conditional set. Thin
wrapper over ProgramDenotation.wp_get_then_conditional_set_disjoint_no_op_footprint.
Per-iteration body equivalence: ow_loop_body and ow_loop_body_tracked
produce the same wp for posts that ignore chal_x_queried.
Loop and experiment equivalence #
By induction on q, the loop equivalence lifts the body equivalence.
This requires ow_adv.inFootprint (chal_x_queried.footprint)ᶜ so that
ow_loop (untouched) is in (chal_x_queried.footprint)ᶜ and the
"G' ignores chal_x_queried" hypothesis carries through induction.
Loop equivalence: ow_loop and ow_loop_tracked produce the same wp
for posts that ignore chal_x_queried. By induction on q.
Experiment equivalence (for lazy oracle): ow_experiment with
lazy_query and ow_experiment_tracked with lazy_query produce the same
wp for posts ignoring chal_x_queried.
Layer A_obs: per-iteration query-hit bound #
When entering a loop iteration with chal_x_queried = false, the probability
that the iteration sets chal_x_queried = true is at most 1/|input|.
The key insight: with chal_x_queried = false, by the equivalence lemma
combined with wp_shift_input_prob, the experiment's behavior up to this point
is independent of chal_x's value. Marginalizing over the initial uniform
sample of chal_x gives 1/|input|.
Bound on chal_x_queried_at_end (Layer C_obs) #
The "bad event" bound: across the q loop iterations, the probability that
some adversary oracle_input equals ow_challenge_x is at most q/|input|.
This is a union bound, valid because the adversary cannot read ow_challenge_x
and ow_challenge_x is uniformly sampled.
Proof sketch (Layer C_obs) #
The bound reduces (via wp_uniform at the experiment's outer uniform x) to
a strengthened sum inequality on the loop:
Sum lemma: ∀ q : ℕ, ∀ σ with chal_x_queried.get σ = false,
∑ x : input, (ow_loop_tracked q lazy_query).wp
[chal_x_queried.get bσ.2 = true] (ow_challenge_x.set x σ) ≤ q
Proof by induction on q.
q = 0:pure ()preserves chal_x_queried = false; indicator = 0; sum = 0. ✓q → q+1:- Unfold
ow_loop_tracked (q+1) = body_tracked >>= ow_loop_tracked q. - Use
wp_bindto factor. - body_tracked =
ow_adv >>= post_advwherepost_advdoes the conditional chal_x_queried update and the lazy_query. - Apply
wp_shift_input_probonow_adv(∈(chal_x.footprint)ᶜ): commute thechal_x.set xpast the adversary. - Apply
wp_finset_sumto pull∑ xinsideow_adv.wp. - For each adversary outcome
aσ_adv(withinp = oracle_input.get aσ_adv.2, noteinpis independent ofx):- For
x = inp(one term): the conditional fires, setting chal_x_queried = true; the rest of body preserves it; loop_q preserves it. Contribution ≤ 1. - For
x ≠ inp(other terms): conditional doesn't fire; the remaininglazy_query inp >>= set oracle_output >>= loop_qis independent ofxvia anotherwp_shift_input_prob(this program is in(chal_x.footprint)ᶜ). Applywp_finset_sumagain, then IH gives sum ≤ q.
- For
- Total per outcome: ≤ 1 + q. Adversary mass ≤ 1 gives sum ≤ q+1.
- Unfold
This argument relies crucially on h_ow_adv_chal_x: the adversary cannot read
ow_challenge_x, so its choice of inp is independent of chal_x.
Layer C_obs: the probability that chal_x_queried is set during the
tracked experiment is at most q/|input|.
Reduction: use lazy-query freshness invariance to drop the pre-loop's
lazy_query x (which only affects RO[x] = chal_y), then apply the
strengthened sum lemma.
Conditional independence: on the event ¬chal_x_queried_at_end,
the adversary's response equals ow_challenge_x with probability
at most 1/|input|.
Intuition: if chal_x_queried_at_end is false, the adversary never
queried ow_challenge_x during the loop. Since the adversary cannot
read ow_challenge_x directly, its view (and hence its response) is
statistically independent of ow_challenge_x. Thus the probability
the adversary's deterministic-from-view response coincides with the
uniformly-sampled ow_challenge_x is 1/|input|.
Composition: closing the OW bound #
Using the two bounds above plus the experiment equivalence, we close the
original ow_experiment_resp_eq_chal_x_bound sorry in OneWayness.lean.
The OW bound, via the tracking variable approach: in the lazy
experiment, E[resp = chal_x ∧ is_preimage] ≤ (q+1)/|input|.
Composes:
ow_experiment_eq_tracked_lazy(switch to tracked variant).resp_chal_x_preimage_decomp(decompose indicator).ow_experiment_tracked_chal_x_queried_bound(Layer C_obs).ow_experiment_tracked_indep_bound(conditional independence).
Layer D_OW (closed): probability bound on preimage_indicator at the
end of the experiment. Closes the original ow_preimage_bound from
OneWayness.lean without axioms (modulo two clean sub-bounds).
Birthday-style bound for the lazy one-wayness experiment, closed via the deferred-sampling tracking variable.
One-wayness bound for the eager (true random oracle) game, obtained by
transferring ow_lazy_bound via ow_transfer. Closed via the tracking
variable.