Expected-cost PMF theorems for Fiat-Shamir with aborts

Expected random-oracle query costs of fsAbortSignLoop and FiatShamirWithAbort.sign/verify, stated as tsum identities over the induced output distributions. These drive the aggregate runtime bounds used in the security proof.

@[reducible, inline]

noncomputable abbrev FiatShamirWithAbort.signAttemptAbortProbability {Stmt Wit Commit PrvState Chal Resp : Type} {rel : Stmt → Wit → Bool} (ids : IdenSchemeWithAbort Stmt Wit Commit PrvState Chal Resp rel) (M : Type) {m : Type → Type u} [Monad m] [MonadLiftT ProbComp m] [HasEvalPMF m] (runtime : QueryRuntime (OracleSpec.ofFn fun (x : M × Commit) => Chal) m) (pk : Stmt) (sk : Wit) (msg : M) : ENNReal

The probability that a single Fiat-Shamir-with-aborts signing attempt aborts.

theorem FiatShamirWithAbort.sign_abortPrefixProbability_eq_signAttemptAbortProbability_pow {Stmt Wit Commit PrvState Chal Resp : Type} {rel : Stmt → Wit → Bool} (ids : IdenSchemeWithAbort Stmt Wit Commit PrvState Chal Resp rel) (M : Type) {m : Type → Type u} [Monad m] [MonadLiftT ProbComp m] [HasEvalPMF m] (runtime : QueryRuntime (OracleSpec.ofFn fun (x : M × Commit) => Chal) m) (pk : Stmt) (sk : Wit) (msg : M) (i : ℕ) : Pr[= none | HasQuery.inRuntime (fun [HasQuery (OracleSpec.ofFn fun (x : M × Commit) => Chal) m] => fsAbortSignLoop ids M pk sk msg i) runtime] = signAttemptAbortProbability ids M runtime pk sk msg ^ i

The probability that the first i signing attempts all abort is the i-th power of the single-attempt abort probability.

theorem FiatShamirWithAbort.sign_queryTailProbability_eq_probAllFirstAttemptsAbort {Stmt Wit Commit PrvState Chal Resp : Type} {rel : Stmt → Wit → Bool} (ids : IdenSchemeWithAbort Stmt Wit Commit PrvState Chal Resp rel) (M : Type) {m : Type → Type u} [Monad m] [MonadLiftT ProbComp m] [HasEvalPMF m] [LawfulMonad m] (hr : GenerableRelation Stmt Wit rel) (runtime : QueryRuntime (OracleSpec.ofFn fun (x : M × Commit) => Chal) m) (pk : Stmt) (sk : Wit) (msg : M) {i maxAttempts : ℕ} (hi : i < maxAttempts) : (probEvent (HasQuery.queryCountDist (fun [HasQuery (OracleSpec.ofFn fun (x : M × Commit) => Chal) (AddWriterT ℕ m)] => (FiatShamirWithAbort ids hr M maxAttempts).sign pk sk msg) runtime) fun (q : ℕ) => i < q) = Pr[= none | HasQuery.inRuntime (fun [HasQuery (OracleSpec.ofFn fun (x : M × Commit) => Chal) m] => fsAbortSignLoop ids M pk sk msg i) runtime]

The probability that signing makes more than i random-oracle queries is exactly the probability that the first i signing attempts all abort.

Equivalently, the event i < q for the signer query count is the event that the retry loop of length i returns none, meaning that the (i + 1)-st attempt is reached.

theorem FiatShamirWithAbort.sign_queryTailProbability_eq_signAttemptAbortProbability_pow {Stmt Wit Commit PrvState Chal Resp : Type} {rel : Stmt → Wit → Bool} (ids : IdenSchemeWithAbort Stmt Wit Commit PrvState Chal Resp rel) (M : Type) {m : Type → Type u} [Monad m] [MonadLiftT ProbComp m] [HasEvalPMF m] [LawfulMonad m] (hr : GenerableRelation Stmt Wit rel) (runtime : QueryRuntime (OracleSpec.ofFn fun (x : M × Commit) => Chal) m) (pk : Stmt) (sk : Wit) (msg : M) {i maxAttempts : ℕ} (hi : i < maxAttempts) : (probEvent (HasQuery.queryCountDist (fun [HasQuery (OracleSpec.ofFn fun (x : M × Commit) => Chal) (AddWriterT ℕ m)] => (FiatShamirWithAbort ids hr M maxAttempts).sign pk sk msg) runtime) fun (q : ℕ) => i < q) = signAttemptAbortProbability ids M runtime pk sk msg ^ i

