Fiat-Shamir transform for Σ-protocols

The classical (non-aborting) Fiat-Shamir transform: given a 3-round Σ-protocol and a generable relation, produce a signature scheme in the random-oracle model. The signing algorithm commits, queries the random oracle on (message, commitment), and responds to the resulting challenge.

This file contains the scheme definition, the random-oracle runtime bundle, the naturality theorem, cost accounting, and completeness. The forking-lemma bridge lives in FiatShamir.Sigma.Fork and the EUF-CMA reduction in FiatShamir.Sigma.Security.

def FiatShamir {Stmt Wit Commit PrvState Chal Resp : Type} {rel : Stmt → Wit → Bool} {m : Type → Type v} [Monad m] (sigmaAlg : SigmaProtocol Stmt Wit Commit PrvState Chal Resp rel) (hr : GenerableRelation Stmt Wit rel) (M : Type) [MonadLiftT ProbComp m] [HasQuery (OracleSpec.ofFn fun (x : M × Commit) => Chal) m] : SignatureAlg m M Stmt Wit (Commit × Resp)

Given a Σ-protocol and a generable relation, the Fiat-Shamir transform produces a signature scheme. The signing algorithm commits, queries the random oracle on (message, commitment), and then responds to the challenge.

noncomputable def FiatShamir.runtime {Commit Chal : Type} (M : Type) [SampleableType Chal] : ProbCompRuntime (OracleComp (unifSpec + OracleSpec.ofFn fun (x : M × Commit) => Chal))

Runtime bundle for the Fiat-Shamir random-oracle world.

theorem FiatShamir.map_construction {Stmt Wit Commit PrvState Chal Resp : Type} {rel : Stmt → Wit → Bool} (σ : SigmaProtocol Stmt Wit Commit PrvState Chal Resp rel) (hr : GenerableRelation Stmt Wit rel) (M : Type) {m : Type → Type u} [Monad m] {n : Type → Type v} [Monad n] [MonadLiftT ProbComp m] [MonadLiftT ProbComp n] [HasQuery (OracleSpec.ofFn fun (x : M × Commit) => Chal) m] [HasQuery (OracleSpec.ofFn fun (x : M × Commit) => Chal) n] (F : HasQuery.QueryHom (OracleSpec.ofFn fun (x : M × Commit) => Chal) m n) (hLift : HasQuery.PreservesProbCompLift F.toMonadHom) : SignatureAlg.map F.toMonadHom (FiatShamir σ hr M) = FiatShamir σ hr M

Fiat-Shamir is natural in any oracle semantics morphism that preserves both random-oracle queries and public-randomness lifting.

This is the basic coherence theorem behind the generic/concrete split:

• define Fiat-Shamir once over HasQuery
• specialize it in one monad
• transport it along a query-preserving monad morphism into another analysis monad

If the morphism also commutes with the designated ProbComp lift, then transporting the generic construction agrees with re-instantiating the construction directly in the target monad.

theorem FiatShamir.sign_usesCostAsQueryCost {Stmt Wit Commit PrvState Chal Resp : Type} {rel : Stmt → Wit → Bool} (σ : SigmaProtocol Stmt Wit Commit PrvState Chal Resp rel) (hr : GenerableRelation Stmt Wit rel) (M : Type) {m : Type → Type u} [Monad m] [LawfulMonad m] [MonadLiftT ProbComp m] {ω : Type} [AddMonoid ω] (runtime : QueryRuntime (OracleSpec.ofFn fun (x : M × Commit) => Chal) m) (pk : Stmt) (sk : Wit) (msg : M) (costFn : M × Commit → ω) : HasQuery.UsesCostAs (fun [HasQuery (OracleSpec.ofFn fun (x : M × Commit) => Chal) (AddWriterT ω m)] => (FiatShamir σ hr M).sign pk sk msg) runtime costFn fun (sig : Commit × Resp) => costFn (msg, sig.1)

Fiat-Shamir signing has query cost determined by its output: the signature (c, s) records the unique queried commitment c, so the total weighted query cost is exactly costFn (msg, c).

theorem FiatShamir.sign_expectedQueryCost_eq_outputExpectation {Stmt Wit Commit PrvState Chal Resp : Type} {rel : Stmt → Wit → Bool} (σ : SigmaProtocol Stmt Wit Commit PrvState Chal Resp rel) (hr : GenerableRelation Stmt Wit rel) (M : Type) {m : Type → Type u} [Monad m] [LawfulMonad m] [MonadLiftT ProbComp m] {ω : Type} [AddMonoid ω] [HasEvalSPMF m] (runtime : QueryRuntime (OracleSpec.ofFn fun (x : M × Commit) => Chal) m) (pk : Stmt) (sk : Wit) (msg : M) (costFn : M × Commit → ω) (val : ω → ENNReal) : HasQuery.expectedQueryCost (fun [HasQuery (OracleSpec.ofFn fun (x : M × Commit) => Chal) (AddWriterT ω m)] => (FiatShamir σ hr M).sign pk sk msg) runtime costFn val = ∑' (sig : Commit × Resp), Pr[= sig | HasQuery.inRuntime (fun [HasQuery (OracleSpec.ofFn fun (x : M × Commit) => Chal) m] => (FiatShamir σ hr M).sign pk sk msg) runtime] * val (costFn (msg, sig.1))

