Documentation

VCVio.CryptoFoundations.Fischlin.Completeness

Fischlin Transform: Completeness #

The completeness bound for the Fischlin transform (Fischlin 2005, Lemma 1). The random-oracle game is analysed through an equivalent pure-probability model game G, culminating in almostComplete: an honest proof verifies except with probability at most completenessError ρ b S (FinEnum.card Chal).

Completeness #

source
noncomputable def Fischlin.completenessError (ρ b S t : ℕ) :
ENNReal

Completeness error bound for the Fischlin transform (Fischlin 2005, Lemma 1).

Given ρ repetitions, b-bit hashes, max sum S, and challenge space size t: the error is ρ · ((2^b - ⌊S/ρ⌋ - 1) / 2^b)^t.

Derivation: by a union/pigeonhole bound over repetitions, if the sum of minimum hash values exceeds S, at least one minimum exceeds ⌊S/ρ⌋. The probability that the minimum of t independent uniform samples from Fin (2^b) exceeds k is ((2^b - k - 1) / 2^b)^t.

For S = 0 this simplifies to ρ · ((2^b - 1) / 2^b)^t. The intended regime is 0 < ρ; theorem statements below make that explicit.

Instances For

    Model game G for the completeness analysis #

    The random-oracle game is analysed via an equivalent pure-probability model G. In G, each random-oracle query of the prover's search is replaced by a fresh uniform draw from Fin (2^b) (justified because every query in sign is at a distinct fresh input, hence a cache miss), and the verifier reads the kept hash value directly from the search result rather than re-querying (a cache hit returning the same value).

    source
    @[reducible]
    noncomputable def Fischlin.fischlinImpl {Stmt Commit Chal Resp : Type} [DecidableEq Stmt] [DecidableEq Commit] [DecidableEq Chal] [DecidableEq Resp] (ρ b : ℕ) (M : Type) [DecidableEq M] :
    QueryImpl (unifSpec + fischlinROSpec Stmt Commit Chal Resp ρ b M) (StateT (fischlinROSpec Stmt Commit Chal Resp ρ b M).QueryCache ProbComp)

    The full simulation implementation (unifFwdImpl + randomOracle) interpreting the Fischlin random-oracle world into StateT QueryCache ProbComp. This is definitionally the implementation used by the bundled withStateOracle runtime.

    Instances For
      source
      theorem Fischlin.run_mOfFn_query_hit {Stmt Commit Chal Resp : Type} [DecidableEq Stmt] [DecidableEq Commit] [DecidableEq Chal] [DecidableEq Resp] (ρ b : ℕ) (M : Type) [DecidableEq M] {β : Type} (n : ℕ) (records : Fin n → (fischlinROSpec Stmt Commit Chal Resp ρ b M).Domain) (hash : Fin n → Fin (2 ^ b)) (f : Fin n → Fin (2 ^ b) → β) (cache : (fischlinROSpec Stmt Commit Chal Resp ρ b M).QueryCache) (hhit : ∀ (i : Fin n), cache (records i) = some (hash i)) :
      (simulateQ (fischlinImpl ρ b M) (Fin.mOfFn n fun (i : Fin n) => do let h ← query (records i) pure (f i h))).run cache = pure (fun (i : Fin n) => f i (hash i), cache)

      Simulating the verifier's Fin.mOfFn of random-oracle re-queries on a cache that already stores every re-queried record is deterministic: each query is a cache hit returning the stored value, leaving the cache untouched. The result is the pure product of the per-repetition outputs f i (hash i), where hash i is the value cached at record i.

      source
      theorem Fischlin.almostComplete {Stmt Wit Commit PrvState Chal Resp : Type} {rel : Stmt → Wit → Bool} [DecidableEq Stmt] [DecidableEq Commit] [DecidableEq Chal] [DecidableEq Resp] [FinEnum Chal] [Inhabited Chal] [Inhabited Resp] [SampleableType Chal] (σ : SigmaProtocol Stmt Wit Commit PrvState Chal Resp rel) (hr : GenerableRelation Stmt Wit rel) (ρ b S : ℕ) (M : Type) [DecidableEq M] (hρ : 0 < ρ) (hc : σ.PerfectlyComplete) (msg : M) :
      Pr[= true | (runtime ρ b M).evalDist do let __discr ← (Fischlin σ hr ρ b S M).keygen match __discr with | (pk, sk) => do let sig ← (Fischlin σ hr ρ b S M).sign pk sk msg (Fischlin σ hr ρ b S M).verify pk msg sig] ≥ 1 - completenessError ρ b S (FinEnum.card Chal)

      Almost completeness of the Fischlin transform: if the underlying Σ-protocol is perfectly complete, then the signature scheme verifies with probability at least 1 - completenessError ρ b S t where t = FinEnum.card Chal is the challenge space size.

      Unlike the Fiat-Shamir transform (which is perfectly complete), the Fischlin transform has a non-zero completeness error because the prover's proof-of-work search may fail to find hash values whose sum is at most S.