The probability that signing makes more than i oracle queries is the i-th power of the single-attempt abort probability, as long as i < maxAttempts.

theorem FiatShamirWithAbort.sign_expectedQueries_eq_sum_abortPrefixProbabilities {Stmt Wit Commit PrvState Chal Resp : Type} {rel : Stmt → Wit → Bool} (ids : IdenSchemeWithAbort Stmt Wit Commit PrvState Chal Resp rel) (M : Type) {m : Type → Type u} [Monad m] [MonadLiftT ProbComp m] [HasEvalPMF m] [LawfulMonad m] (hr : GenerableRelation Stmt Wit rel) (runtime : QueryRuntime (OracleSpec.ofFn fun (x : M × Commit) => Chal) m) (pk : Stmt) (sk : Wit) (msg : M) (maxAttempts : ℕ) : HasQuery.expectedQueries (fun [HasQuery (OracleSpec.ofFn fun (x : M × Commit) => Chal) (AddWriterT ℕ m)] => (FiatShamirWithAbort ids hr M maxAttempts).sign pk sk msg) runtime = ∑ i ∈ Finset.range maxAttempts, Pr[= none | HasQuery.inRuntime (fun [HasQuery (OracleSpec.ofFn fun (x : M × Commit) => Chal) m] => fsAbortSignLoop ids M pk sk msg i) runtime]

The expected number of signing queries is the sum, over prefixes of the retry loop, of the probability that every attempt in the prefix aborts.

theorem FiatShamirWithAbort.sign_expectedQueries_eq_sum_signAttemptAbortProbability_powers {Stmt Wit Commit PrvState Chal Resp : Type} {rel : Stmt → Wit → Bool} (ids : IdenSchemeWithAbort Stmt Wit Commit PrvState Chal Resp rel) (M : Type) {m : Type → Type u} [Monad m] [MonadLiftT ProbComp m] [HasEvalPMF m] [LawfulMonad m] (hr : GenerableRelation Stmt Wit rel) (runtime : QueryRuntime (OracleSpec.ofFn fun (x : M × Commit) => Chal) m) (pk : Stmt) (sk : Wit) (msg : M) (maxAttempts : ℕ) : HasQuery.expectedQueries (fun [HasQuery (OracleSpec.ofFn fun (x : M × Commit) => Chal) (AddWriterT ℕ m)] => (FiatShamirWithAbort ids hr M maxAttempts).sign pk sk msg) runtime = ∑ i ∈ Finset.range maxAttempts, signAttemptAbortProbability ids M runtime pk sk msg ^ i

The expected number of signing queries is the finite geometric sum of the one-step abort probability.

theorem FiatShamirWithAbort.sign_queryTailProbability_le_signAttemptAbortProbability_pow {Stmt Wit Commit PrvState Chal Resp : Type} {rel : Stmt → Wit → Bool} (ids : IdenSchemeWithAbort Stmt Wit Commit PrvState Chal Resp rel) (M : Type) {m : Type → Type u} [Monad m] [MonadLiftT ProbComp m] [HasEvalPMF m] [LawfulMonad m] (hr : GenerableRelation Stmt Wit rel) (runtime : QueryRuntime (OracleSpec.ofFn fun (x : M × Commit) => Chal) m) (pk : Stmt) (sk : Wit) (msg : M) (i maxAttempts : ℕ) : (probEvent (HasQuery.queryCountDist (fun [HasQuery (OracleSpec.ofFn fun (x : M × Commit) => Chal) (AddWriterT ℕ m)] => (FiatShamirWithAbort ids hr M maxAttempts).sign pk sk msg) runtime) fun (q : ℕ) => i < q) ≤ signAttemptAbortProbability ids M runtime pk sk msg ^ i

Tail probabilities for the signer query count are bounded by the corresponding power of the single-attempt abort probability.

