Fischlin Transform: Query-Cost Accounting

Query-complexity accounting for the Fischlin transform: bounds on the number of random-oracle queries made by verify and sign, their weighted query cost, and the corresponding expected-query bounds.

theorem Fischlin.verify_usesAtMostRhoQueries {Stmt Wit Commit PrvState Chal Resp : Type} {rel : Stmt → Wit → Bool} (ρ b : ℕ) (M : Type) {m : Type → Type v} [Monad m] [LawfulMonad m] [MonadLiftT ProbComp m] (σ : SigmaProtocol Stmt Wit Commit PrvState Chal Resp rel) [FinEnum Chal] [Inhabited Chal] [Inhabited Resp] (hr : GenerableRelation Stmt Wit rel) (S : ℕ) [DecidableEq M] [MonadLiftT m SetM] [LawfulMonadLiftT m SetM] (runtime : QueryImpl (fischlinROSpec Stmt Commit Chal Resp ρ b M) m) (pk : Stmt) (msg : M) (π : FischlinProof Commit Chal Resp ρ) : HasQuery.UsesAtMostQueries (fun [HasQuery (fischlinROSpec Stmt Commit Chal Resp ρ b M) (AddWriterT ℕ m)] => (Fischlin σ hr ρ b S M).verify pk msg π) runtime ρ

Fischlin verification makes at most ρ random-oracle queries under unit-cost instrumentation.

theorem Fischlin.verify_usesAtLeastRhoQueries {Stmt Wit Commit PrvState Chal Resp : Type} {rel : Stmt → Wit → Bool} (ρ b : ℕ) (M : Type) {m : Type → Type v} [Monad m] [LawfulMonad m] [MonadLiftT ProbComp m] (σ : SigmaProtocol Stmt Wit Commit PrvState Chal Resp rel) [FinEnum Chal] [Inhabited Chal] [Inhabited Resp] (hr : GenerableRelation Stmt Wit rel) (S : ℕ) [DecidableEq M] [MonadLiftT m SetM] [LawfulMonadLiftT m SetM] (runtime : QueryImpl (fischlinROSpec Stmt Commit Chal Resp ρ b M) m) (pk : Stmt) (msg : M) (π : FischlinProof Commit Chal Resp ρ) : HasQuery.UsesAtLeastQueries (fun [HasQuery (fischlinROSpec Stmt Commit Chal Resp ρ b M) (AddWriterT ℕ m)] => (Fischlin σ hr ρ b S M).verify pk msg π) runtime ρ

Fischlin verification makes at least ρ random-oracle queries under unit-cost instrumentation.

theorem Fischlin.sign_usesAtMostRhoCardOmegaQueries {Stmt Wit Commit PrvState Chal Resp : Type} {rel : Stmt → Wit → Bool} (ρ b : ℕ) (M : Type) {m : Type → Type v} [Monad m] [LawfulMonad m] [MonadLiftT ProbComp m] (σ : SigmaProtocol Stmt Wit Commit PrvState Chal Resp rel) [FinEnum Chal] [Inhabited Chal] [Inhabited Resp] (hr : GenerableRelation Stmt Wit rel) (S : ℕ) [DecidableEq M] [MonadLiftT m SetM] [LawfulMonadLiftT m SetM] (runtime : QueryImpl (fischlinROSpec Stmt Commit Chal Resp ρ b M) m) (pk : Stmt) (sk : Wit) (msg : M) : HasQuery.UsesAtMostQueries (fun [HasQuery (fischlinROSpec Stmt Commit Chal Resp ρ b M) (AddWriterT ℕ m)] => (Fischlin σ hr ρ b S M).sign pk sk msg) runtime (ρ * FinEnum.card Chal)

Fischlin signing makes at most ρ * |Ω| random-oracle queries under unit-cost instrumentation.

theorem Fischlin.sign_usesWeightedQueryCostAtMost {Stmt Wit Commit PrvState Chal Resp : Type} {rel : Stmt → Wit → Bool} (ρ b : ℕ) (M : Type) {m : Type → Type v} [Monad m] [LawfulMonad m] [MonadLiftT ProbComp m] (σ : SigmaProtocol Stmt Wit Commit PrvState Chal Resp rel) [FinEnum Chal] [Inhabited Chal] [Inhabited Resp] (hr : GenerableRelation Stmt Wit rel) (S : ℕ) [DecidableEq M] [MonadLiftT m SetM] [LawfulMonadLiftT m SetM] {κ : Type} [AddCommMonoid κ] [PartialOrder κ] [IsOrderedAddMonoid κ] [CanonicallyOrderedAdd κ] (runtime : QueryImpl (fischlinROSpec Stmt Commit Chal Resp ρ b M) m) (pk : Stmt) (sk : Wit) (msg : M) (costFn : (fischlinROSpec Stmt Commit Chal Resp ρ b M).Domain → κ) (w : κ) (hcost : ∀ (t : (fischlinROSpec Stmt Commit Chal Resp ρ b M).Domain), costFn t ≤ w) : HasQuery.UsesCostAtMost (fun [HasQuery (fischlinROSpec Stmt Commit Chal Resp ρ b M) (AddWriterT κ m)] => (Fischlin σ hr ρ b S M).sign pk sk msg) runtime costFn (ρ • FinEnum.card Chal • w)

