From ca0bccbaec658520e0fcf88f01c9ac6343d3e386 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 23 Oct 2026 22:49:17 -0400 Subject: [PATCH 1/3] feat(probability): structural call budgets, presampling and the difference lemma MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `OracleComp.IsQueryBounded` bounds the calls of a program on every path. It is preserved by sequencing and by running through a handler, and it implies the semantic `HasQueryBounds`. A budget justifies presampling a handler's per-call draws (`run_interpret_withSampleList`). `IdenticalUntilBad` gives the difference lemma for stateful handlers (`bind_apply_le`) and the accumulated bad-event bound `n · budget + C(n, 2) · δ` (`toOuterMeasure_bad_le`). `runWithAnswers_bind`, `length_runWithAnswers_le` and `runWithAnswers_run_interpret_invariant` reason about a handler's run on fixed answers. Refs #581 Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Dvi6MU29zU9t8zYfeU51sB --- .../Languages/Probabilistic/Forking.lean | 70 +++++++ .../Languages/Probabilistic/QueryCount.lean | 152 ++++++++++++++ .../Languages/Probabilistic/UntilBad.lean | 198 ++++++++++++++++++ 3 files changed, 420 insertions(+) create mode 100644 Complexity/Languages/Probabilistic/QueryCount.lean create mode 100644 Complexity/Languages/Probabilistic/UntilBad.lean diff --git a/Complexity/Languages/Probabilistic/Forking.lean b/Complexity/Languages/Probabilistic/Forking.lean index bab38b63c..ae119954d 100644 --- a/Complexity/Languages/Probabilistic/Forking.lean +++ b/Complexity/Languages/Probabilistic/Forking.lean @@ -8,6 +8,7 @@ module -- upstream: candidate public import Complexity.Languages.Probabilistic.Oracle.Transcript +public import Complexity.Languages.Probabilistic.QueryCount public import Complexity.Probability.Forking import Complexity.Languages.Probabilistic.Presample import Complexity.Languages.Probabilistic.Repeat @@ -27,6 +28,9 @@ ask the same first `j + 1` queries, so the named query exists in both and is the two answers differ (`mem_support_fork`). `runWithAnswers` runs a program on a list of answers, deterministically, recording its queries. +Sequencing splits the answers (`runWithAnswers_bind`), so properties of a program run through a +stateful handler follow from properties of single calls +(`runWithAnswers_run_interpret_invariant`). Answering queries from `q` presampled uniform answers has the law of answering them uniformly as they come, when the program asks at most `q` queries: this is the presampling theorem `ProbOracleComp.HasQueryBounds.eval_presample` (`interpret_uniform_eq`, and @@ -53,6 +57,9 @@ this form by drawing its coins in advance. The statements are exact; no efficien the named one, and answer it differently. * `Cslib.OracleComp.take_runWithAnswers`: a program's first `n + 1` queries depend only on its first `n` answers. +* `Cslib.OracleComp.runWithAnswers_run_interpret_invariant`: an invariant of a handler's state + and the queries asked so far holds after running a program through the handler on fixed + answers. ## References @@ -112,6 +119,69 @@ theorem take_runWithAnswers (default : H) (program : OracleComp (fun _ : Query = cases answers <;> cases answers' <;> simp_all simp only [runWithAnswers, List.take_succ_cons, hsplit.1, ih _ hsplit.2] +/-- Running a sequenced program on a list of answers runs the first part on the list and the +second part on the answers the first part left unused. -/ +theorem runWithAnswers_bind {β : Type} (default : H) (program : OracleComp (fun _ : Query => H) α) + (next : α → OracleComp (fun _ : Query => H) β) (answers : List H) : + runWithAnswers default (program >>= next) answers = + ((runWithAnswers default (next (runWithAnswers default program answers).1) + (answers.drop (runWithAnswers default program answers).2.length)).1, + (runWithAnswers default program answers).2 ++ + (runWithAnswers default (next (runWithAnswers default program answers).1) + (answers.drop (runWithAnswers default program answers).2.length)).2) := by + induction program generalizing answers with + | pure a => rfl + | liftBind q cont ih => + change runWithAnswers default (OracleComp.query q >>= fun a => cont a >>= next) answers = _ + rw [runWithAnswers_query_bind, ih] + cases answers with + | nil => simp [runWithAnswers] + | cons a rest => rfl + +/-- A program making at most `n` calls asks at most `n` queries on every list of answers. -/ +theorem IsQueryBounded.length_runWithAnswers_le (default : H) + {program : OracleComp (fun _ : Query => H) α} {n : ℕ} (h : IsQueryBounded program n) + (answers : List H) : (runWithAnswers default program answers).2.length ≤ n := by + induction h generalizing answers with + | pure a n => exact Nat.zero_le n + | liftBind q cont n _ ih => + change (q :: (runWithAnswers default (cont (answers.headD default)) answers.tail).2).length ≤ _ + rw [List.length_cons] + exact Nat.succ_le_succ (ih _ _) + +/-- **An invariant of a handler's run on a list of answers.** A program runs through a stateful +handler whose calls are oracle programs, and the resulting program runs on a list of answers. A +property of the handler's state and of the queries asked so far that every handler call +preserves, when run on the answers not yet used, holds at the end. -/ +theorem runWithAnswers_run_interpret_invariant {ι σ β : Type} {spec : ι → Type} (default : H) + (handler : (q : ι) → StateT σ (OracleComp (fun _ : Query => H)) (spec q)) + (answers : List H) (invariant : σ → List Query → Prop) + (step : ∀ q s queries, invariant s queries → + invariant (runWithAnswers default ((handler q).run s) (answers.drop queries.length)).1.2 + (queries ++ (runWithAnswers default ((handler q).run s) + (answers.drop queries.length)).2)) + (program : OracleComp spec β) (s : σ) (queries : List Query) (hs : invariant s queries) : + invariant (runWithAnswers default ((interpret handler program).run s) + (answers.drop queries.length)).1.2 + (queries ++ (runWithAnswers default ((interpret handler program).run s) + (answers.drop queries.length)).2) := by + induction program generalizing s queries with + | pure b => simpa using hs + | liftBind q cont ih => + change invariant (runWithAnswers default + ((interpret handler (OracleComp.query q >>= cont)).run s) + (answers.drop queries.length)).1.2 + (queries ++ (runWithAnswers default + ((interpret handler (OracleComp.query q >>= cont)).run s) + (answers.drop queries.length)).2) + simp only [interpret_bind, interpret_query, StateT.run_bind, runWithAnswers_bind, + List.drop_drop] + have hstep := step q s queries hs + have hnext := ih (runWithAnswers default ((handler q).run s) + (answers.drop queries.length)).1.1 _ _ hstep + simp only [List.length_append, List.append_assoc] at hnext + exact hnext + /-! ### Presampled answers -/ /-- Answering the lifted program from a saved list is running it on that list. -/ diff --git a/Complexity/Languages/Probabilistic/QueryCount.lean b/Complexity/Languages/Probabilistic/QueryCount.lean new file mode 100644 index 000000000..214e33464 --- /dev/null +++ b/Complexity/Languages/Probabilistic/QueryCount.lean @@ -0,0 +1,152 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Languages.Probabilistic.Oracle.Transcript +public import Complexity.Languages.Probabilistic.Presample +public import Complexity.Probability.IID +import Complexity.Probability.PMF + +/-! +# Counting oracle calls structurally + +`OracleComp.IsQueryBounded program n` says that `program` makes at most `n` oracle calls on every +path through its tree of calls, whatever the answers. This is the structural form of a call +budget: it is preserved by sequencing (`IsQueryBounded.bind`) and proved by induction on the +program, and it gives the semantic, handler-quantified bound +`ProbOracleComp.HasQueryBounds` for the program's external calls +(`IsQueryBounded.hasQueryBounds`). Running a program through a handler multiplies budgets +(`IsQueryBounded.run_interpret`). + +A budget also justifies presampling: a handler that draws one sample per call can read its +samples from a list of independent draws made in advance, with the same law of the result and the +final state (`IsQueryBounded.run_interpret_withSampleList`). + +## Main definitions + +* `Cslib.OracleComp.IsQueryBounded`: at most `n` calls on every path. + +## Main results + +* `Cslib.OracleComp.IsQueryBounded.bind`: budgets add under sequencing. +* `Cslib.OracleComp.IsQueryBounded.hasQueryBounds`: the semantic external call bound. +* `Cslib.OracleComp.IsQueryBounded.run_interpret`: the budget of a program run through a handler. +* `Cslib.OracleComp.IsQueryBounded.run_interpret_withSampleList`: presampling a handler's draws. +-/ + +@[expose] public section + +namespace Cslib.OracleComp + +universe u v + +variable {ι : Type u} {spec : OracleSpec.{u, v} ι} {α β : Type v} + +/-- The program makes at most `n` oracle calls on every path, whatever the answers. -/ +inductive IsQueryBounded : OracleComp spec α → ℕ → Prop + /-- Returning a value makes no call. -/ + | pure (a : α) (n : ℕ) : IsQueryBounded (PFunctor.FreeM.pure a) n + /-- A call followed by continuations that each make at most `n` calls. -/ + | liftBind (q : ι) (cont : spec q → OracleComp spec α) (n : ℕ) + (hcont : ∀ a, IsQueryBounded (cont a) n) : + IsQueryBounded (PFunctor.FreeM.liftBind q cont) (n + 1) + +namespace IsQueryBounded + +/-- A larger budget is still a budget. -/ +theorem mono {program : OracleComp spec α} {n m : ℕ} (h : IsQueryBounded program n) + (hnm : n ≤ m) : IsQueryBounded program m := by + induction h generalizing m with + | pure a n => exact .pure a m + | liftBind q cont n _ ih => + obtain ⟨m, rfl⟩ : ∃ m', m = m' + 1 := ⟨m - 1, by omega⟩ + exact .liftBind q cont m fun a => ih a (by omega) + +/-- One call. -/ +theorem query (q : ι) : IsQueryBounded (OracleComp.query (spec := spec) q) 1 := + .liftBind q _ 0 fun a => .pure a 0 + +/-- Budgets add under sequencing. -/ +theorem bind {program : OracleComp spec α} {next : α → OracleComp spec β} {n m : ℕ} + (h : IsQueryBounded program n) (hnext : ∀ a, IsQueryBounded (next a) m) : + IsQueryBounded (program >>= next) (n + m) := by + induction h with + | pure a n => exact (hnext a).mono (by omega) + | liftBind q cont n _ ih => + rw [show n + 1 + m = n + m + 1 by omega] + exact .liftBind q _ (n + m) ih + +end IsQueryBounded + +/-- A structural budget bounds the external calls of the program run with private +randomness, for every size bound on its queries. -/ +theorem IsQueryBounded.hasQueryBounds {Query : Type} {Response : Query → Type} {γ : Type} + {program : OracleComp Response γ} {n : ℕ} (h : IsQueryBounded program n) + {size : Query → ℕ} {maxSize : ℕ} (hsize : ∀ q, size q ≤ maxSize) : + (interpret (fun q => ProbOracleComp.query (spec := Response) q) + program).HasQueryBounds size n maxSize := by + induction h with + | pure a n => exact (ProbOracleComp.HasQueryBounds.pure a size maxSize).mono (by omega) le_rfl + | liftBind q cont n _ ih => + have hbind := (ProbOracleComp.HasQueryBounds.query (Response := Response) q size + (hsize q)).bind ih + rw [show 1 + n = n + 1 by omega] at hbind + exact hbind + +/-- A program run through a stateful handler, each of whose calls makes at most `k` calls to the +target oracle, makes at most `n * k` target calls when the program makes at most `n` calls. -/ +theorem IsQueryBounded.run_interpret {κ : Type u} {target : OracleSpec.{u, v} κ} {σ : Type v} + {handler : (q : ι) → StateT σ (OracleComp target) (spec q)} {k : ℕ} + (hhandler : ∀ q s, IsQueryBounded ((handler q).run s) k) {program : OracleComp spec α} + {n : ℕ} (h : IsQueryBounded program n) (s : σ) : + IsQueryBounded ((interpret handler program).run s) (n * k) := by + induction h generalizing s with + | pure a n => exact .pure (a, s) _ + | liftBind q cont n _ ih => + change IsQueryBounded ((interpret handler (OracleComp.query q >>= cont)).run s) _ + simp only [interpret_bind, interpret_query, StateT.run_bind] + rw [show (n + 1) * k = k + n * k by ring] + exact (hhandler q s).bind fun result => ih result.1 result.2 + +/-- **Presampling a handler's randomness.** A handler that draws one sample per call from +`source` can instead read the samples from a list of independent draws, made in advance: for a +program making at most `n` calls, `n` presampled draws give the same law of the result and the +final state. -/ +theorem IsQueryBounded.run_interpret_withSampleList {ι' σ γ V : Type} {spec' : ι' → Type} + {program : OracleComp spec' γ} {n : ℕ} (h : IsQueryBounded program n) (source : PMF V) + (fallback : V) (oracle : V → (q : ι') → StateT σ PMF (spec' q)) (s : σ) : + ((Probability.PMF.iid source n).map List.ofFn).bind (fun values => + ((interpret (withSampleList fallback oracle) program).run (s, values)).map + fun result => (result.1, result.2.1)) = + (interpret (m := StateT σ PMF) (fun q state => source.bind fun value => oracle value q state) + program).run s := by + induction h generalizing s with + | pure a n => + change ((Probability.PMF.iid source n).map List.ofFn).bind (fun values => + (PMF.pure (a, s, values)).map fun result => (result.1, result.2.1)) = PMF.pure (a, s) + simp only [PMF.pure_map, PMF.bind_const] + | liftBind q cont n _ ih => + change ((Probability.PMF.iid source (n + 1)).map List.ofFn).bind (fun values => + (((withSampleList fallback oracle q) (s, values)).bind fun result => + (interpret (withSampleList fallback oracle) (cont result.1)).run result.2).map + fun result => (result.1, result.2.1)) = + (source.bind fun value => oracle value q s).bind fun result => + (interpret (m := StateT σ PMF) + (fun q state => source.bind fun value => oracle value q state) (cont result.1)).run + result.2 + simp only [Probability.PMF.iid, withSampleList, Probability.PMF.monad_bind_eq_bind, + PMF.monad_map_eq_map, PMF.map_bind, PMF.bind_bind, PMF.bind_map, PMF.map_comp, + Function.comp_def, List.ofFn_succ, Fin.cons_zero, Fin.cons_succ, List.headD_cons, + List.tail_cons] + refine congrArg (source.bind ·) (funext fun value => ?_) + rw [PMF.bind_comm] + refine congrArg ((oracle value q s).bind ·) (funext fun result => ?_) + rw [← ih result.1 result.2, PMF.bind_map] + rfl + +end Cslib.OracleComp diff --git a/Complexity/Languages/Probabilistic/UntilBad.lean b/Complexity/Languages/Probabilistic/UntilBad.lean new file mode 100644 index 000000000..0c8c11a62 --- /dev/null +++ b/Complexity/Languages/Probabilistic/UntilBad.lean @@ -0,0 +1,198 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Languages.Probabilistic.QueryCount +public import Mathlib.Probability.ProbabilityMassFunction.Monad +import Complexity.Probability.PMF + +/-! +# Identical until bad + +Two stateful oracle handlers are *identical until bad* when, from a good state, they give the same +probability to every answer that leads to a good state, and bad states are absorbing in both. Then +the two interpretations of any program give the same probability to every outcome with a good +final state (`IdenticalUntilBad.run_apply`). Consequently, an experiment that continues the run +accepts with the first handler at most as often as with the second, plus the probability of +reaching a bad state ([BonehShoup2023], Theorem 4.7, the difference lemma), with no bound on the +program's number of calls (`IdenticalUntilBad.bind_apply_le`). + +The probability of reaching a bad state is bounded by summing over the calls: if each call from a +good state turns bad with probability at most `budget s`, and each call raises the budget by at +most `δ`, then a program making at most `n` calls reaches a bad state with probability at most +`n · budget s + C(n, 2) · δ` (`toOuterMeasure_bad_le`). This is the union bound for a growing +collision set, such as a random oracle that is programmed at points that may already be +defined. + +## Main definitions + +* `Cslib.OracleComp.IdenticalUntilBad`: two handlers that agree until a bad state. + +## Main results + +* `Cslib.OracleComp.IdenticalUntilBad.run_apply`: equal outcome probabilities at good states. +* `Cslib.OracleComp.IdenticalUntilBad.bind_apply_le`: the difference lemma. +* `Cslib.OracleComp.toOuterMeasure_bad_le`: the accumulated probability of a bad state. + +## References + +* [D. Boneh, V. Shoup, *A Graduate Course in Applied Cryptography*, + Version 0.6][BonehShoup2023], Theorem 4.7. +-/ + +@[expose] public section + +namespace Cslib.OracleComp + +open scoped ENNReal + +variable {ι σ α : Type} {spec : ι → Type} + +/-- Two stateful handlers agree until a bad state: from a good state they give equal probability +to every answer with a good next state, and bad states are absorbing for both. -/ +structure IdenticalUntilBad (first second : (q : ι) → StateT σ PMF (spec q)) (bad : σ → Prop) : + Prop where + /-- From a good state, answers with good next states are equally likely. -/ + agree : ∀ q s, ¬bad s → ∀ a s', ¬bad s' → first q s (a, s') = second q s (a, s') + /-- Bad states are absorbing for the first handler. -/ + absorb_first : ∀ q s, bad s → ∀ x ∈ (first q s).support, bad x.2 + /-- Bad states are absorbing for the second handler. -/ + absorb_second : ∀ q s, bad s → ∀ x ∈ (second q s).support, bad x.2 + +/-- A handler for which bad states are absorbing keeps every run from a bad state bad. -/ +theorem bad_of_mem_support_run {handler : (q : ι) → StateT σ PMF (spec q)} {bad : σ → Prop} + (habsorb : ∀ q s, bad s → ∀ x ∈ (handler q s).support, bad x.2) + (program : OracleComp spec α) {s : σ} (hs : bad s) : + ∀ x ∈ ((interpret handler program).run s).support, bad x.2 := by + induction program generalizing s with + | pure a => + intro x hx + rw [show (interpret handler (PFunctor.FreeM.pure a)).run s = PMF.pure (a, s) from rfl, + PMF.mem_support_pure_iff] at hx + exact hx ▸ hs + | liftBind q cont ih => + intro x hx + change x ∈ ((handler q s).bind fun y => (interpret handler (cont y.1)).run y.2).support at hx + rw [PMF.mem_support_bind_iff] at hx + obtain ⟨y, hy, hxy⟩ := hx + exact ih y.1 (habsorb q s hs y hy) x hxy + +namespace IdenticalUntilBad + +variable {first second : (q : ι) → StateT σ PMF (spec q)} {bad : σ → Prop} + +/-- Handlers that agree until a bad state give the same probability to every outcome whose final +state is good. -/ +theorem run_apply (h : IdenticalUntilBad first second bad) (program : OracleComp spec α) + (s : σ) (a : α) (s' : σ) (hs' : ¬bad s') : + (interpret first program).run s (a, s') = (interpret second program).run s (a, s') := by + induction program generalizing s with + | pure b => rfl + | liftBind q cont ih => + change ((first q s).bind fun y => (interpret first (cont y.1)).run y.2) (a, s') = + ((second q s).bind fun y => (interpret second (cont y.1)).run y.2) (a, s') + rw [PMF.bind_apply, PMF.bind_apply] + refine tsum_congr fun y => ?_ + by_cases hy : bad y.2 + · have hzero (handler : (q : ι) → StateT σ PMF (spec q)) + (habsorb : ∀ q s, bad s → ∀ x ∈ (handler q s).support, bad x.2) : + (interpret handler (cont y.1)).run y.2 (a, s') = 0 := + (PMF.apply_eq_zero_iff _ _).mpr fun hmem => + hs' (bad_of_mem_support_run habsorb (cont y.1) hy _ hmem) + rw [hzero first h.absorb_first, hzero second h.absorb_second, mul_zero, mul_zero] + · by_cases hs : bad s + · have hzero (handler : (q : ι) → StateT σ PMF (spec q)) + (habsorb : ∀ q s, bad s → ∀ x ∈ (handler q s).support, bad x.2) : + handler q s y = 0 := + (PMF.apply_eq_zero_iff _ _).mpr fun hmem => hy (habsorb q s hs y hmem) + rw [hzero first h.absorb_first, hzero second h.absorb_second, zero_mul, zero_mul] + · rw [show y = (y.1, y.2) from rfl, h.agree q s hs y.1 y.2 hy, ih y.1 y.2] + +/-- **The difference lemma** ([BonehShoup2023], Theorem 4.7): any experiment continuing the run +of a program accepts with the first handler at most as often as with the second, plus the +probability of reaching a bad state with the first. -/ +theorem bind_apply_le (h : IdenticalUntilBad first second bad) (program : OracleComp spec α) + (s : σ) {β : Type} (next : α × σ → PMF β) (b : β) : + ((interpret first program).run s).bind next b ≤ + ((interpret second program).run s).bind next b + + ((interpret first program).run s).toOuterMeasure {x | bad x.2} := by + classical + simp only [PMF.bind_apply, PMF.toOuterMeasure_apply] + rw [← ENNReal.tsum_add] + refine ENNReal.tsum_le_tsum fun x => ?_ + by_cases hx : bad x.2 + · have hbad : x ∈ {x : α × σ | bad x.2} := hx + rw [Set.indicator_of_mem hbad] + calc ((interpret first program).run s) x * next x b + ≤ ((interpret first program).run s) x * 1 := + mul_le_mul_of_nonneg_left (PMF.coe_le_one _ _) zero_le + _ ≤ _ := by rw [mul_one]; exact le_add_self + · have hgood : x ∉ {x : α × σ | bad x.2} := hx + rw [Set.indicator_of_notMem hgood, add_zero, show x = (x.1, x.2) from rfl, + h.run_apply program s x.1 x.2 hx] + +end IdenticalUntilBad + +/-- **The accumulated probability of a bad state.** If each call from a good state turns bad with +probability at most `budget s` and raises the budget by at most `δ`, a program making at most `n` +calls from a good state reaches a bad state with probability at most +`n · budget s + C(n, 2) · δ`. -/ +theorem toOuterMeasure_bad_le {handler : (q : ι) → StateT σ PMF (spec q)} {bad : σ → Prop} + (budget : σ → ℝ≥0∞) (δ : ℝ≥0∞) + (hstep : ∀ q s, ¬bad s → (handler q s).toOuterMeasure {x | bad x.2} ≤ budget s) + (hgrow : ∀ q s, ¬bad s → ∀ x ∈ (handler q s).support, ¬bad x.2 → + budget x.2 ≤ budget s + δ) + {program : OracleComp spec α} {n : ℕ} (hn : IsQueryBounded program n) {s : σ} + (hs : ¬bad s) : + ((interpret handler program).run s).toOuterMeasure {x | bad x.2} ≤ + n * budget s + n.choose 2 * δ := by + induction hn generalizing s with + | pure a n => + rw [show (interpret handler (PFunctor.FreeM.pure a)).run s = PMF.pure (a, s) from rfl, + PMF.toOuterMeasure_pure_apply, ite_eq_right (show (a, s) ∉ {x : α × σ | bad x.2} from hs)] + exact zero_le + | liftBind q cont n _ ih => + classical + change ((handler q s).bind fun y => (interpret handler (cont y.1)).run y.2).toOuterMeasure + {x | bad x.2} ≤ _ + rw [PMF.toOuterMeasure_bind_apply] + set K : ℝ≥0∞ := n * (budget s + δ) + n.choose 2 * δ + have hterm (y : spec q × σ) : (handler q s) y * + ((interpret handler (cont y.1)).run y.2).toOuterMeasure {x | bad x.2} ≤ + (handler q s) y * ({x : spec q × σ | bad x.2}.indicator 1 y + K) := by + by_cases hmem : y ∈ (handler q s).support + · refine mul_le_mul_of_nonneg_left ?_ zero_le + by_cases hy : bad y.2 + · have : y ∈ {x : spec q × σ | bad x.2} := hy + rw [Set.indicator_of_mem this, Pi.one_apply] + exact (Probability.PMF.toOuterMeasure_le_one _ _).trans le_self_add + · have : y ∉ {x : spec q × σ | bad x.2} := hy + rw [Set.indicator_of_notMem this, zero_add] + refine (ih y.1 hy).trans ?_ + simp only [K] + gcongr + exact hgrow q s hs y hmem hy + · rw [(PMF.apply_eq_zero_iff _ _).mpr hmem, zero_mul, zero_mul] + calc ∑' y, (handler q s) y * ((interpret handler (cont y.1)).run y.2).toOuterMeasure + {x | bad x.2} + ≤ ∑' y, (handler q s) y * ({x : spec q × σ | bad x.2}.indicator 1 y + K) := + ENNReal.tsum_le_tsum hterm + _ = (handler q s).toOuterMeasure {x | bad x.2} + K := by + simp only [mul_add, ENNReal.tsum_add, ENNReal.tsum_mul_right, PMF.tsum_coe, one_mul, + PMF.toOuterMeasure_apply] + congr 1 + refine tsum_congr fun y => ?_ + by_cases hy : y ∈ {x : spec q × σ | bad x.2} + · rw [Set.indicator_of_mem hy, Set.indicator_of_mem hy, Pi.one_apply, mul_one] + · rw [Set.indicator_of_notMem hy, Set.indicator_of_notMem hy, mul_zero] + _ ≤ budget s + K := add_le_add (hstep q s hs) le_rfl + _ = (n + 1 : ℕ) * budget s + (n + 1).choose 2 * δ := by + simp only [K, Nat.choose_succ_succ', Nat.choose_one_right, Nat.cast_add, Nat.cast_one] + ring + +end Cslib.OracleComp From 7e45c3e7582e733ec045f19ff78b843b5c94b412 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 23 Oct 2026 22:49:17 -0400 Subject: [PATCH 2/3] feat(crypto): signatures and EUF-CMA in the random-oracle model MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit A typed `ROMSignature.Scheme` signs and verifies with `OracleComp` access to `H : Query → Digest`. The oracle is lazily sampled and memoized. The forger has explicit coins, so it can be rerun. `eufCmaGame` is the random-oracle EUF-CMA experiment, and `Scheme.Correct` says that honest signatures verify. The oracle interface is kept small so it can be re-expressed in the interactive-protocol core of #643. Refs #581 Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Dvi6MU29zU9t8zYfeU51sB --- .../Protocols/Signature/RandomOracle.lean | 123 ++++++++++++++++++ 1 file changed, 123 insertions(+) create mode 100644 Complexity/Crypto/Protocols/Signature/RandomOracle.lean diff --git a/Complexity/Crypto/Protocols/Signature/RandomOracle.lean b/Complexity/Crypto/Protocols/Signature/RandomOracle.lean new file mode 100644 index 000000000..bc9f57786 --- /dev/null +++ b/Complexity/Crypto/Protocols/Signature/RandomOracle.lean @@ -0,0 +1,123 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Foundations.Control.Monad.Memoize +public import Complexity.Languages.Probabilistic.Basic +public import Cslib.Probability.PMF +import Complexity.Probability.PMF + +/-! +# Signatures in the random-oracle model + +A signature scheme in the random-oracle model ([BonehShoup2023], Section 13.2.1) signs and +verifies with oracle access to a function `H : Query → Digest`, which the security experiment +draws uniformly at random. Signing draws its coins and then runs an `OracleComp` program against +`H`; verification is a deterministic `OracleComp` program. The oracle is sampled lazily: each new +point gets a uniform answer, remembered in an association list (`oracle`), so the query and digest +types need not be finite beyond the digests. + +The existential-unforgeability experiment (`eufCmaGame`, [BonehShoup2023], Attack Game 13.1 in +its random-oracle version) gives a forger the public key and oracle access to the signer and to +`H`; the forger wins with a valid signature on a message it never asked to have signed. A +`Forger` has explicit coins, drawn first, and is otherwise a deterministic `OracleComp` program; +this is the form in which a forger can be rerun on the same coins, as forking needs. + +These are exact probability laws for one scheme and one forger, with no efficiency claim. The +oracle interface is the library's `OracleComp`; it is meant to be re-expressed in the shared +interactive-protocol core of #643 once that core exists. + +## Main definitions + +* `Cslib.Crypto.Protocols.ROMSignature.Scheme`: key generation, signing and verification. +* `Cslib.Crypto.Protocols.ROMSignature.Forger`: a forger with explicit coins. +* `Cslib.Crypto.Protocols.ROMSignature.oracle`: the lazily sampled uniform random oracle. +* `Cslib.Crypto.Protocols.ROMSignature.eufCmaGame`: the random-oracle EUF-CMA experiment. +* `Cslib.Crypto.Protocols.ROMSignature.Scheme.Correct`: honest signatures verify. + +## References + +* [D. Boneh, V. Shoup, *A Graduate Course in Applied Cryptography*, + Version 0.6][BonehShoup2023], Sections 13.1 and 13.2.1. +-/ + +@[expose] public section + +namespace Cslib.Crypto.Protocols.ROMSignature + +open Probability OracleComp + +/-- The calls of a forger: a signing call names a message and returns a signature, and a hash call +names a point and returns its digest. -/ +abbrev ForgerSpec (M Query Sig Digest : Type) : M ⊕ Query → Type + | .inl _ => Sig + | .inr _ => Digest + +/-- A signature scheme in the random-oracle model, with public keys `PK`, secret keys `SK`, +messages `M`, signatures `Sig`, and oracle `H : Query → Digest`. Signing first draws coins. -/ +structure Scheme (PK SK M Sig Query Digest : Type) where + /-- Draw a public key and a secret key. -/ + keyGen : PMF (PK × SK) + /-- The signer's coins. -/ + SignCoins : Type + /-- Draw the signer's coins for a message. -/ + signCoins : SK → M → PMF SignCoins + /-- Sign, querying the oracle. -/ + sign : SK → M → SignCoins → OracleComp (fun _ : Query => Digest) Sig + /-- Verify, querying the oracle. -/ + verify : PK → M → Sig → OracleComp (fun _ : Query => Digest) Bool + +/-- A forger with explicit coins: it draws its coins, then, given the public key, calls the signer +and the oracle and outputs a message and a signature. -/ +structure Forger (PK M Sig Query Digest : Type) where + /-- The forger's coins. -/ + Coins : Type + /-- Draw the forger's coins. -/ + coins : PMF Coins + /-- Forge, calling the signer and the oracle. -/ + forge : PK → Coins → OracleComp (ForgerSpec M Query Sig Digest) (M × Sig) + +variable {PK SK M Sig Query Digest : Type} [DecidableEq Query] [Fintype Digest] [Nonempty Digest] + +variable (Digest) in +/-- The random oracle: a uniform digest for each new point, remembered thereafter. -/ +noncomputable def oracle (q : Query) : StateT (List (Query × Digest)) PMF Digest := + memoize (fun _ => PMF.uniformOfFintype Digest) q + +/-- Answer a forger's calls: sign with the secret key, recording the message, or query the +oracle. Signing and the forger share the oracle. -/ +noncomputable def handler (scheme : Scheme PK SK M Sig Query Digest) (sk : SK) : + (q : M ⊕ Query) → StateT (List (Query × Digest) × List M) PMF (ForgerSpec M Query Sig Digest q) + | .inl m => fun state => do + let coins ← scheme.signCoins sk m + let signed ← (interpret (oracle Digest) (scheme.sign sk m coins)).run state.1 + return (signed.1, (signed.2, m :: state.2)) + | .inr x => fun state => do + let answer ← oracle Digest x state.1 + return (answer.1, (answer.2, state.2)) + +/-- The random-oracle EUF-CMA experiment ([BonehShoup2023], Attack Game 13.1): the forger wins with +a valid signature, under the same oracle, on a message it never had signed. -/ +noncomputable def eufCmaGame [DecidableEq M] (scheme : Scheme PK SK M Sig Query Digest) + (forger : Forger PK M Sig Query Digest) : PMF Bool := do + let keys ← scheme.keyGen + let s ← forger.coins + let forged ← (interpret (handler scheme keys.2) (forger.forge keys.1 s)).run ([], []) + let verified ← (interpret (oracle Digest) (scheme.verify keys.1 forged.1.1 forged.1.2)).run + forged.2.1 + return (verified.1 && !(forged.2.2.contains forged.1.1)) + +/-- A scheme is correct when every honest signature verifies under the same oracle, from every +state of the oracle. -/ +def Scheme.Correct (scheme : Scheme PK SK M Sig Query Digest) : Prop := + ∀ keys ∈ scheme.keyGen.support, ∀ m coins, coins ∈ (scheme.signCoins keys.2 m).support → + ∀ cache, ∀ signed ∈ ((interpret (oracle Digest) (scheme.sign keys.2 m coins)).run + cache).support, ∀ verified ∈ ((interpret (oracle Digest) + (scheme.verify keys.1 m signed.1)).run signed.2).support, verified.1 = true + +end Cslib.Crypto.Protocols.ROMSignature From df5dd4d0378cad1ef53e599294d0555f982c7ebc Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 23 Oct 2026 22:49:17 -0400 Subject: [PATCH 3/3] feat(crypto): Fiat-Shamir signatures and their exact security MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `fiatShamir` turns a Sigma protocol into a random-oracle signature scheme, and `fiatShamir_correct` shows that honest signatures verify. The protocol must be special sound on the generated keys and special HVZK, and must have δ-unpredictable commitments. Under these assumptions, `succProbability_eufCmaGame_le` bounds every forger with at most `Q` calls by `C(Q, 2) · δ + (Q + 1) / N + √((Q + 1) · ε')`, where ε' is the one-way success of the explicit forking reduction `FiatShamir.reduction` (Boneh–Shoup Theorem 19.16 and Equation 19.21, via Bellare–Neven). The tests instantiate the theorem for Schnorr signatures in `ZMod 11`. There, a forger that knows the witness forces `ε' ≥ 81 / 242`. Refs #581 Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Dvi6MU29zU9t8zYfeU51sB --- Complexity.lean | 4 + .../Protocols/SigmaProtocol/FiatShamir.lean | 933 ++++++++++++++++++ ComplexityTests.lean | 1 + ComplexityTests/Crypto/FiatShamir.lean | 152 +++ ROADMAP.md | 12 +- references.bib | 13 + 6 files changed, 1111 insertions(+), 4 deletions(-) create mode 100644 Complexity/Crypto/Protocols/SigmaProtocol/FiatShamir.lean create mode 100644 ComplexityTests/Crypto/FiatShamir.lean diff --git a/Complexity.lean b/Complexity.lean index d0a61e2d0..8ac58b914 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -1470,9 +1470,11 @@ public import Complexity.Crypto.Primitives.PRG.NisanWigderson.Reconstruction public import Complexity.Crypto.Primitives.PRG.NisanWigderson.Sampling public import Complexity.Crypto.Protocols.SigmaProtocol.Basic public import Complexity.Crypto.Protocols.SigmaProtocol.Composition +public import Complexity.Crypto.Protocols.SigmaProtocol.FiatShamir public import Complexity.Crypto.Protocols.SigmaProtocol.Identification public import Complexity.Crypto.Protocols.SigmaProtocol.Linear public import Complexity.Crypto.Protocols.SigmaProtocol.SchnorrIdentification +public import Complexity.Crypto.Protocols.Signature.RandomOracle public import Complexity.Foundations.Analysis.HarmonicMean public import Complexity.Foundations.Analysis.MarkovInequality public import Complexity.Foundations.Analysis.SpecialFunctions.Arccos @@ -1738,6 +1740,7 @@ public import Complexity.Languages.Probabilistic.Oracle.Simulation public import Complexity.Languages.Probabilistic.Oracle.Support public import Complexity.Languages.Probabilistic.Oracle.Transcript public import Complexity.Languages.Probabilistic.Presample +public import Complexity.Languages.Probabilistic.QueryCount public import Complexity.Languages.Probabilistic.RandomOracle public import Complexity.Languages.Probabilistic.RandomOracle.Probabilistic public import Complexity.Languages.Probabilistic.Repeat @@ -1746,6 +1749,7 @@ public import Complexity.Languages.Probabilistic.Simulation public import Complexity.Languages.Probabilistic.Transcript public import Complexity.Languages.Probabilistic.Traverse public import Complexity.Languages.Probabilistic.UniformNat +public import Complexity.Languages.Probabilistic.UntilBad public import Complexity.Languages.Probabilistic.Vector public import Complexity.Logics.FirstOrder.Basic public import Complexity.Logics.FirstOrder.Encoding diff --git a/Complexity/Crypto/Protocols/SigmaProtocol/FiatShamir.lean b/Complexity/Crypto/Protocols/SigmaProtocol/FiatShamir.lean new file mode 100644 index 000000000..1ec2b61c0 --- /dev/null +++ b/Complexity/Crypto/Protocols/SigmaProtocol/FiatShamir.lean @@ -0,0 +1,933 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Crypto.Protocols.SigmaProtocol.Identification +public import Complexity.Crypto.Protocols.Signature.RandomOracle +public import Complexity.Languages.Probabilistic.Forking +import Complexity.Languages.Probabilistic.Simulation +import Complexity.Languages.Probabilistic.UntilBad +import Complexity.Languages.Probabilistic.RandomOracle +import Complexity.Probability.PMF + +/-! +# Fiat–Shamir signatures + +The Fiat–Shamir transform ([BonehShoup2023], Section 19.6.1) turns a Sigma protocol into a +signature scheme in the random-oracle model: to sign `m`, the prover commits to `t`, takes the +challenge `c := H(m, t)` and responds with `z`; the signature `(t, z)` verifies when +`(t, H(m, t), z)` is an accepting conversation. + +Honest signatures verify (`fiatShamir_correct`). With special soundness, special HVZK and +`δ`-unpredictable commitments ([BonehShoup2023], Definition 19.7), a forger making at most `Q` +signing and hash calls in total wins the random-oracle EUF-CMA experiment with probability `ε` +bounded by + +`ε ≤ C(Q, 2) · δ + (Q + 1) / N + √((Q + 1) · ε')`, + +where `N` is the number of challenges and `ε'` the success probability of an explicit adversary +in the one-way game for the key generator (`succProbability_eufCmaGame_le`), as in +[BonehShoup2023], Equation 19.21, which has `Q_s (Q_s + Q_ro + 1) · δ` in place of +`C(Q, 2) · δ` and `Q_ro` in place of `Q`, for `Q_s` signing and `Q_ro` hash calls. + +The proof follows [BonehShoup2023], Theorems 19.7 and 19.16, with the general forking lemma of +[BellareNeven2006] in place of the reduction through impersonation: + +1. The signer is replaced by one that programs the oracle at `(m, t)` with a fresh challenge. + The two agree until the signer's commitment hits a point already in the oracle's table, which + has probability at most `C(Q, 2) · δ` (the difference lemma, + `OracleComp.IdenticalUntilBad.bind_apply_le`). +2. Special HVZK replaces the programming signer by the simulator, which needs no witness. +3. The simulated transcripts are drawn in advance, one per call + (`OracleComp.IsQueryBounded.run_interpret_withSampleList`). +4. The result is a program over the hash oracle alone, with explicit coins + (`FiatShamir.forkingProgram`), that names the hash query of the forgery whenever the forger + wins. The forking lemma (`OracleComp.le_add_sqrt_fork`) and special soundness turn it into + the one-way adversary `FiatShamir.reduction`. + +These are exact probability laws for one Sigma protocol, key generator and forger; there is no +efficiency claim. The forger has explicit coins, so the reduction can rerun it. + +## Main definitions + +* `Cslib.Crypto.Protocols.SigmaProtocol.fiatShamir`: the Fiat–Shamir signature scheme. +* `Cslib.Crypto.Protocols.SigmaProtocol.FiatShamir.forkingProgram`: the forger with simulated + signing, as a program over the hash oracle. +* `Cslib.Crypto.Protocols.SigmaProtocol.FiatShamir.reduction`: the one-way adversary. + +## Main results + +* `Cslib.Crypto.Protocols.SigmaProtocol.fiatShamir_correct`: honest signatures verify. +* `Cslib.Crypto.Protocols.SigmaProtocol.succProbability_eufCmaGame_le`: the security bound. + +## References + +* [D. Boneh, V. Shoup, *A Graduate Course in Applied Cryptography*, + Version 0.6][BonehShoup2023], Sections 19.2 and 19.6.1. +* [M. Bellare, G. Neven, *Multi-Signatures in the Plain Public-Key Model and a General Forking + Lemma*][BellareNeven2006], Lemma 1. +* [A. Fiat, A. Shamir, *How to Prove Yourself: Practical Solutions to Identification and Signature + Problems*][FiatShamir1986]. +-/ + +@[expose] public section + +namespace Cslib.Crypto.Protocols.SigmaProtocol + +open Probability OracleComp ROMSignature + +variable {X Y T C Z M : Type} + +/-- The Fiat–Shamir signature scheme ([BonehShoup2023], Section 19.6.1): the public key is the +statement and the secret key the witness-statement pair. To sign `m`, commit to `t`, query the +oracle at `(m, t)` for the challenge and respond; a signature `(t, z)` verifies when +`(t, H(m, t), z)` is accepting. -/ +noncomputable def fiatShamir (P : SigmaProtocol X Y T C Z) (keyGen : PMF (X × Y)) : + Scheme Y (X × Y) M (T × Z) (M × T) C where + keyGen := keyGen.map fun key => (key.2, key) + SignCoins := T × P.State + signCoins sk _ := P.commit sk.1 sk.2 + sign sk m coins := (fun c => (coins.1, P.respond sk.1 sk.2 coins.2 c)) <$> + OracleComp.query (spec := fun _ : M × T => C) (m, coins.1) + verify y m σ := (fun c => P.verify y σ.1 c σ.2) <$> + OracleComp.query (spec := fun _ : M × T => C) (m, σ.1) + +variable [DecidableEq M] [DecidableEq T] [Fintype C] [Nonempty C] + +/-- A table entry produced by a call of the oracle is found at its point. -/ +private theorem lookup_of_mem_support_oracle {x : M × T} {cache : List ((M × T) × C)} + {result : C × List ((M × T) × C)} (h : result ∈ (oracle C x cache).support) : + result.2.lookup x = some result.1 := by + rcases (RandomOracle.mem_support_memoize_iff _ _ _ _).mp h with ⟨hlookup, hnext⟩ | ⟨_, _, hnext⟩ + · rw [hnext, hlookup] + · rw [hnext, List.lookup_cons_self] + +/-- **Correctness** of Fiat–Shamir signatures: with a complete Sigma protocol and keys in the +relation, every honest signature verifies. -/ +theorem fiatShamir_correct {P : SigmaProtocol X Y T C Z} {keyGen : PMF (X × Y)} + {R : X → Y → Prop} (hP : P.Complete R) (hkey : ∀ key ∈ keyGen.support, R key.1 key.2) : + (fiatShamir (M := M) P keyGen).Correct := by + intro keys hkeys m coins hcoins cache signed hsigned verified hverified + obtain ⟨key, hmem, rfl⟩ := (PMF.mem_support_map_iff _ _ _).mp hkeys + simp only [fiatShamir, interpret_map, interpret_query, StateT.run_map, + PMF.monad_map_eq_map, PMF.mem_support_map_iff] at hsigned hverified + obtain ⟨r, hr, rfl⟩ := hsigned + obtain ⟨r', hr', rfl⟩ := hverified + have hlookup := lookup_of_mem_support_oracle hr + change r' ∈ (oracle C (m, coins.1) r.2).support at hr' + rw [oracle] at hr' + rw [memoize_of_some _ _ _ _ hlookup, PMF.monad_pure_eq_pure, PMF.mem_support_pure_iff] at hr' + subst hr' + exact hP.accepts_of_mem_support_commit (hkey key hmem) hcoins r.1 + +/-! ### The reduction -/ + +namespace FiatShamir + +/-- The state of the reduction while it runs the forger: the oracle table, each point with its +challenge and, when the reduction asked its own oracle for the point, the position of that query; +the messages signed so far; the number of queries asked so far; and the simulated transcripts not +used yet. -/ +structure ReductionState (M T C Z : Type) where + /-- The oracle table. -/ + table : List ((M × T) × C × Option ℕ) + /-- The messages signed so far. -/ + signed : List M + /-- The number of queries asked so far. -/ + count : ℕ + /-- The simulated transcripts not used yet. -/ + transcripts : List (T × C × Z) + +variable [Nonempty T] [Nonempty Z] + +/-- Answer the forger's calls without the witness, consuming one simulated transcript `(t, c, z)` +per call. A signing call on `m` returns `(t, z)` and programs the table at `(m, t)` with `c`. A +hash call returns the table's challenge, or asks the reduction's own oracle and records the +answer with the position of the query. -/ +noncomputable def reductionHandler : + (q : M ⊕ (M × T)) → StateT (ReductionState M T C Z) (OracleComp (fun _ : M × T => C)) + (ForgerSpec M (M × T) (T × Z) C q) + | .inl m => fun st => + let v := st.transcripts.headD (Classical.arbitrary _) + pure ((v.1, v.2.2), + ⟨((m, v.1), v.2.1, none) :: st.table, m :: st.signed, st.count, st.transcripts.tail⟩) + | .inr x => fun st => + match st.table.lookup x with + | some entry => pure (entry.1, ⟨st.table, st.signed, st.count, st.transcripts.tail⟩) + | none => (fun c => (c, ⟨(x, c, some st.count) :: st.table, st.signed, st.count + 1, + st.transcripts.tail⟩)) <$> OracleComp.query x + +/-- The verdict on a forgery `(m, (t, z))` whose point `(m, t)` has challenge `c`: the forgery wins +when `(t, c, z)` is accepting and `m` was never signed, and then the reduction names `position`, +the position of the query for `(m, t)`. The verdict records the point, the challenge and the +response. -/ +def verdict (P : SigmaProtocol X Y T C Z) (y : Y) (forged : (M × (T × Z)) × ReductionState M T C Z) + (c : C) (position : Option ℕ) : Option ℕ × Bool × (M × T) × C × Z := + (if P.verify y forged.1.2.1 c forged.1.2.2 && !forged.2.signed.contains forged.1.1 then position + else none, P.verify y forged.1.2.1 c forged.1.2.2 && !forged.2.signed.contains forged.1.1, + (forged.1.1, forged.1.2.1), c, forged.1.2.2) + +/-- Check a forgery, querying its point when the table lacks it. -/ +noncomputable def finish (P : SigmaProtocol X Y T C Z) (y : Y) + (forged : (M × (T × Z)) × ReductionState M T C Z) : + OracleComp (fun _ : M × T => C) (Option ℕ × Bool × (M × T) × C × Z) := + match forged.2.table.lookup (forged.1.1, forged.1.2.1) with + | some entry => pure (verdict P y forged entry.1 entry.2) + | none => (fun c => verdict P y forged c (some forged.2.count)) <$> + OracleComp.query (forged.1.1, forged.1.2.1) + +/-- The forger, with simulated signing, as a program over the hash oracle with explicit coins: the +statement, the forger's coins and the simulated transcripts. It names the query of the forgery's +point when the forger wins. -/ +noncomputable def forkingProgram (P : SigmaProtocol X Y T C Z) + (A : Forger Y M (T × Z) (M × T) C) (s : Y × A.Coins × List (T × C × Z)) : + OracleComp (fun _ : M × T => C) (Option ℕ × Bool × (M × T) × C × Z) := + (interpret reductionHandler (A.forge s.1 s.2.1)).run ⟨[], [], 0, s.2.2⟩ >>= finish P s.1 + +/-- The coins of the forking program for the statement `y`: the forger's coins and `Q` simulated +transcripts. -/ +noncomputable def coins (simulate : Y → C → PMF (T × Z)) (A : Forger Y M (T × Z) (M × T) C) + (Q : ℕ) (y : Y) : PMF (Y × A.Coins × List (T × C × Z)) := do + let s ← A.coins + let transcripts ← (PMF.iid (simulateConversation simulate y) Q).map List.ofFn + return (y, s, transcripts) + +variable [DecidableEq C] + +/-- **The one-way adversary** built from a forger: fork the forking program, with the `Q + 1` +answers of its hash oracle, and extract a witness from the two forgeries. -/ +noncomputable def reduction [Nonempty X] (P : SigmaProtocol X Y T C Z) + (simulate : Y → C → PMF (T × Z)) (extract : Y → T → C → Z → C → Z → X) + (A : Forger Y M (T × Z) (M × T) C) (Q : ℕ) (y : Y) : PMF X := + (Forking.fork (coins simulate A Q y) + (forkingAlgorithm (Classical.arbitrary C) (Q + 1) (forkingProgram P A))).map fun result => + match result with + | none => Classical.arbitrary X + | some (_, out, out') => + extract y out.1.2.2.1.2 out.1.2.2.2.1 out.1.2.2.2.2 out'.1.2.2.2.1 out'.1.2.2.2.2 + +end FiatShamir + +/-! ### Game hops -/ + +/-- The oracle table and the signed messages. -/ +private abbrev GameState (M T C : Type) := List ((M × T) × C) × List M + +/-- The experiment's final step: check the forgery against the oracle. -/ +private noncomputable def finishGame (P : SigmaProtocol X Y T C Z) (y : Y) + (forged : (M × (T × Z)) × GameState M T C) : PMF Bool := + (oracle C (forged.1.1, forged.1.2.1) forged.2.1).map fun r => + P.verify y forged.1.2.1 r.1 forged.1.2.2 && !forged.2.2.contains forged.1.1 + +/-- The EUF-CMA experiment for Fiat–Shamir signatures, with the final verification unfolded. -/ +private theorem eufCmaGame_fiatShamir (P : SigmaProtocol X Y T C Z) (keyGen : PMF (X × Y)) + (A : Forger Y M (T × Z) (M × T) C) : + eufCmaGame (fiatShamir P keyGen) A = keyGen.bind fun key => A.coins.bind fun s => + ((interpret (handler (fiatShamir P keyGen) key) (A.forge key.2 s)).run ([], [])).bind + (finishGame P key.2) := by + simp only [eufCmaGame, PMF.monad_bind_eq_bind, PMF.monad_pure_eq_pure] + rw [show (fiatShamir (M := M) P keyGen).keyGen = keyGen.map fun key => (key.2, key) from rfl, + PMF.bind_map] + refine congrArg keyGen.bind (funext fun key => congrArg A.coins.bind (funext fun s => ?_)) + refine congrArg (PMF.bind _) (funext fun forged => ?_) + simp only [fiatShamir, finishGame, interpret_map, interpret_query, StateT.run_map, + PMF.monad_map_eq_map, PMF.bind_map] + rfl + +/-- The real signer, with a flag raised when its commitment hits a point of the table. -/ +private noncomputable def realHandler (P : SigmaProtocol X Y T C Z) (key : X × Y) : + (q : M ⊕ (M × T)) → StateT (GameState M T C × Bool) PMF (ForgerSpec M (M × T) (T × Z) C q) + | .inl m => fun st => (P.commit key.1 key.2).bind fun ts => + (oracle C (m, ts.1) st.1.1).map fun r => ((ts.1, P.respond key.1 key.2 ts.2 r.1), + ((r.2, m :: st.1.2), st.2 || (st.1.1.lookup (m, ts.1)).isSome)) + | .inr x => fun st => (oracle C x st.1.1).map fun r => (r.1, ((r.2, st.1.2), st.2)) + +/-- The programming signer: it sets the oracle at `(m, t)` to a fresh challenge, with the same +flag as the real signer. -/ +private noncomputable def programHandler (P : SigmaProtocol X Y T C Z) (key : X × Y) : + (q : M ⊕ (M × T)) → StateT (GameState M T C × Bool) PMF (ForgerSpec M (M × T) (T × Z) C q) + | .inl m => fun st => (P.commit key.1 key.2).bind fun ts => + (PMF.uniformOfFintype C).map fun c => ((ts.1, P.respond key.1 key.2 ts.2 c), + ((((m, ts.1), c) :: st.1.1, m :: st.1.2), st.2 || (st.1.1.lookup (m, ts.1)).isSome)) + | .inr x => fun st => (oracle C x st.1.1).map fun r => (r.1, ((r.2, st.1.2), st.2)) + +/-- The signer from a simulated transcript `(t, c, z)`: it returns `(t, z)` and sets the oracle at +`(m, t)` to `c`. -/ +private noncomputable def simulatedHandler (v : T × C × Z) : + (q : M ⊕ (M × T)) → StateT (GameState M T C) PMF (ForgerSpec M (M × T) (T × Z) C q) + | .inl m => fun st => PMF.pure ((v.1, v.2.2), ((((m, v.1), v.2.1) :: st.1), m :: st.2)) + | .inr x => fun st => (oracle C x st.1).map fun r => (r.1, (r.2, st.2)) + +/-- Forgetting the flag, the flagged real signer is the real signer. -/ +private theorem realHandler_map (P : SigmaProtocol X Y T C Z) (keyGen : PMF (X × Y)) + (key : X × Y) (q : M ⊕ (M × T)) (st : GameState M T C × Bool) : + (realHandler P key q st).map (fun x => (x.1, x.2.1)) = + handler (fiatShamir P keyGen) key q st.1 := by + cases q with + | inl m => + simp only [realHandler, handler, fiatShamir, interpret_map, interpret_query, StateT.run_map, + PMF.monad_bind_eq_bind, PMF.monad_pure_eq_pure, PMF.monad_map_eq_map, PMF.map_bind, + PMF.map_comp, PMF.bind_map, Function.comp_def] + exact congrArg (PMF.bind _) (funext fun ts => (PMF.bind_pure_comp _ _).symm) + | inr x => + simp only [realHandler, handler, PMF.monad_bind_eq_bind, PMF.monad_pure_eq_pure, + PMF.map_comp, Function.comp_def] + rfl + +/-- An oracle call adds at most one entry to the table. -/ +private theorem length_le_of_mem_support_oracle {x : M × T} {cache : List ((M × T) × C)} + {result : C × List ((M × T) × C)} (h : result ∈ (oracle C x cache).support) : + result.2.length ≤ cache.length + 1 := by + rcases (RandomOracle.mem_support_memoize_iff _ _ _ _).mp h with ⟨_, hnext⟩ | ⟨_, _, hnext⟩ + · rw [hnext] + exact Nat.le_succ _ + · rw [hnext, List.length_cons] + +/-- The real and the programming signer agree until the flag is raised. -/ +private theorem identicalUntilBad (P : SigmaProtocol X Y T C Z) (key : X × Y) : + IdenticalUntilBad (realHandler (M := M) P key) (programHandler P key) + fun st => st.2 = true where + agree q st _ a st' hst' := by + cases q with + | inr x => rfl + | inl m => + simp only [realHandler, programHandler, PMF.bind_apply] + refine tsum_congr fun ts => congrArg (_ * ·) ?_ + cases hlookup : st.1.1.lookup (m, ts.1) with + | some c => + refine ((PMF.apply_eq_zero_iff _ _).mpr fun hx => ?_).trans + ((PMF.apply_eq_zero_iff _ _).mpr fun hx => ?_).symm <;> + · obtain ⟨r, -, hr⟩ := (PMF.mem_support_map_iff _ _ _).mp hx + exact hst' (by rw [← (Prod.mk.inj hr).2]; simp) + | none => + rw [oracle, memoize_of_none _ _ _ hlookup] + simp only [PMF.monad_bind_eq_bind, PMF.monad_pure_eq_pure, PMF.map_bind, PMF.pure_map] + exact DFunLike.congr_fun (PMF.bind_pure_comp _ _) _ + absorb_first q st hst x hx := by + cases q with + | inl m => + obtain ⟨ts, -, hx⟩ := (PMF.mem_support_bind_iff _ _ _).mp hx + obtain ⟨r, -, rfl⟩ := (PMF.mem_support_map_iff _ _ _).mp hx + simp [hst] + | inr x' => + obtain ⟨r, -, rfl⟩ := (PMF.mem_support_map_iff _ _ _).mp hx + exact hst + absorb_second q st hst x hx := by + cases q with + | inl m => + obtain ⟨ts, -, hx⟩ := (PMF.mem_support_bind_iff _ _ _).mp hx + obtain ⟨c, -, rfl⟩ := (PMF.mem_support_map_iff _ _ _).mp hx + simp [hst] + | inr x' => + obtain ⟨r, -, rfl⟩ := (PMF.mem_support_map_iff _ _ _).mp hx + exact hst + +omit [Fintype C] [Nonempty C] in +open scoped ENNReal in +/-- With `δ`-unpredictable commitments, a commitment hits one of the points of a table, for a +fixed message, with probability at most `δ` times the table's length. -/ +private theorem toOuterMeasure_lookup_le (P : SigmaProtocol X Y T C Z) (key : X × Y) + {δ : ℝ≥0∞} (hcommit : ∀ t, (P.commit key.1 key.2).map Prod.fst t ≤ δ) (m : M) + (cache : List ((M × T) × C)) : + (P.commit key.1 key.2).toOuterMeasure {ts | (cache.lookup (m, ts.1)).isSome} ≤ + cache.length * δ := by + induction cache with + | nil => simp + | cons e rest ih => + obtain ⟨⟨m', t'⟩, c⟩ := e + calc (P.commit key.1 key.2).toOuterMeasure + {ts | ((((m', t'), c) :: rest).lookup (m, ts.1)).isSome} + ≤ (P.commit key.1 key.2).toOuterMeasure + ({ts | ts.1 = t'} ∪ {ts | (rest.lookup (m, ts.1)).isSome}) := by + refine (P.commit key.1 key.2).toOuterMeasure.mono fun ts hts => ?_ + have hts : ((((m', t'), c) :: rest).lookup (m, ts.1)).isSome = true := hts + rw [List.lookup_cons] at hts + by_cases h : (m, ts.1) = (m', t') + · exact Or.inl (Prod.ext_iff.mp h).2 + · rw [beq_false_of_ne h] at hts + exact Or.inr hts + _ ≤ (P.commit key.1 key.2).toOuterMeasure {ts | ts.1 = t'} + + (P.commit key.1 key.2).toOuterMeasure {ts | (rest.lookup (m, ts.1)).isSome} := + MeasureTheory.measure_union_le _ _ + _ ≤ δ + rest.length * δ := by + refine add_le_add ?_ ih + rw [show {ts : T × P.State | ts.1 = t'} = Prod.fst ⁻¹' {t'} from rfl, + ← PMF.toOuterMeasure_map_apply, PMF.toOuterMeasure_apply_singleton] + exact hcommit t' + _ = (((m', t'), c) :: rest).length * δ := by + rw [List.length_cons, Nat.cast_add, Nat.cast_one] + ring + +open scoped ENNReal in +/-- With `δ`-unpredictable commitments, the flag of a forger making at most `Q` calls is raised +with probability at most `C(Q, 2) · δ`. -/ +private theorem toOuterMeasure_flag_le (P : SigmaProtocol X Y T C Z) (key : X × Y) + {δ : ℝ≥0∞} (hcommit : ∀ t, (P.commit key.1 key.2).map Prod.fst t ≤ δ) {α : Type} + {program : OracleComp (ForgerSpec M (M × T) (T × Z) C) α} {Q : ℕ} + (hQ : IsQueryBounded program Q) : + ((interpret (realHandler P key) program).run (([], []), false)).toOuterMeasure + {x | x.2.2 = true} ≤ Q.choose 2 * δ := by + have h := toOuterMeasure_bad_le (handler := realHandler P key) (bad := fun st => st.2 = true) + (fun st => st.1.1.length * δ) δ ?_ ?_ hQ (s := (([], []), false)) (by simp) + · simpa using h + · intro q st hst + cases q with + | inl m => + rw [realHandler, PMF.toOuterMeasure_bind_apply] + calc ∑' ts, (P.commit key.1 key.2) ts * + ((oracle C (m, ts.1) st.1.1).map fun r => ((ts.1, P.respond key.1 key.2 ts.2 r.1), + ((r.2, m :: st.1.2), st.2 || (st.1.1.lookup (m, ts.1)).isSome))).toOuterMeasure + {x | x.2.2 = true} + ≤ ∑' ts, (P.commit key.1 key.2) ts * + {ts : T × P.State | (st.1.1.lookup (m, ts.1)).isSome}.indicator 1 ts := by + refine ENNReal.tsum_le_tsum fun ts => mul_le_mul_of_nonneg_left ?_ zero_le + by_cases hts : (st.1.1.lookup (m, ts.1)).isSome + · rw [Set.indicator_of_mem (show ts ∈ {ts : T × P.State | + (st.1.1.lookup (m, ts.1)).isSome} from hts), Pi.one_apply] + exact Probability.PMF.toOuterMeasure_le_one _ _ + · rw [Set.indicator_of_notMem (show ts ∉ {ts : T × P.State | + (st.1.1.lookup (m, ts.1)).isSome} from hts)] + refine le_of_eq ((PMF.toOuterMeasure_apply_eq_zero_iff _ _).mpr ?_) + refine Set.disjoint_left.mpr fun x hx hbad => ?_ + obtain ⟨r, -, rfl⟩ := (PMF.mem_support_map_iff _ _ _).mp hx + simp_all + _ = (P.commit key.1 key.2).toOuterMeasure + {ts | (st.1.1.lookup (m, ts.1)).isSome} := by + rw [PMF.toOuterMeasure_apply] + refine tsum_congr fun ts => ?_ + by_cases hts : (st.1.1.lookup (m, ts.1)).isSome + · rw [Set.indicator_of_mem (show ts ∈ {ts : T × P.State | + (st.1.1.lookup (m, ts.1)).isSome} from hts), + Set.indicator_of_mem (show ts ∈ {ts : T × P.State | + (st.1.1.lookup (m, ts.1)).isSome} from hts), Pi.one_apply, mul_one] + · rw [Set.indicator_of_notMem (show ts ∉ {ts : T × P.State | + (st.1.1.lookup (m, ts.1)).isSome} from hts), + Set.indicator_of_notMem (show ts ∉ {ts : T × P.State | + (st.1.1.lookup (m, ts.1)).isSome} from hts), mul_zero] + _ ≤ st.1.1.length * δ := toOuterMeasure_lookup_le P key hcommit m st.1.1 + | inr x => + refine le_of_eq_of_le ((PMF.toOuterMeasure_apply_eq_zero_iff _ _).mpr ?_) zero_le + refine Set.disjoint_left.mpr fun y hy hbad => hst ?_ + obtain ⟨r, -, rfl⟩ := (PMF.mem_support_map_iff _ _ _).mp hy + exact hbad + · intro q st _ x hx _ + have hlen : x.2.1.1.length ≤ st.1.1.length + 1 := by + cases q with + | inl m => + obtain ⟨ts, -, hx⟩ := (PMF.mem_support_bind_iff _ _ _).mp hx + obtain ⟨r, hr, rfl⟩ := (PMF.mem_support_map_iff _ _ _).mp hx + exact length_le_of_mem_support_oracle hr + | inr x' => + obtain ⟨r, hr, rfl⟩ := (PMF.mem_support_map_iff _ _ _).mp hx + exact length_le_of_mem_support_oracle hr + calc (x.2.1.1.length : ℝ≥0∞) * δ ≤ ((st.1.1.length + 1 : ℕ) : ℝ≥0∞) * δ := by + gcongr + _ = st.1.1.length * δ + δ := by + rw [Nat.cast_add, Nat.cast_one, add_mul, one_mul] + +/-- Forgetting the flag, the programming signer is the simulator's signer, by special HVZK. -/ +private theorem programHandler_map {P : SigmaProtocol X Y T C Z} {R : X → Y → Prop} + {simulate : Y → C → PMF (T × Z)} (hzk : P.SpecialHVZK R simulate) {key : X × Y} + (hkey : R key.1 key.2) (q : M ⊕ (M × T)) (st : GameState M T C × Bool) : + (programHandler P key q st).map (fun x => (x.1, x.2.1)) = + (simulateConversation simulate key.2).bind fun v => simulatedHandler v q st.1 := by + cases q with + | inl m => + simp only [programHandler, simulatedHandler, simulateConversation, PMF.monad_bind_eq_bind, + PMF.monad_pure_eq_pure, PMF.map_bind, PMF.map_comp, PMF.bind_bind, PMF.pure_bind, + hzk.transcript_eq key.1 key.2 hkey, SigmaProtocol.transcript, PMF.bind_map, + Function.comp_def] + rw [PMF.bind_comm] + rfl + | inr x => + simp only [programHandler, simulatedHandler, PMF.bind_const, PMF.map_comp] + rfl + +/-! ### The reduction simulates the game -/ + +namespace FiatShamir + +/-- The game's view of the reduction's state: the table without positions, the signed messages, +and the unused transcripts. -/ +private def represent (st : ReductionState M T C Z) : GameState M T C × List (T × C × Z) := + ((st.table.map fun e => (e.1, e.2.1), st.signed), st.transcripts) + +omit [Fintype C] [Nonempty C] in +/-- Forgetting positions commutes with looking up a point. -/ +private theorem lookup_map_table (table : List ((M × T) × C × Option ℕ)) (x : M × T) : + (table.map fun e => (e.1, e.2.1)).lookup x = (table.lookup x).map Prod.fst := by + induction table with + | nil => rfl + | cons e rest ih => + obtain ⟨k, b⟩ := e + cases hxk : x == k <;> simp [List.lookup_cons, hxk, ih] + +variable [Nonempty T] [Nonempty Z] + +omit [Fintype C] in +/-- A signing call of the reduction's handler. -/ +private theorem run_reductionHandler_inl (m : M) (st : ReductionState M T C Z) : + (reductionHandler (.inl m)).run st = + pure (((st.transcripts.headD (Classical.arbitrary _)).1, + (st.transcripts.headD (Classical.arbitrary _)).2.2), + ⟨((m, (st.transcripts.headD (Classical.arbitrary _)).1), + (st.transcripts.headD (Classical.arbitrary _)).2.1, none) :: st.table, m :: st.signed, + st.count, st.transcripts.tail⟩) := rfl + +omit [Fintype C] in +/-- A hash call of the reduction's handler on a point of the table. -/ +private theorem run_reductionHandler_inr_some {x : M × T} {st : ReductionState M T C Z} + {e : C × Option ℕ} (h : st.table.lookup x = some e) : + (reductionHandler (.inr x)).run st = + pure (e.1, ⟨st.table, st.signed, st.count, st.transcripts.tail⟩) := by + simp only [reductionHandler, StateT.run, h] + +omit [Fintype C] in +/-- A hash call of the reduction's handler on a new point. -/ +private theorem run_reductionHandler_inr_none {x : M × T} {st : ReductionState M T C Z} + (h : st.table.lookup x = none) : + (reductionHandler (.inr x)).run st = + (fun c => (c, ⟨(x, c, some st.count) :: st.table, st.signed, st.count + 1, + st.transcripts.tail⟩)) <$> OracleComp.query x := by + simp only [reductionHandler, StateT.run, h] + +omit [DecidableEq M] [DecidableEq T] [Nonempty T] in +/-- A returned value, with the oracle answered uniformly and counted, makes no call. -/ +private theorem run_interpret_countingUniform_pure {β : Type} (b : β) (n : ℕ) : + (interpret countingUniform (pure b : OracleComp (fun _ : M × T => C) β)).run n = + PMF.pure (b, n) := rfl + +omit [DecidableEq M] [DecidableEq T] [Nonempty T] in +/-- A counted uniform answer. -/ +private theorem run_countingUniform (x : M × T) (n : ℕ) : + (countingUniform (H := C) x).run n = (PMF.uniformOfFintype C).map (·, n + 1) := rfl + +/-- One call of the reduction's handler, with its oracle answered uniformly and counted, is a call +of the simulator's signer in the game's view. -/ +private theorem combined_step (q : M ⊕ (M × T)) (s : ReductionState M T C Z × ℕ) : + ((fun result => (result.1.1, result.1.2, result.2)) <$> + (interpret countingUniform ((reductionHandler q).run s.1)).run s.2).map + (fun x => (x.1, represent x.2.1)) = + withSampleList (Classical.arbitrary _) simulatedHandler q (represent s.1) := by + cases q with + | inl m => + rw [run_reductionHandler_inl, run_interpret_countingUniform_pure] + simp only [PMF.monad_map_eq_map, PMF.pure_map, withSampleList, simulatedHandler, represent] + rfl + | inr x => + cases h : s.1.table.lookup x with + | some e => + have hcache : (represent s.1).1.1.lookup x = some e.1 := by + rw [represent, lookup_map_table, h] + rfl + rw [run_reductionHandler_inr_some h] + simp only [run_interpret_countingUniform_pure, PMF.monad_map_eq_map, PMF.pure_map, + withSampleList, simulatedHandler] + rw [oracle, memoize_of_some _ _ _ _ hcache] + simp only [PMF.monad_pure_eq_pure, PMF.pure_map] + rfl + | none => + have hcache : (represent s.1).1.1.lookup x = none := by + rw [represent, lookup_map_table, h] + rfl + rw [run_reductionHandler_inr_none h] + simp only [interpret_map, interpret_query, StateT.run_map, PMF.monad_map_eq_map, + withSampleList, simulatedHandler] + rw [oracle, memoize_of_none _ _ _ hcache] + simp only [run_countingUniform, PMF.monad_bind_eq_bind, PMF.monad_pure_eq_pure, + ← PMF.bind_pure_comp, PMF.bind_bind, PMF.pure_bind, Function.comp_apply] + rfl + +omit [Nonempty T] [Nonempty Z] in +/-- The reduction's final check, with its oracle answered uniformly, wins exactly when the game's +final check does. -/ +private theorem map_run_finish (P : SigmaProtocol X Y T C Z) (y : Y) (a : M × (T × Z)) + (st : ReductionState M T C Z) (n : ℕ) : + ((interpret countingUniform (finish P y (a, st))).run n).map (fun run => run.1.2.1) = + finishGame P y (a, (represent st).1) := by + cases h : st.table.lookup (a.1, a.2.1) with + | some e => + have hcache : (represent st).1.1.lookup (a.1, a.2.1) = some e.1 := by + rw [represent, lookup_map_table, h] + rfl + simp only [finish, h, run_interpret_countingUniform_pure, PMF.pure_map, finishGame] + rw [oracle, memoize_of_some _ _ _ _ hcache] + simp only [PMF.monad_pure_eq_pure, PMF.pure_map] + rfl + | none => + have hcache : (represent st).1.1.lookup (a.1, a.2.1) = none := by + rw [represent, lookup_map_table, h] + rfl + simp only [finish, h, interpret_map, interpret_query, StateT.run_map, PMF.monad_map_eq_map, + finishGame] + rw [oracle, memoize_of_none _ _ _ hcache] + simp only [run_countingUniform, PMF.monad_bind_eq_bind, PMF.monad_pure_eq_pure, + ← PMF.bind_pure_comp, PMF.bind_bind, PMF.pure_bind, Function.comp_apply] + rfl + +/-- **The reduction simulates the game.** With its oracle answered uniformly, the forking program +wins exactly when the forger wins against the simulator's signer with the same transcripts. -/ +private theorem map_run_forkingProgram (P : SigmaProtocol X Y T C Z) + (A : Forger Y M (T × Z) (M × T) C) (s : Y × A.Coins × List (T × C × Z)) : + ((interpret countingUniform (forkingProgram P A s)).run 0).map (fun run => run.1.2.1) = + ((interpret (withSampleList (Classical.arbitrary _) simulatedHandler) + (A.forge s.1 s.2.1)).run (([], []), s.2.2)).bind fun x => + finishGame P s.1 (x.1, x.2.1) := by + have hsim := run_interpret_map_state _ + (withSampleList (Classical.arbitrary _) simulatedHandler) (fun s => represent s.1) + combined_step (A.forge s.1 s.2.1) (⟨[], [], 0, s.2.2⟩, 0) + rw [show represent (⟨[], [], 0, s.2.2⟩ : ReductionState M T C Z) = (([], []), s.2.2) from rfl] + at hsim + rw [forkingProgram, interpret_bind, StateT.run_bind, run_interpret_run_interpret, ← hsim] + simp only [PMF.monad_bind_eq_bind, PMF.monad_map_eq_map, PMF.map_bind, PMF.bind_map, + Function.comp_def] + exact congrArg (PMF.bind _) (funext fun r => map_run_finish P s.1 r.1 r.2.1 r.2.2) + +/-! ### The reduction's runs on fixed answers -/ + +omit [Fintype C] [Nonempty C] [Nonempty T] [Nonempty Z] in +/-- The final check on a forgery whose point is in the table. -/ +private theorem finish_of_some {P : SigmaProtocol X Y T C Z} {y : Y} + {forged : (M × (T × Z)) × ReductionState M T C Z} {e : C × Option ℕ} + (h : forged.2.table.lookup (forged.1.1, forged.1.2.1) = some e) : + finish P y forged = pure (verdict P y forged e.1 e.2) := by + simp only [finish, h] + +omit [Fintype C] [Nonempty C] [Nonempty T] [Nonempty Z] in +/-- The final check on a forgery whose point is not in the table. -/ +private theorem finish_of_none {P : SigmaProtocol X Y T C Z} {y : Y} + {forged : (M × (T × Z)) × ReductionState M T C Z} + (h : forged.2.table.lookup (forged.1.1, forged.1.2.1) = none) : + finish P y forged = (fun c => verdict P y forged c (some forged.2.count)) <$> + OracleComp.query (forged.1.1, forged.1.2.1) := by + simp only [finish, h] + +/-- The invariant of the reduction's run on a list of answers, given the queries asked so far: the +count is their number; an entry with a position records the query at that position and its +answer; an entry without one is for a signed message. -/ +private def Consistent (answers : List C) (st : ReductionState M T C Z) + (queries : List (M × T)) : Prop := + st.count = queries.length ∧ + (∀ x c i, (x, c, some i) ∈ st.table → + queries[i]? = some x ∧ answers.getD i (Classical.arbitrary C) = c) ∧ + ∀ x c, (x, c, none) ∈ st.table → x.1 ∈ st.signed + +omit [Fintype C] in +/-- Every call of the reduction's handler preserves the invariant. -/ +private theorem consistent_step (answers : List C) (q : M ⊕ (M × T)) + (st : ReductionState M T C Z) (queries : List (M × T)) + (h : Consistent answers st queries) : + Consistent answers (runWithAnswers (Classical.arbitrary C) ((reductionHandler q).run st) + (answers.drop queries.length)).1.2 + (queries ++ (runWithAnswers (Classical.arbitrary C) ((reductionHandler q).run st) + (answers.drop queries.length)).2) := by + obtain ⟨hcount, hpos, hsigned⟩ := h + cases q with + | inl m => + rw [run_reductionHandler_inl, runWithAnswers_pure, List.append_nil] + refine ⟨hcount, fun x c i hx => ?_, fun x c hx => ?_⟩ + · simp only [List.mem_cons, Prod.mk.injEq, reduceCtorEq, and_false, false_or] at hx + exact hpos x c i hx + · simp only [List.mem_cons, Prod.mk.injEq] at hx + rcases hx with ⟨rfl, -, -⟩ | hx + · exact List.mem_cons_self + · exact List.mem_cons_of_mem _ (hsigned x c hx) + | inr x => + cases hl : st.table.lookup x with + | some e => + rw [run_reductionHandler_inr_some hl, runWithAnswers_pure, List.append_nil] + exact ⟨hcount, hpos, hsigned⟩ + | none => + rw [run_reductionHandler_inr_none hl, runWithAnswers_map_query] + refine ⟨by simp [hcount], fun x' c i hx => ?_, fun x' c hx => ?_⟩ + · simp only [List.mem_cons, Prod.mk.injEq, Option.some.injEq] at hx + rcases hx with ⟨rfl, rfl, rfl⟩ | hx + · rw [hcount, List.getElem?_concat_length, List.getD_eq_getElem?_getD, + List.headD_eq_head?_getD, List.head?_drop] + exact ⟨rfl, rfl⟩ + · obtain ⟨hq, hc⟩ := hpos x' c i hx + have hi : i < queries.length := (List.getElem?_eq_some_iff.mp hq).1 + exact ⟨by rw [List.getElem?_append_left hi, hq], hc⟩ + · simp only [List.mem_cons, Prod.mk.injEq, reduceCtorEq, and_false, false_or] at hx + exact hsigned x' c hx + +omit [Fintype C] in +/-- **The reduction's run on fixed answers.** On any list of answers, a winning forgery names a +position, and a named position is that of the query for the forgery's point, answered there with +the forgery's challenge, and the forgery is accepting. -/ +private theorem runWithAnswers_forkingProgram (P : SigmaProtocol X Y T C Z) + (A : Forger Y M (T × Z) (M × T) C) (s : Y × A.Coins × List (T × C × Z)) (answers : List C) + {out : (Option ℕ × Bool × (M × T) × C × Z) × List (M × T)} + (hout : runWithAnswers (Classical.arbitrary C) (forkingProgram P A s) answers = out) : + (out.1.2.1 = true → out.1.1.isSome) ∧ + ∀ j, out.1.1 = some j → out.2[j]? = some out.1.2.2.1 ∧ + answers.getD j (Classical.arbitrary C) = out.1.2.2.2.1 ∧ + P.verify s.1 out.1.2.2.1.2 out.1.2.2.2.1 out.1.2.2.2.2 = true := by + have hinv := runWithAnswers_run_interpret_invariant (Classical.arbitrary C) reductionHandler + answers (Consistent answers) (consistent_step answers) (A.forge s.1 s.2.1) + ⟨[], [], 0, s.2.2⟩ [] ⟨rfl, by simp, by simp⟩ + simp only [List.length_nil, List.drop_zero, List.nil_append] at hinv + rw [forkingProgram, runWithAnswers_bind] at hout + subst hout + generalize runWithAnswers (Classical.arbitrary C) + ((interpret reductionHandler (A.forge s.1 s.2.1)).run ⟨[], [], 0, s.2.2⟩) answers = r at hinv ⊢ + obtain ⟨⟨forged, st⟩, queries⟩ := r + obtain ⟨hcount, hpos, hsigned⟩ := hinv + cases hl : st.table.lookup (forged.1, forged.2.1) with + | some e => + rw [finish_of_some hl, runWithAnswers_pure, List.append_nil] + obtain ⟨l₁, l₂, htable, -⟩ := List.lookup_eq_some_iff.mp hl + have hmem : ((forged.1, forged.2.1), e.1, e.2) ∈ st.table := by + rw [htable] + exact List.mem_append_right _ List.mem_cons_self + obtain ⟨c, position⟩ := e + cases position with + | none => + have hm := hsigned _ _ hmem + simp [verdict, hm] + | some i => + obtain ⟨hq, hc⟩ := hpos _ _ _ hmem + refine ⟨fun hwin => ?_, fun j hj => ?_⟩ + · simp only [verdict] at hwin ⊢ + simpa using hwin + · simp only [verdict] at hj ⊢ + split_ifs at hj with hwin + · cases hj + exact ⟨hq, hc, (Bool.and_eq_true _ _).mp hwin |>.1⟩ + | none => + rw [finish_of_none hl, runWithAnswers_map_query] + refine ⟨fun hwin => ?_, fun j hj => ?_⟩ + · simp only [verdict] at hwin ⊢ + simpa using hwin + · simp only [verdict] at hj ⊢ + split_ifs at hj with hwin + · cases hj + refine ⟨by rw [hcount, List.getElem?_concat_length], ?_, + (Bool.and_eq_true _ _).mp hwin |>.1⟩ + rw [hcount, List.getD_eq_getElem?_getD, List.headD_eq_head?_getD, List.head?_drop] + +omit [Fintype C] in +/-- The forking program asks at most one query per call of the forger, and one more to check the +forgery. -/ +private theorem isQueryBounded_forkingProgram (P : SigmaProtocol X Y T C Z) + (A : Forger Y M (T × Z) (M × T) C) {Q : ℕ} (hQ : ∀ y s, IsQueryBounded (A.forge y s) Q) + (s : Y × A.Coins × List (T × C × Z)) : IsQueryBounded (forkingProgram P A s) (Q + 1) := by + have hhandler (q : M ⊕ (M × T)) (st : ReductionState M T C Z) : + IsQueryBounded ((reductionHandler q).run st) 1 := by + cases q with + | inl m => + rw [run_reductionHandler_inl] + exact .pure _ _ + | inr x => + cases hl : st.table.lookup x with + | some e => + rw [run_reductionHandler_inr_some hl] + exact .pure _ _ + | none => + rw [run_reductionHandler_inr_none hl] + exact .liftBind _ _ 0 fun _ => .pure _ 0 + have hforge := (hQ s.1 s.2.1).run_interpret hhandler ⟨[], [], 0, s.2.2⟩ + rw [Nat.mul_one] at hforge + refine hforge.bind fun forged => ?_ + cases hl : forged.2.table.lookup (forged.1.1, forged.1.2.1) with + | some e => + rw [finish_of_some hl] + exact .pure _ _ + | none => + rw [finish_of_none hl] + exact .liftBind _ _ 0 fun _ => .pure _ 0 + +/-- With its oracle answered uniformly, the forking program wins at most as often as it validly +names a query. -/ +private theorem map_run_le_accept (P : SigmaProtocol X Y T C Z) + (A : Forger Y M (T × Z) (M × T) C) {Q : ℕ} (hQ : ∀ y s, IsQueryBounded (A.forge y s) Q) + (s : Y × A.Coins × List (T × C × Z)) : + ((interpret countingUniform (forkingProgram P A s)).run 0).map (fun run => run.1.2.1) true ≤ + ((interpret countingUniform (forkingProgram P A s)).run 0).bind + (fun run => PMF.pure (validIndex (Q + 1) run.2 run.1.1).isSome) true := by + have hbound := isQueryBounded_forkingProgram P A hQ s + rw [run_interpret_countingUniform_eq (Classical.arbitrary C) _ + (hbound.hasQueryBounds (size := fun _ => 0) (maxSize := 0) fun _ => le_rfl)] + simp only [← PMF.bind_pure_comp, PMF.bind_bind, PMF.pure_bind, Function.comp_def] + refine Probability.PMF.bind_apply_mono_on_support _ _ fun h _ => ?_ + obtain ⟨hwin, hnamed⟩ := runWithAnswers_forkingProgram P A s (List.ofFn h) rfl + by_cases hw : (runWithAnswers (Classical.arbitrary C) (forkingProgram P A s) + (List.ofFn h)).1.2.1 = true + · obtain ⟨j, hj⟩ := Option.isSome_iff_exists.mp (hwin hw) + have hlt : j < (runWithAnswers (Classical.arbitrary C) (forkingProgram P A s) + (List.ofFn h)).2.length := (List.getElem?_eq_some_iff.mp (hnamed j hj).1).1 + have hle := hbound.length_runWithAnswers_le (Classical.arbitrary C) (List.ofFn h) + have hvalid : (validIndex (Q + 1) (0 + (runWithAnswers (Classical.arbitrary C) + (forkingProgram P A s) (List.ofFn h)).2.length) (runWithAnswers (Classical.arbitrary C) + (forkingProgram P A s) (List.ofFn h)).1.1).isSome = true := by + rw [hj, zero_add] + simp only [validIndex, Option.bind_some] + split_ifs with hc + · rfl + · exact absurd ⟨by omega, hlt⟩ hc + rw [hw, hvalid] + · rw [Bool.eq_false_iff.mpr hw] + simp + +omit [DecidableEq M] [DecidableEq T] [Fintype C] [Nonempty C] in +/-- The entry of a list of `n` values at a position below `n`. -/ +private theorem getD_ofFn {n : ℕ} (h : Fin n → C) (j : Fin n) (d : C) : + (List.ofFn h).getD j d = h j := by + simp [List.getD_eq_getElem?_getD] + +variable [DecidableEq C] + +/-- **Extraction from a successful fork.** Both runs of a successful fork name the same query, +for the same point, answered with two different challenges, and both forgeries are accepting; +special soundness turns them into a witness. -/ +private theorem fork_le_oneWayGame [Nonempty X] {P : SigmaProtocol X Y T C Z} + {keyGen : PMF (X × Y)} {R : X → Y → Prop} [∀ x y, Decidable (R x y)] + {extract : Y → T → C → Z → C → Z → X} (hsound : P.SpecialSoundOn keyGen R extract) + (simulate : Y → C → PMF (T × Z)) (A : Forger Y M (T × Z) (M × T) C) (Q : ℕ) : + (Forking.fork (keyGen.bind fun key => coins simulate A Q key.2) + (forkingAlgorithm (Classical.arbitrary C) (Q + 1) (forkingProgram P A))).map + Option.isSome true ≤ + oneWayGame keyGen R (reduction P simulate extract A Q) true := by + have hfork : Forking.fork (keyGen.bind fun key => coins simulate A Q key.2) + (forkingAlgorithm (Classical.arbitrary C) (Q + 1) (forkingProgram P A)) = + keyGen.bind fun key => Forking.fork (coins simulate A Q key.2) + (forkingAlgorithm (Classical.arbitrary C) (Q + 1) (forkingProgram P A)) := by + simp only [Forking.fork, PMF.monad_bind_eq_bind, PMF.bind_bind] + rw [hfork, PMF.map_bind] + simp only [oneWayGame, reduction, PMF.monad_bind_eq_bind, PMF.monad_pure_eq_pure, PMF.bind_map] + refine Probability.PMF.bind_apply_mono_on_support _ _ fun key hkey => ?_ + rw [← PMF.bind_pure_comp] + refine Probability.PMF.bind_apply_mono_on_support _ _ fun result hresult => ?_ + rcases result with _ | ⟨j, out, out'⟩ + · simp + · obtain ⟨s, hs, h, h', -, hne, hout, hout', hj, hj', -, query, hq, hq'⟩ := + mem_support_fork hresult + simp only [coins, PMF.monad_bind_eq_bind, PMF.monad_pure_eq_pure, PMF.mem_support_bind_iff, + PMF.mem_support_pure_iff] at hs + obtain ⟨c, -, trs, -, rfl⟩ := hs + obtain ⟨-, hnamed⟩ := runWithAnswers_forkingProgram P A _ (List.ofFn h) hout.symm + obtain ⟨-, hnamed'⟩ := runWithAnswers_forkingProgram P A _ (List.ofFn h') hout'.symm + obtain ⟨hp, hc, hv⟩ := hnamed j hj + obtain ⟨hp', hc', hv'⟩ := hnamed' j hj' + rw [getD_ofFn] at hc hc' + have hpoint : out.1.2.2.1 = out'.1.2.2.1 := + Option.some.inj (hp.symm.trans (hq.trans (hq'.symm.trans hp'))) + have hR := hsound key hkey out.1.2.2.1.2 out.1.2.2.2.1 out.1.2.2.2.2 out'.1.2.2.2.1 + out'.1.2.2.2.2 (by rw [← hc, ← hc']; exact hne) hv (by rw [hpoint]; exact hv') + simp [hR] + +omit [DecidableEq C] in +/-- If every continuation accepts at most `K` more often than another, then so does the whole +experiment. -/ +private theorem bind_apply_le_add {α β : Type} {μ : PMF α} {f g : α → PMF β} {b : β} + {K : ENNReal} (h : ∀ a ∈ μ.support, f a b ≤ g a b + K) : + (μ.bind f) b ≤ (μ.bind g) b + K := by + simp only [PMF.bind_apply] + calc ∑' a, μ a * f a b ≤ ∑' a, μ a * (g a b + K) := by + refine ENNReal.tsum_le_tsum fun a => ?_ + by_cases ha : a ∈ μ.support + · exact mul_le_mul_of_nonneg_left (h a ha) zero_le + · rw [(PMF.apply_eq_zero_iff _ _).mpr ha, zero_mul, zero_mul] + _ = ∑' a, μ a * g a b + K := by + simp only [mul_add, ENNReal.tsum_add, ENNReal.tsum_mul_right, PMF.tsum_coe, one_mul] + +omit [DecidableEq C] in +/-- **The game hops** for one key and one choice of the forger's coins: the experiment wins at +most as often as the forking program, with presampled transcripts, plus `C(Q, 2) · δ`. -/ +private theorem run_bind_finishGame_le {P : SigmaProtocol X Y T C Z} {keyGen : PMF (X × Y)} + {R : X → Y → Prop} {simulate : Y → C → PMF (T × Z)} (hzk : P.SpecialHVZK R simulate) + {key : X × Y} (hkey : R key.1 key.2) {δ : ENNReal} + (hcommit : ∀ t, (P.commit key.1 key.2).map Prod.fst t ≤ δ) + (A : Forger Y M (T × Z) (M × T) C) {Q : ℕ} (hQ : ∀ y s, IsQueryBounded (A.forge y s) Q) + (c : A.Coins) : + ((interpret (handler (fiatShamir P keyGen) key) (A.forge key.2 c)).run ([], [])).bind + (finishGame P key.2) true ≤ + ((PMF.iid (simulateConversation simulate key.2) Q).map List.ofFn).bind (fun trs => + ((interpret countingUniform (forkingProgram P A (key.2, c, trs))).run 0).map + fun run => run.1.2.1) true + Q.choose 2 * δ := by + have h0 := run_interpret_map_state (realHandler P key) (handler (fiatShamir P keyGen) key) + Prod.fst (realHandler_map P keyGen key) (A.forge key.2 c) (([], []), false) + have h1 := run_interpret_map_state (programHandler P key) + (fun q st => (simulateConversation simulate key.2).bind fun v => simulatedHandler v q st) + Prod.fst (programHandler_map hzk hkey) (A.forge key.2 c) (([], []), false) + have h2 := (hQ key.2 c).run_interpret_withSampleList (simulateConversation simulate key.2) + (Classical.arbitrary _) simulatedHandler ([], []) + rw [← h0, PMF.bind_map] + refine ((identicalUntilBad P key).bind_apply_le _ _ _ _).trans + (add_le_add (le_of_eq ?_) (toOuterMeasure_flag_le P key hcommit (hQ key.2 c))) + rw [← PMF.bind_map, h1, ← h2, PMF.bind_bind] + refine congrArg (fun p : PMF Bool => p true) (congrArg (PMF.bind _) (funext fun trs => ?_)) + rw [PMF.bind_map, map_run_forkingProgram] + rfl + +end FiatShamir + +open FiatShamir in +open scoped NNReal in +/-- **Security of Fiat–Shamir signatures** ([BonehShoup2023], Theorem 19.16 with Equation 19.21, +via [BellareNeven2006], Lemma 1). Let the Sigma protocol be special sound on the generated keys +with extractor `extract`, special HVZK with simulator `simulate`, and have `δ`-unpredictable +commitments, and let the key generator produce pairs in the relation. A forger making at most `Q` +signing and hash calls in total wins the random-oracle EUF-CMA experiment with probability at +most `C(Q, 2) · δ + (Q + 1) / N + √((Q + 1) · ε')`, where `N` is the number of challenges and `ε'` +is the probability that the reduction outputs a witness for a generated statement. -/ +theorem succProbability_eufCmaGame_le [Nonempty X] [Nonempty T] [Nonempty Z] [DecidableEq C] + {P : SigmaProtocol X Y T C Z} {keyGen : PMF (X × Y)} {R : X → Y → Prop} + [∀ x y, Decidable (R x y)] {extract : Y → T → C → Z → C → Z → X} + {simulate : Y → C → PMF (T × Z)} {δ : ℝ≥0} + (hkey : ∀ key ∈ keyGen.support, R key.1 key.2) (hsound : P.SpecialSoundOn keyGen R extract) + (hzk : P.SpecialHVZK R simulate) + (hcommit : ∀ key ∈ keyGen.support, ∀ t, (P.commit key.1 key.2).map Prod.fst t ≤ δ) + (A : Forger Y M (T × Z) (M × T) C) {Q : ℕ} + (hQ : ∀ y s, IsQueryBounded (A.forge y s) Q) : + (Game.succProbability (eufCmaGame (fiatShamir P keyGen) A) : ℝ) ≤ + Q.choose 2 * δ + (Q + 1) / Fintype.card C + + √((Q + 1) * Game.succProbability + (oneWayGame keyGen R (reduction P simulate extract A Q))) := by + classical + set first := keyGen.bind fun key => coins simulate A Q key.2 with hfirst + have hA : eufCmaGame (fiatShamir P keyGen) A true ≤ + first.bind (fun s => ((interpret countingUniform (forkingProgram P A s)).run 0).map + fun run => run.1.2.1) true + Q.choose 2 * (δ : ENNReal) := by + rw [eufCmaGame_fiatShamir, hfirst] + simp only [coins, PMF.monad_bind_eq_bind, PMF.monad_pure_eq_pure, PMF.bind_bind, + PMF.pure_bind] + refine bind_apply_le_add fun key hkey' => bind_apply_le_add fun c _ => ?_ + exact run_bind_finishGame_le hzk (hkey key hkey') (hcommit key hkey') A hQ c + have hB : first.bind (fun s => ((interpret countingUniform (forkingProgram P A s)).run 0).map + fun run => run.1.2.1) true ≤ + first.bind (fun s => ((interpret countingUniform (forkingProgram P A s)).run 0).bind + fun run => PMF.pure (validIndex (Q + 1) run.2 run.1.1).isSome) true := + Probability.PMF.bind_apply_mono_on_support _ _ fun s _ => map_run_le_accept P A hQ s + have hC := le_add_sqrt_fork first (forkingProgram P A) (Classical.arbitrary C) + (fun s => (isQueryBounded_forkingProgram P A hQ s).hasQueryBounds (size := fun _ => 0) + (maxSize := 0) fun _ => le_rfl) + have hD := fork_le_oneWayGame (P := P) hsound simulate A Q + simp only [PMF.monad_bind_eq_bind, PMF.monad_pure_eq_pure] at hC + simp only [Game.succProbability, ENNReal.coe_toNNReal_eq_toReal] + have hK : (Q.choose 2 * (δ : ENNReal)).toReal = Q.choose 2 * δ := by + rw [ENNReal.toReal_mul, ENNReal.toReal_natCast, ENNReal.coe_toReal] + calc (eufCmaGame (fiatShamir P keyGen) A true).toReal + ≤ (first.bind (fun s => ((interpret countingUniform (forkingProgram P A s)).run 0).bind + fun run => PMF.pure (validIndex (Q + 1) run.2 run.1.1).isSome) true).toReal + + Q.choose 2 * δ := by + rw [← hK, ← ENNReal.toReal_add (PMF.apply_ne_top _ _) + (ENNReal.mul_ne_top (ENNReal.natCast_ne_top _) ENNReal.coe_ne_top)] + exact ENNReal.toReal_mono (ENNReal.add_ne_top.mpr ⟨PMF.apply_ne_top _ _, + ENNReal.mul_ne_top (ENNReal.natCast_ne_top _) ENNReal.coe_ne_top⟩) + (hA.trans (add_le_add hB le_rfl)) + _ ≤ ((Q + 1 : ℕ) / Fintype.card C + √((Q + 1 : ℕ) * ((Forking.fork first + (forkingAlgorithm (Classical.arbitrary C) (Q + 1) (forkingProgram P A))).map + Option.isSome true).toReal)) + Q.choose 2 * δ := add_le_add hC le_rfl + _ ≤ _ := by + push_cast + have hsqrt := Real.sqrt_le_sqrt (mul_le_mul_of_nonneg_left + (ENNReal.toReal_mono (PMF.apply_ne_top _ _) hD) (by positivity : (0 : ℝ) ≤ Q + 1)) + linarith + +end Cslib.Crypto.Protocols.SigmaProtocol diff --git a/ComplexityTests.lean b/ComplexityTests.lean index 0c013b883..b23902b64 100644 --- a/ComplexityTests.lean +++ b/ComplexityTests.lean @@ -90,6 +90,7 @@ import ComplexityTests.CountingSpace import ComplexityTests.CountingVerifier import ComplexityTests.Crypto.Bootstrapping import ComplexityTests.Crypto.Encryption +import ComplexityTests.Crypto.FiatShamir import ComplexityTests.Crypto.FixedKeySecurity import ComplexityTests.Crypto.Forking import ComplexityTests.Crypto.GMWPointwise diff --git a/ComplexityTests/Crypto/FiatShamir.lean b/ComplexityTests/Crypto/FiatShamir.lean new file mode 100644 index 000000000..8c2d0eaa7 --- /dev/null +++ b/ComplexityTests/Crypto/FiatShamir.lean @@ -0,0 +1,152 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +import Complexity.Crypto.Protocols.SigmaProtocol.FiatShamir +import Complexity.Crypto.Protocols.SigmaProtocol.SchnorrIdentification +import Complexity.Probability.PMF +import Mathlib.Tactic.LinearCombination +import Mathlib.Tactic.NormNum.Prime + +/-! +# Tests for Fiat–Shamir signatures + +Schnorr signatures in `ZMod 11`, with base `2`, are Fiat–Shamir signatures from Schnorr's +protocol: honest signatures verify, and the commitments are `1 / 11`-unpredictable. Discrete +logarithms are easy here: a forger that computes the witness and signs a message honestly, with +one hash call, always wins, so the security theorem makes the reduction compute discrete +logarithms with probability at least `81 / 242`. +-/ + +namespace ComplexityTests.Crypto.FiatShamir + +open Cslib Cslib.Probability Cslib.Crypto Cslib.Crypto.Protocols SigmaProtocol ROMSignature +open scoped NNReal + +instance : Fact (Nat.Prime 11) := ⟨by norm_num⟩ + +/-- Challenges are all of `ZMod 11`. -/ +abbrev ι : ZMod 11 ↪ ZMod 11 := Function.Embedding.refl _ + +/-- Schnorr signatures on `Bool` messages in `ZMod 11` with base `2`. -/ +noncomputable abbrev scheme := + fiatShamir (M := Bool) (schnorr ι (2 : ZMod 11)) (schnorrKeyGen 2) + +/-- Honest Schnorr signatures verify. -/ +example : scheme.Correct := + fiatShamir_correct schnorr_complete fun _ h => mem_support_schnorrKeyGen h + +/-- Schnorr commitments in `ZMod 11` with base `2` are `1 / 11`-unpredictable: the commitment +`r • 2` of a uniform `r` is uniform. -/ +theorem commit_unpredictable (key : ZMod 11 × ZMod 11) (t : ZMod 11) : + ((schnorr ι (2 : ZMod 11)).commit key.1 key.2).map Prod.fst t ≤ ((11 : ℝ≥0)⁻¹ : ℝ≥0) := by + have h2 : (2 : ZMod 11) ≠ 0 := by decide + have hmap : ((schnorr ι (2 : ZMod 11)).commit key.1 key.2).map Prod.fst = + (PMF.uniformOfFintype (ZMod 11)).map (Equiv.mulRight₀ (2 : ZMod 11) h2) := by + simp only [schnorr, linear, PMF.map_comp] + rfl + rw [hmap, PMF.uniformOfFintype_map_equiv, PMF.uniformOfFintype_apply, ZMod.card] + simp + +/-- The forger that computes the witness `6 • u` of `u` and signs `true` honestly, with one hash +call. -/ +noncomputable def knower : Forger (ZMod 11) Bool (ZMod 11 × ZMod 11) (Bool × ZMod 11) (ZMod 11) + where + Coins := ZMod 11 + coins := PMF.uniformOfFintype (ZMod 11) + forge u r := do + let c ← OracleComp.query (spec := ForgerSpec Bool (Bool × ZMod 11) (ZMod 11 × ZMod 11) + (ZMod 11)) (.inr (true, r • 2)) + return (true, (r • 2, r + c • (6 • u))) + +/-- The knowing forger always wins. -/ +theorem succProbability_knower : Game.succProbability (eufCmaGame scheme knower) = 1 := by + rw [Game.succProbability, ENNReal.toNNReal_eq_one_iff] + refine le_antisymm (PMF.coe_le_one _ _) ?_ + simp only [eufCmaGame, PMF.monad_bind_eq_bind, PMF.monad_pure_eq_pure] + refine PMF.le_bind_apply_on_support _ fun keys hkeys => ?_ + obtain ⟨key, hkey, rfl⟩ := (_root_.PMF.mem_support_map_iff _ _ _).mp hkeys + have hrel := mem_support_schnorrKeyGen hkey + refine PMF.le_bind_apply_on_support _ fun (r : ZMod 11) _ => ?_ + refine PMF.le_bind_apply_on_support _ fun forged hforged => ?_ + simp only [knower, OracleComp.interpret_bind, OracleComp.interpret_query, StateT.run_bind, + OracleComp.interpret_pure, PMF.monad_bind_eq_bind, PMF.mem_support_bind_iff, + StateT.run_pure, PMF.monad_pure_eq_pure, _root_.PMF.mem_support_pure_iff] at hforged + obtain ⟨answer, hanswer, rfl⟩ := hforged + change answer ∈ ((memoize (fun _ => PMF.uniformOfFintype (ZMod 11)) (true, r • (2 : ZMod 11)) + []).bind fun a => PMF.pure (a.1, a.2, ([] : List Bool))).support at hanswer + rw [memoize_of_none _ _ _ rfl] at hanswer + simp only [PMF.monad_bind_eq_bind, PMF.monad_pure_eq_pure, PMF.bind_bind, PMF.pure_bind, + PMF.mem_support_bind_iff, _root_.PMF.mem_support_pure_iff] at hanswer + obtain ⟨c, -, rfl⟩ := hanswer + refine PMF.le_bind_apply_on_support _ fun verified hverified => ?_ + simp only [scheme, fiatShamir, OracleComp.interpret_map, OracleComp.interpret_query, + StateT.run_map, PMF.monad_map_eq_map, _root_.PMF.mem_support_map_iff] at hverified + obtain ⟨v, hv, rfl⟩ := hverified + change v ∈ (memoize (fun _ => PMF.uniformOfFintype (ZMod 11)) (true, r • (2 : ZMod 11)) + [((true, r • 2), c)]).support at hv + rw [memoize_of_some _ _ _ _ List.lookup_cons_self, PMF.monad_pure_eq_pure, + _root_.PMF.mem_support_pure_iff] at hv + subst hv + have h11 : (11 : ZMod 11) = 0 := by decide + have haccept : (schnorr ι (2 : ZMod 11)).Accepts key.2 (r • 2) c (r + c • (6 • key.2)) := by + rw [schnorr_accepts_iff, ← hrel] + simp only [smul_eq_mul, Function.Embedding.refl_apply] + linear_combination (2 * c * key.1) * h11 + have hverify : (schnorr ι (2 : ZMod 11)).verify key.2 (r • 2) c (r + c • (6 • key.2)) = true := + haccept + simp only [hverify] + simp + +/-- The knowing forger makes one call. -/ +theorem knower_isQueryBounded (u r : ZMod 11) : OracleComp.IsQueryBounded (knower.forge u r) 1 := + .liftBind _ _ 0 fun _ => .pure _ 0 + +/-- The reduction built from the knowing forger computes a discrete logarithm with probability at +least `81 / 242`: the security bound reads `1 ≤ 0 + 2 / 11 + √(2 · ε')`. -/ +example : (81 / 242 : ℝ) ≤ Game.succProbability (oneWayGame (schnorrKeyGen (2 : ZMod 11)) + (fun α u => α • (2 : ZMod 11) = u) + (FiatShamir.reduction (schnorr ι (2 : ZMod 11)) + (linearSimulate (fun _ => LinearMap.toSpanSingleton (ZMod 11) (ZMod 11) 2) id ι) + (linearExtract ι) knower 1)) := by + have h := succProbability_eufCmaGame_le (δ := 11⁻¹) + (fun _ h => mem_support_schnorrKeyGen h) + ((schnorr_specialSoundness (ι := ι) (g := (2 : ZMod 11))).specialSoundOn (schnorrKeyGen 2)) + schnorr_specialHVZK (fun key _ t => commit_unpredictable key t) knower + knower_isQueryBounded + have hknower : Game.succProbability (eufCmaGame (fiatShamir (M := Bool) + (schnorr ι (2 : ZMod 11)) (schnorrKeyGen 2)) knower) = 1 := succProbability_knower + rw [hknower, ZMod.card] at h + set ε := (Game.succProbability (oneWayGame (schnorrKeyGen (2 : ZMod 11)) + (fun α u => α • (2 : ZMod 11) = u) + (FiatShamir.reduction (schnorr ι (2 : ZMod 11)) + (linearSimulate (fun _ => LinearMap.toSpanSingleton (ZMod 11) (ZMod 11) 2) id ι) + (linearExtract ι) knower 1)) : ℝ) with hε + have hε0 : 0 ≤ ε := NNReal.coe_nonneg _ + have hchoose : ((Nat.choose 1 2 : ℕ) : ℝ) = 0 := by norm_num + rw [hchoose, zero_mul, zero_add, Nat.cast_one, show (1 : ℝ) + 1 = 2 by norm_num] at h + have hsqrt : (9 / 11 : ℝ) ≤ √(2 * ε) := by + simp only [NNReal.coe_one, Nat.cast_ofNat] at h + linarith + have hsq := Real.sq_sqrt (by positivity : (0 : ℝ) ≤ 2 * ε) + nlinarith [mul_le_mul hsqrt hsqrt (by norm_num) (Real.sqrt_nonneg _)] + +/-! ### Axioms -/ + +/-- +info: 'Cslib.Crypto.Protocols.SigmaProtocol.succProbability_eufCmaGame_le' depends on axioms: +[propext, Classical.choice, Quot.sound] +-/ +#guard_msgs (whitespace := lax) in +#print axioms succProbability_eufCmaGame_le + +/-- +info: 'Cslib.Crypto.Protocols.SigmaProtocol.fiatShamir_correct' depends on axioms: +[propext, Classical.choice, Quot.sound] +-/ +#guard_msgs (whitespace := lax) in +#print axioms fiatShamir_correct + +end ComplexityTests.Crypto.FiatShamir diff --git a/ROADMAP.md b/ROADMAP.md index 2afa57f94..d04db535b 100644 --- a/ROADMAP.md +++ b/ROADMAP.md @@ -1173,10 +1173,14 @@ Jukna coverage below is an additional target beyond the V1 port: against direct attacks by uniform strict PPT impersonators under it. The general [forking lemma](Complexity/Probability/Forking.lean) (Bellare–Neven) is proved, also for [oracle programs](Complexity/Languages/Probabilistic/Forking.lean) with explicit coins and - presampled answers. Open (see #640): Fiat–Shamir/Schnorr signatures in the random-oracle model - with the bound of Theorem 19.16, and security against eavesdropping in the strict-PPT model, - where simulating transcripts needs approximately uniform `ZMod q` samples and hence an explicit - statistical-distance term. + presampled answers. [Fiat–Shamir signatures](Complexity/Crypto/Protocols/SigmaProtocol/FiatShamir.lean) + in the [random-oracle model](Complexity/Crypto/Protocols/Signature/RandomOracle.lean) are + correct and, exactly, EUF-CMA secure with the bound + `C(Q, 2) · δ + (Q + 1)/N + √((Q + 1) · ε')` of Theorem 19.16 and Equation 19.21, by the + [difference lemma](Complexity/Languages/Probabilistic/UntilBad.lean), presampling and forking. + Open (see #640): computational Schnorr signatures under discrete log for strict PPT forgers, + and security against eavesdropping in the strict-PPT model, where simulating transcripts needs + approximately uniform `ZMod q` samples and hence an explicit statistical-distance term. The current V1 port excludes the circuitized anti-checker, hardness-magnification argument and MINKT/MINCKT developments. The long-term canon above includes metacomplexity; those results should diff --git a/references.bib b/references.bib index 8d9a6be8c..4db700c1a 100644 --- a/references.bib +++ b/references.bib @@ -400,6 +400,19 @@ @inproceedings{BellareNeven2006 doi = {10.1145/1180405.1180453} } +@inproceedings{FiatShamir1986, + author = {Amos Fiat and Adi Shamir}, + title = {How to Prove Yourself: Practical Solutions to Identification and Signature + Problems}, + booktitle = {Advances in Cryptology -- CRYPTO '86}, + series = {Lecture Notes in Computer Science}, + volume = {263}, + pages = {186--194}, + publisher = {Springer}, + year = {1987}, + doi = {10.1007/3-540-47721-7_12} +} + @misc{BonehShoup2023, author = {Dan Boneh and Victor Shoup}, title = {A Graduate Course in Applied Cryptography},