feat(crypto): Fiat–Shamir signatures in the random-oracle model, exact security (#581 3b-i)

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

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

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. -/