Fischlin signing has weighted query cost at most ρ • (|Ω| • w) whenever every random-oracle query carries cost at most w.

theorem Fischlin.sign_expectedQueryCost_le {Stmt Wit Commit PrvState Chal Resp : Type} {rel : Stmt → Wit → Bool} (ρ b : ℕ) (M : Type) {m : Type → Type v} [Monad m] [LawfulMonad m] [MonadLiftT ProbComp m] (σ : SigmaProtocol Stmt Wit Commit PrvState Chal Resp rel) [FinEnum Chal] [Inhabited Chal] [Inhabited Resp] (hr : GenerableRelation Stmt Wit rel) (S : ℕ) [DecidableEq M] [MonadLiftT m SPMF] [MonadLiftT m SetM] [LawfulMonadLiftT m SetM] [EvalDistCompatible m] {κ : Type} [AddCommMonoid κ] [PartialOrder κ] [IsOrderedAddMonoid κ] [CanonicallyOrderedAdd κ] (runtime : QueryImpl (fischlinROSpec Stmt Commit Chal Resp ρ b M) m) (pk : Stmt) (sk : Wit) (msg : M) (costFn : (fischlinROSpec Stmt Commit Chal Resp ρ b M).Domain → κ) (w : κ) (val : κ → ENNReal) (hcost : ∀ (t : (fischlinROSpec Stmt Commit Chal Resp ρ b M).Domain), costFn t ≤ w) (hval : Monotone val) : HasQuery.expectedQueryCost (fun [HasQuery (fischlinROSpec Stmt Commit Chal Resp ρ b M) (AddWriterT κ m)] => (Fischlin σ hr ρ b S M).sign pk sk msg) runtime costFn val ≤ val (ρ • FinEnum.card Chal • w)

Fischlin signing has expected weighted query cost at most ρ • (|Ω| • w) whenever every random-oracle query is weighted by at most w.

theorem Fischlin.sign_expectedQueries_le_rhoCardOmega {Stmt Wit Commit PrvState Chal Resp : Type} {rel : Stmt → Wit → Bool} (ρ b : ℕ) (M : Type) {m : Type → Type v} [Monad m] [LawfulMonad m] [MonadLiftT ProbComp m] (σ : SigmaProtocol Stmt Wit Commit PrvState Chal Resp rel) [FinEnum Chal] [Inhabited Chal] [Inhabited Resp] (hr : GenerableRelation Stmt Wit rel) (S : ℕ) [DecidableEq M] [MonadLiftT m SPMF] [MonadLiftT m SetM] [LawfulMonadLiftT m SetM] [EvalDistCompatible m] (runtime : QueryImpl (fischlinROSpec Stmt Commit Chal Resp ρ b M) m) (pk : Stmt) (sk : Wit) (msg : M) : HasQuery.expectedQueries (fun [HasQuery (fischlinROSpec Stmt Commit Chal Resp ρ b M) (AddWriterT ℕ m)] => (Fischlin σ hr ρ b S M).sign pk sk msg) runtime ≤ ↑ρ * ↑(FinEnum.card Chal)

Fischlin signing has expected query count at most ρ * |Ω| in the unit-cost runtime model.

This is the expectation-level counterpart of [Fischlin.sign_usesAtMostRhoCardOmegaQueries].

theorem Fischlin.verify_expectedQueries_eq_rho {Stmt Wit Commit PrvState Chal Resp : Type} {rel : Stmt → Wit → Bool} (ρ b : ℕ) (M : Type) {m : Type → Type v} [Monad m] [LawfulMonad m] [MonadLiftT ProbComp m] (σ : SigmaProtocol Stmt Wit Commit PrvState Chal Resp rel) [FinEnum Chal] [Inhabited Chal] [Inhabited Resp] (hr : GenerableRelation Stmt Wit rel) (S : ℕ) [DecidableEq M] [MonadLiftT m PMF] [MonadLiftT m SetM] [LawfulMonadLiftT m SetM] [EvalDistCompatible m] (runtime : QueryImpl (fischlinROSpec Stmt Commit Chal Resp ρ b M) m) (pk : Stmt) (msg : M) (π : FischlinProof Commit Chal Resp ρ) : HasQuery.expectedQueries (fun [HasQuery (fischlinROSpec Stmt Commit Chal Resp ρ b M) (AddWriterT ℕ m)] => (Fischlin σ hr ρ b S M).verify pk msg π) runtime = ↑ρ

Fischlin verification has expected query count exactly ρ in the unit-cost runtime model.