Fiat-Shamir Transform

This file defines a basic version of the Fiat-Shamir transform on sigma protocols. For simplicity we construct signature schemes rather than general proofs of knowledge.

structure GenerableRelation (X W : Type) (r : X → W → Bool) [OracleComp.SelectableType X] [OracleComp.SelectableType W] : Type 1

• gen : ProbComp (X × W)
• gen_sound (x : X) (w : W) : (x, w) ∈ OracleComp.support self.gen → r x w = true
• gen_uniform_right (x : X) : [=x|Prod.fst <$> self.gen] = [=x|$ᵗX]
• gen_uniform_left (w : W) : [=w|Prod.snd <$> self.gen] = [=w|$ᵗW]

def FiatShamir {X W PC SC Ω P : Type} {p : X → W → Bool} [OracleComp.SelectableType X] [OracleComp.SelectableType W] [DecidableEq PC] [DecidableEq Ω] [OracleComp.SelectableType Ω] (sigmaAlg : SigmaAlg X W PC SC Ω P p) (hr : GenerableRelation X W p) (M : Type) [DecidableEq M] : SignatureAlg (OracleComp (unifSpec ++ₒ (M × PC →ₒ Ω))) M X W (PC × P)

Equations

• One or more equations did not get rendered due to their size.