theorem FiatShamirWithAbort.sign_expectedQueries_le_tsum_signAttemptAbortProbability_powers {Stmt Wit Commit PrvState Chal Resp : Type} {rel : Stmt → Wit → Bool} (ids : IdenSchemeWithAbort Stmt Wit Commit PrvState Chal Resp rel) (M : Type) {m : Type → Type u} [Monad m] [MonadLiftT ProbComp m] [HasEvalPMF m] [LawfulMonad m] (hr : GenerableRelation Stmt Wit rel) (runtime : QueryRuntime (OracleSpec.ofFn fun (x : M × Commit) => Chal) m) (pk : Stmt) (sk : Wit) (msg : M) (maxAttempts : ℕ) : HasQuery.expectedQueries (fun [HasQuery (OracleSpec.ofFn fun (x : M × Commit) => Chal) (AddWriterT ℕ m)] => (FiatShamirWithAbort ids hr M maxAttempts).sign pk sk msg) runtime ≤ ∑' (i : ℕ), signAttemptAbortProbability ids M runtime pk sk msg ^ i

The expected number of signing queries is bounded by the infinite geometric series generated by the single-attempt abort probability.

theorem FiatShamirWithAbort.sign_expectedQueries_le_geometric_of_signAttemptAbortProbability_le {Stmt Wit Commit PrvState Chal Resp : Type} {rel : Stmt → Wit → Bool} (ids : IdenSchemeWithAbort Stmt Wit Commit PrvState Chal Resp rel) (M : Type) {m : Type → Type u} [Monad m] [MonadLiftT ProbComp m] [HasEvalPMF m] [LawfulMonad m] (hr : GenerableRelation Stmt Wit rel) (runtime : QueryRuntime (OracleSpec.ofFn fun (x : M × Commit) => Chal) m) (pk : Stmt) (sk : Wit) (msg : M) (maxAttempts : ℕ) {q : ENNReal} (hq : signAttemptAbortProbability ids M runtime pk sk msg ≤ q) : HasQuery.expectedQueries (fun [HasQuery (OracleSpec.ofFn fun (x : M × Commit) => Chal) (AddWriterT ℕ m)] => (FiatShamirWithAbort ids hr M maxAttempts).sign pk sk msg) runtime ≤ (1 - q)⁻¹

If the single-attempt abort probability is bounded by q, then the expected number of signing queries is bounded by the corresponding geometric series.

theorem FiatShamirWithAbort.sign_expectedQueries_le_geometric {Stmt Wit Commit PrvState Chal Resp : Type} {rel : Stmt → Wit → Bool} (ids : IdenSchemeWithAbort Stmt Wit Commit PrvState Chal Resp rel) (M : Type) {m : Type → Type u} [Monad m] [MonadLiftT ProbComp m] [HasEvalPMF m] [LawfulMonad m] (hr : GenerableRelation Stmt Wit rel) (runtime : QueryRuntime (OracleSpec.ofFn fun (x : M × Commit) => Chal) m) (pk : Stmt) (sk : Wit) (msg : M) (maxAttempts : ℕ) : HasQuery.expectedQueries (fun [HasQuery (OracleSpec.ofFn fun (x : M × Commit) => Chal) (AddWriterT ℕ m)] => (FiatShamirWithAbort ids hr M maxAttempts).sign pk sk msg) runtime ≤ (1 - signAttemptAbortProbability ids M runtime pk sk msg)⁻¹

Specializing the geometric upper bound to the actual one-step abort probability yields the canonical infinite geometric upper bound on expected query count.

theorem FiatShamirWithAbort.verify_expectedQueryCost_eq {Stmt Wit Commit PrvState Chal Resp : Type} {rel : Stmt → Wit → Bool} (ids : IdenSchemeWithAbort Stmt Wit Commit PrvState Chal Resp rel) (M : Type) {m : Type → Type u} [Monad m] [MonadLiftT ProbComp m] [HasEvalPMF m] [LawfulMonad m] (hr : GenerableRelation Stmt Wit rel) {ω : Type} [AddMonoid ω] [Preorder ω] (runtime : QueryRuntime (OracleSpec.ofFn fun (x : M × Commit) => Chal) m) (pk : Stmt) (msg : M) (sig : Option (Commit × Resp)) (costFn : M × Commit → ω) (val : ω → ENNReal) (hval : Monotone val) (maxAttempts : ℕ) : HasQuery.expectedQueryCost (fun [HasQuery (OracleSpec.ofFn fun (x : M × Commit) => Chal) (AddWriterT ω m)] => (FiatShamirWithAbort ids hr M maxAttempts).verify pk msg sig) runtime costFn val = match sig with | none => val 0 | some (w', snd) => val (costFn (msg, w'))

Verification has expected weighted query cost equal to the cost of the single verification query when a signature is present, and 0 when the signature is none.