Fiat-Shamir signing has expected weighted query cost equal to the expectation of the queried commitment cost over the output signature distribution.

@[simp]

theorem FiatShamir.sign_usesExactlyOneQuery {Stmt Wit Commit PrvState Chal Resp : Type} {rel : Stmt → Wit → Bool} (σ : SigmaProtocol Stmt Wit Commit PrvState Chal Resp rel) (hr : GenerableRelation Stmt Wit rel) (M : Type) {m : Type → Type u} [Monad m] [LawfulMonad m] [MonadLiftT ProbComp m] (runtime : QueryRuntime (OracleSpec.ofFn fun (x : M × Commit) => Chal) m) (pk : Stmt) (sk : Wit) (msg : M) : HasQuery.UsesExactlyQueries (fun [HasQuery (OracleSpec.ofFn fun (x : M × Commit) => Chal) (AddWriterT ℕ m)] => (FiatShamir σ hr M).sign pk sk msg) runtime 1

Fiat-Shamir signing makes exactly one random-oracle query under unit-cost instrumentation.

theorem FiatShamir.verify_usesExactQueryCost {Stmt Wit Commit PrvState Chal Resp : Type} {rel : Stmt → Wit → Bool} (σ : SigmaProtocol Stmt Wit Commit PrvState Chal Resp rel) (hr : GenerableRelation Stmt Wit rel) (M : Type) {m : Type → Type u} [Monad m] [LawfulMonad m] [MonadLiftT ProbComp m] {ω : Type} [AddMonoid ω] (runtime : QueryRuntime (OracleSpec.ofFn fun (x : M × Commit) => Chal) m) (pk : Stmt) (msg : M) (sig : Commit × Resp) (costFn : M × Commit → ω) : HasQuery.UsesCostExactly (fun [HasQuery (OracleSpec.ofFn fun (x : M × Commit) => Chal) (AddWriterT ω m)] => (FiatShamir σ hr M).verify pk msg sig) runtime costFn (costFn (msg, sig.1))

Fiat-Shamir verification incurs exactly the weighted cost assigned to the single random-oracle query on (msg, sig.1).

theorem FiatShamir.verify_expectedQueryCost_eq {Stmt Wit Commit PrvState Chal Resp : Type} {rel : Stmt → Wit → Bool} (σ : SigmaProtocol Stmt Wit Commit PrvState Chal Resp rel) (hr : GenerableRelation Stmt Wit rel) (M : Type) {m : Type → Type u} [Monad m] [LawfulMonad m] [MonadLiftT ProbComp m] {ω : Type} [AddMonoid ω] [Preorder ω] [HasEvalPMF m] (runtime : QueryRuntime (OracleSpec.ofFn fun (x : M × Commit) => Chal) m) (pk : Stmt) (msg : M) (sig : Commit × Resp) (costFn : M × Commit → ω) (val : ω → ENNReal) (hval : Monotone val) : HasQuery.expectedQueryCost (fun [HasQuery (OracleSpec.ofFn fun (x : M × Commit) => Chal) (AddWriterT ω m)] => (FiatShamir σ hr M).verify pk msg sig) runtime costFn val = val (costFn (msg, sig.1))

Fiat-Shamir verification has expected weighted query cost equal to the weight of its single random-oracle query.

@[simp]

theorem FiatShamir.verify_usesExactlyOneQuery {Stmt Wit Commit PrvState Chal Resp : Type} {rel : Stmt → Wit → Bool} (σ : SigmaProtocol Stmt Wit Commit PrvState Chal Resp rel) (hr : GenerableRelation Stmt Wit rel) (M : Type) {m : Type → Type u} [Monad m] [LawfulMonad m] [MonadLiftT ProbComp m] (runtime : QueryRuntime (OracleSpec.ofFn fun (x : M × Commit) => Chal) m) (pk : Stmt) (msg : M) (sig : Commit × Resp) : HasQuery.UsesExactlyQueries (fun [HasQuery (OracleSpec.ofFn fun (x : M × Commit) => Chal) (AddWriterT ℕ m)] => (FiatShamir σ hr M).verify pk msg sig) runtime 1

Fiat-Shamir verification makes exactly one random-oracle query under unit-cost instrumentation.

theorem FiatShamir.perfectlyCorrect {Stmt Wit Commit PrvState Chal Resp : Type} {rel : Stmt → Wit → Bool} (σ : SigmaProtocol Stmt Wit Commit PrvState Chal Resp rel) (hr : GenerableRelation Stmt Wit rel) (M : Type) [SampleableType Chal] (hc : σ.PerfectlyComplete) : (FiatShamir σ hr M).PerfectlyComplete (runtime M)

Completeness of the Fiat-Shamir signature scheme follows from completeness of the underlying Σ-protocol.