Documentation

VCVio.CryptoFoundations.FiatShamir.WithAbort.Security

EUF-CMA security of Fiat-Shamir with aborts #

Statistical CMA-to-NMA reduction for the Fiat-Shamir-with-aborts transform, matching Theorem 3 of Barbosa et al. (CRYPTO 2023). Instantiates FiatShamir.signHashQueryBound at the with-aborts signature type and exposes cmaToNmaLoss plus euf_cma_bound / euf_cma_bound_perfectHVZK.

The scheme-specific NMA-to-hard-problem reduction lives with each concrete scheme (e.g. MLDSA.nma_security).

source
noncomputable def FiatShamirWithAbort.cmaToNmaLoss (qS qH : ℕ) (ε p ζ_zk δ : ℝ) (_hp : p < 1) :
ℝ

The exact classical ROM statistical loss from the Fiat-Shamir-with-aborts CMA-to-NMA reduction (Theorem 3, CRYPTO 2023), parameterized by the HVZK simulator error ζ_zk.

The paper proves

`Adv_EUF-CMA(A) ≤ Adv_EUF-NMA(B)

  • 2·qS·(qH+1)·ε/(1-p)
  • qS·ε·(qS+1)/(2·(1-p)^2)
  • qS·ζ_zk
  • δ`

where:

  • qS: number of signing-oracle queries
  • qH: number of adversarial random-oracle queries
  • ε: commitment-guessing bound
  • p: effective abort probability
  • ζ_zk: total-variation error of the HVZK simulator for one signing transcript
  • δ: regularity failure probability

The qH + 1 term comes from applying the paper's hybrid bounds to the forging experiment, which adds one final verification query to the random oracle.

Instances For
    source
    theorem FiatShamirWithAbort.euf_cma_bound {Stmt Wit Commit PrvState Chal Resp : Type} {rel : Stmt → Wit → Bool} [SampleableType Stmt] [DecidableEq Commit] [SampleableType Chal] (ids : IdenSchemeWithAbort Stmt Wit Commit PrvState Chal Resp rel) (hr : GenerableRelation Stmt Wit rel) (M : Type) [DecidableEq M] (maxAttempts : ℕ) (hc : ids.Complete) (sim : Stmt → ProbComp (Option (Commit × Chal × Resp))) (ζ_zk : ℝ) (hζ : 0 ≤ ζ_zk) (hhvzk : ids.HVZK sim ζ_zk) (recover : Stmt → Chal → Resp → Commit) (hcr : ids.CommitmentRecoverable recover) (adv : (FiatShamirWithAbort ids hr M maxAttempts).unforgeableAdv) (qS qH : ℕ) (ε p_abort δ : ℝ) (hp : p_abort < 1) (hQ : ∀ (pk : Stmt), FiatShamir.signHashQueryBound M (adv.main pk) qS qH) :
    ∃ (reduction : Stmt → ProbComp Wit), SignatureAlg.unforgeableAdv.advantage (runtime M) adv ≤ Pr[= true | hardRelationExp hr reduction] + ENNReal.ofReal (cmaToNmaLoss qS qH ε p_abort ζ_zk δ hp)

    CMA-to-NMA reduction for Fiat-Shamir with aborts (Theorem 3, CRYPTO 2023).

    For any EUF-CMA adversary A making at most qS signing-oracle queries and qH random-oracle queries, there exists an NMA reduction such that:

    Adv^{EUF-CMA}(A) ≤ Adv^{EUF-NMA}(B) + L

    The reduction uses:

    1. The quantitative HVZK simulator sim to answer signing queries without the secret key
    2. Commitment recoverability recover to map between the standard and commitment-recoverable variants of the signature scheme
    3. Nested hybrid arguments over ROM reprogramming (accepted and rejected transcripts)

    The statistical loss L involves the commitment guessing probability ε, the effective abort probability p, the simulator error ζ_zk, the regularity failure probability δ, and the query bounds qS, qH; it is captured here by cmaToNmaLoss.

    The scheme-specific reduction from NMA to computational assumptions (e.g., MLWE + SelfTargetMSIS for ML-DSA) is stated separately; see MLDSA.nma_security and MLDSA.euf_cma_security.

    source
    theorem FiatShamirWithAbort.euf_cma_bound_perfectHVZK {Stmt Wit Commit PrvState Chal Resp : Type} {rel : Stmt → Wit → Bool} [SampleableType Stmt] [DecidableEq Commit] [SampleableType Chal] (ids : IdenSchemeWithAbort Stmt Wit Commit PrvState Chal Resp rel) (hr : GenerableRelation Stmt Wit rel) (M : Type) [DecidableEq M] (maxAttempts : ℕ) (hc : ids.Complete) (sim : Stmt → ProbComp (Option (Commit × Chal × Resp))) (hhvzk : ids.PerfectHVZK sim) (recover : Stmt → Chal → Resp → Commit) (hcr : ids.CommitmentRecoverable recover) (adv : (FiatShamirWithAbort ids hr M maxAttempts).unforgeableAdv) (qS qH : ℕ) (ε p_abort δ : ℝ) (hp : p_abort < 1) (hQ : ∀ (pk : Stmt), FiatShamir.signHashQueryBound M (adv.main pk) qS qH) :
    ∃ (reduction : Stmt → ProbComp Wit), SignatureAlg.unforgeableAdv.advantage (runtime M) adv ≤ Pr[= true | hardRelationExp hr reduction] + ENNReal.ofReal (cmaToNmaLoss qS qH ε p_abort 0 δ hp)

    Perfect-HVZK special case of euf_cma_bound, where the simulator contributes no qS · ζ_zk loss term.