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.runtimeWithCache {Commit Chal : Type} (M : Type) [SampleableType Chal] (cache : (OracleSpec.ofFn fun (x : M × Commit) => Chal).QueryCache) : ProbCompRuntime (OracleComp (unifSpec + OracleSpec.ofFn fun (x : M × Commit) => Chal))

Runtime bundle for the Fiat-Shamir random-oracle world starting from a fixed initial cache.

This is the cache-parametric form of runtime: the random oracle is preloaded with cache, so queries that hit return the cached value and misses fall through to fresh uniform sampling and get cached for later. Specializing cache := ∅ recovers the standard fresh-RO runtime (runtime).

The cache parameter is the universal hook for programming the random oracle: any caller that wants to inject pre-decided answers at chosen points runs its experiment under runtimeWithCache cache instead of runtime.

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.

Definitionally equal to runtimeWithCache ∅: the standard runtime is the cache-parametric one preloaded with the empty cache.

@[simp]

theorem FiatShamir.runtime_eq_runtimeWithCache_empty {Commit Chal : Type} (M : Type) [SampleableType Chal] : runtime M = runtimeWithCache M ∅

theorem FiatShamir.runtimeWithCache_evalDist_map {Commit Chal : Type} (M : Type) [SampleableType Chal] (cache : (OracleSpec.ofFn fun (x : M × Commit) => Chal).QueryCache) {α β : Type} (f : α → β) (mx : OracleComp (unifSpec + OracleSpec.ofFn fun (x : M × Commit) => Chal) α) : (runtimeWithCache M cache).evalDist (f <$> mx) = f <$> (runtimeWithCache M cache).evalDist mx

The cache-parametric Fiat-Shamir runtime commutes with <$>: mapping a function over the surface computation is the same as mapping it over the observed SPMF. A direct corollary of SPMFSemantics.withStateOracle_evalDist_map.

theorem FiatShamir.runtimeWithCache_evalDist_bind_pure {Commit Chal : Type} (M : Type) [SampleableType Chal] (cache : (OracleSpec.ofFn fun (x : M × Commit) => Chal).QueryCache) {α β : Type} (mx : OracleComp (unifSpec + OracleSpec.ofFn fun (x : M × Commit) => Chal) α) (f : α → β) : ((runtimeWithCache M cache).evalDist do let x ← mx pure (f x)) = f <$> (runtimeWithCache M cache).evalDist mx

The cache-parametric Fiat-Shamir runtime commutes with >>= pure ∘ f. A direct corollary of runtimeWithCache_evalDist_map.

theorem FiatShamir.runtimeWithCache_evalDist_bind_liftComp {Commit Chal : Type} (M : Type) [SampleableType Chal] (cache : (OracleSpec.ofFn fun (x : M × Commit) => Chal).QueryCache) {α β : Type} (oa : ProbComp α) (rest : α → OracleComp (unifSpec + OracleSpec.ofFn fun (x : M × Commit) => Chal) β) : (runtimeWithCache M cache).evalDist (liftM oa >>= rest) = do let x ← 𝒟[oa] (runtimeWithCache M cache).evalDist (rest x)

The Fiat-Shamir runtime commutes with binding a lifted ProbComp prefix: evaluating liftM oa >>= rest under the runtime is the same as first sampling oa in SPMF and then evaluating rest x under the runtime.

theorem FiatShamir.runtime_evalDist_map {Commit Chal : Type} (M : Type) [SampleableType Chal] {α β : Type} (f : α → β) (mx : OracleComp (unifSpec + OracleSpec.ofFn fun (x : M × Commit) => Chal) α) : (runtime M).evalDist (f <$> mx) = f <$> (runtime M).evalDist mx

The Fiat-Shamir runtime commutes with <$>: cache := ∅ instance of runtimeWithCache_evalDist_map.

theorem FiatShamir.runtime_evalDist_bind_pure {Commit Chal : Type} (M : Type) [SampleableType Chal] {α β : Type} (mx : OracleComp (unifSpec + OracleSpec.ofFn fun (x : M × Commit) => Chal) α) (f : α → β) : ((runtime M).evalDist do let x ← mx pure (f x)) = f <$> (runtime M).evalDist mx

The Fiat-Shamir runtime commutes with >>= pure ∘ f: cache := ∅ instance of runtimeWithCache_evalDist_bind_pure.

theorem FiatShamir.runtime_evalDist_bind_liftComp {Commit Chal : Type} (M : Type) [SampleableType Chal] {α β : Type} (oa : ProbComp α) (rest : α → OracleComp (unifSpec + OracleSpec.ofFn fun (x : M × Commit) => Chal) β) : (runtime M).evalDist (liftM oa >>= rest) = do let x ← 𝒟[oa] (runtime M).evalDist (rest x)

cache := ∅ instance of runtimeWithCache_evalDist_bind_liftComp.

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 : QueryImpl (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 : QueryImpl (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.Program.eval (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 : QueryImpl (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 : QueryImpl (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 : QueryImpl (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 : QueryImpl (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.