Documentation

VCVio.CryptoFoundations.FiatShamir.QueryBounds

Query-count bounds for Fiat-Shamir adversaries #

Structural IsQueryBound predicates used by both the Σ-protocol and with-aborts instances of Fiat-Shamir, plus the reciprocal challenge-space size that appears in the quantitative bounds.

The two non-aborting EUF-CMA variants use exactly the same predicates, so they live here in the shared FiatShamir namespace. With-aborts call sites reference them via their fully qualified name.

source
def FiatShamir.hashQueryBound {Commit Chal : Type} (M : Type) {S' α : Type} (oa : OracleComp ((unifSpec + OracleSpec.ofFn fun (x : M × Commit) => Chal) + OracleSpec.ofFn fun (x : M) => S') α) (Q : ℕ) :
Prop

Structural bound that counts only random-oracle queries in a Fiat-Shamir EUF-CMA adversary. Uniform-sampling and signing-oracle queries are unrestricted.

Instances For
    source
    def FiatShamir.signHashQueryBound {Commit Chal : Type} (M : Type) {S' α : Type} (oa : OracleComp ((unifSpec + OracleSpec.ofFn fun (x : M × Commit) => Chal) + OracleSpec.ofFn fun (x : M) => S') α) (qS qH : ℕ) :
    Prop

    Structural query bound for Fiat-Shamir EUF-CMA adversaries that tracks both signing-oracle queries (qS) and random-oracle queries (qH). Uniform-sampling queries are unrestricted.

    Instances For
      source
      def FiatShamir.nmaHashQueryBound {Commit Chal : Type} (M : Type) {α : Type} (oa : OracleComp (unifSpec + OracleSpec.ofFn fun (x : M × Commit) => Chal) α) (Q : ℕ) :
      Prop

      Structural bound on random-oracle queries for an NMA adversary (no signing oracle). Uniform-sampling queries are unrestricted.

      Instances For
        source
        @[simp]
        theorem FiatShamir.nmaHashQueryBound_query_bind_iff {Commit Chal : Type} (M : Type) {α : Type} (t : (unifSpec + OracleSpec.ofFn fun (x : M × Commit) => Chal).Domain) (oa : (unifSpec + OracleSpec.ofFn fun (x : M × Commit) => Chal).Range t → OracleComp (unifSpec + OracleSpec.ofFn fun (x : M × Commit) => Chal) α) (Q : ℕ) :
        nmaHashQueryBound M (liftM (OracleQuery.query t) >>= oa) Q ↔ (match t, oa with | Sum.inl val, oa => True | Sum.inr val, oa => 0 < Q) ∧ ∀ (u : (unifSpec + OracleSpec.ofFn fun (x : M × Commit) => Chal).Range t), nmaHashQueryBound M (oa u) (match t, oa, u with | Sum.inl val, oa, u => Q | Sum.inr val, oa, u => Q - 1)
        source
        @[simp]
        theorem FiatShamir.nmaHashQueryBound_query_iff {Commit Chal : Type} (M : Type) (t : (unifSpec + OracleSpec.ofFn fun (x : M × Commit) => Chal).Domain) (Q : ℕ) :
        nmaHashQueryBound M (liftM (OracleQuery.query t)) Q ↔ match t with | Sum.inl val => True | Sum.inr val => 0 < Q
        source
        theorem FiatShamir.nmaHashQueryBound_mono {Commit Chal : Type} (M : Type) {α : Type} {oa : OracleComp (unifSpec + OracleSpec.ofFn fun (x : M × Commit) => Chal) α} {Q₁ Q₂ : ℕ} (h : nmaHashQueryBound M oa Q₁) (hQ : Q₁ ≤ Q₂) :
        nmaHashQueryBound M oa Q₂
        source
        theorem FiatShamir.nmaHashQueryBound_bind {Commit Chal : Type} (M : Type) {α β : Type} {oa : OracleComp (unifSpec + OracleSpec.ofFn fun (x : M × Commit) => Chal) α} {ob : α → OracleComp (unifSpec + OracleSpec.ofFn fun (x : M × Commit) => Chal) β} {Q₁ Q₂ : ℕ} (h1 : nmaHashQueryBound M oa Q₁) (h2 : ∀ (x : α), nmaHashQueryBound M (ob x) Q₂) :
        nmaHashQueryBound M (oa >>= ob) (Q₁ + Q₂)
        source
        theorem FiatShamir.nmaHashQueryBound_liftComp_zero {Commit Chal : Type} (M : Type) {α : Type} (oa : ProbComp α) :
        nmaHashQueryBound M (OracleComp.liftComp oa (unifSpec + OracleSpec.ofFn fun (x : M × Commit) => Chal)) 0
        source
        noncomputable def FiatShamir.challengeSpaceInv (challenge : Type) [Fintype challenge] :
        ENNReal

        Reciprocal of the finite challenge-space size.

        Instances For