Fiat-Shamir-with-aborts transform

Signing variant of Fiat-Shamir used by lattice schemes such as ML-DSA. On input (pk, sk, msg) the prover runs a commit-hash-respond loop up to maxAttempts times, returning the first non-aborting transcript or none if every attempt aborts.

This file holds the scheme definition, the random-oracle runtime bundle, and the core cache invariant that drives the correctness proof. Cost-accounting lemmas, expected-cost PMFs, and the EUF-CMA security statement live in the FiatShamir.WithAbort.Cost, FiatShamir.WithAbort.ExpectedCost, and FiatShamir.WithAbort.Security submodules.

References

• Barbosa et al., Fixing and Mechanizing the Security Proof of Fiat-Shamir with Aborts and Dilithium, CRYPTO 2023 (ePrint 2023/246)
• EasyCrypt FSabort.eca, SimplifiedScheme.ec
• NIST FIPS 204, Algorithms 2 (ML-DSA.Sign) and 3 (ML-DSA.Verify)

def fsAbortSignAttempt {Stmt Wit Commit PrvState Chal Resp : Type} {rel : Stmt → Wit → Bool} (ids : IdenSchemeWithAbort Stmt Wit Commit PrvState Chal Resp rel) {m : Type → Type v} [Monad m] (M : Type) [MonadLiftT ProbComp m] [HasQuery (OracleSpec.ofFn fun (x : M × Commit) => Chal) m] (pk : Stmt) (sk : Wit) (msg : M) : m (Commit × Option Resp)

One signing attempt for the Fiat-Shamir-with-aborts transform.

This performs a single commit-hash-respond cycle and returns the public commitment together with either a response or an abort marker. Unlike [fsAbortSignLoop], it never retries internally.

def fsAbortSignLoop {Stmt Wit Commit PrvState Chal Resp : Type} {rel : Stmt → Wit → Bool} (ids : IdenSchemeWithAbort Stmt Wit Commit PrvState Chal Resp rel) {m : Type → Type v} [Monad m] (M : Type) [MonadLiftT ProbComp m] [HasQuery (OracleSpec.ofFn fun (x : M × Commit) => Chal) m] (pk : Stmt) (sk : Wit) (msg : M) : ℕ → m (Option (Commit × Resp))

Signing retry loop with early return for the Fiat-Shamir with aborts transform.

Tries up to n commit-hash-respond cycles:

1. Commit to get (w', st)
2. Hash (msg, w') via the random oracle to get challenge c
3. Attempt to respond; if some z, return immediately; if none (abort), decrement the counter and retry.

Returns none only when all n attempts abort.

def FiatShamirWithAbort {Stmt Wit Commit PrvState Chal Resp : Type} {rel : Stmt → Wit → Bool} {m : Type → Type v} [Monad m] (ids : IdenSchemeWithAbort Stmt Wit Commit PrvState Chal Resp rel) (hr : GenerableRelation Stmt Wit rel) (M : Type) [MonadLiftT ProbComp m] [HasQuery (OracleSpec.ofFn fun (x : M × Commit) => Chal) m] (maxAttempts : ℕ) : SignatureAlg m M Stmt Wit (Option (Commit × Resp))

The Fiat-Shamir with aborts transform applied to an identification scheme with aborts. Produces a signature scheme in the random oracle model.

The signing algorithm runs fsAbortSignLoop (up to maxAttempts iterations) with early return on the first non-aborting response.

The type parameters are:

• M: message space
• Commit: public commitment (included in signature for verification)
• Chal: challenge space (range of the hash/random oracle)
• Resp: response space
• Stmt / Wit: statement / witness (= public key / secret key)

noncomputable def FiatShamirWithAbort.runtime {Commit Chal : Type} (M : Type) [DecidableEq M] [DecidableEq Commit] [SampleableType Chal] : ProbCompRuntime (OracleComp (unifSpec + OracleSpec.ofFn fun (x : M × Commit) => Chal))

Runtime bundle for the Fiat-Shamir-with-aborts random-oracle world.

theorem FiatShamirWithAbort.fsAbortSignLoop_cache_invariant {Stmt Wit Commit PrvState Chal Resp : Type} {rel : Stmt → Wit → Bool} (ids : IdenSchemeWithAbort Stmt Wit Commit PrvState Chal Resp rel) (M : Type) [DecidableEq M] [DecidableEq Commit] [SampleableType Chal] (ro : QueryImpl (OracleSpec.ofFn fun (x : M × Commit) => Chal) (StateT (OracleSpec.ofFn fun (x : M × Commit) => Chal).QueryCache ProbComp)) (hro : ro = randomOracle) (hc : ids.Complete) {pk : Stmt} {sk : Wit} (hrel : rel pk sk = true) (msg : M) (n : ℕ) (s₀ : (OracleSpec.ofFn fun (x : M × Commit) => Chal).QueryCache) (w : Commit) (z : Resp) (s : (OracleSpec.ofFn fun (x : M × Commit) => Chal).QueryCache) (hsup : (some (w, z), s) ∈ support ((simulateQ (unifFwdImpl (OracleSpec.ofFn fun (x : M × Commit) => Chal) + ro) (fsAbortSignLoop ids M pk sk msg n)).run s₀)) : ∃ (c : Chal), s (msg, w) = some c ∧ ids.verify pk w c z = true

When the simulated signing loop produces some (w, z), the random-oracle cache contains a challenge c at (msg, w) satisfying ids.verify pk w c z = true.

This is proved by induction on the loop counter: each abort iteration preserves the invariant (the cache only grows), and a successful iteration writes exactly the challenge used in verification.

theorem FiatShamirWithAbort.verify_eq_true_of_cached {Stmt Wit Commit PrvState Chal Resp : Type} {rel : Stmt → Wit → Bool} (ids : IdenSchemeWithAbort Stmt Wit Commit PrvState Chal Resp rel) (hr : GenerableRelation Stmt Wit rel) (M : Type) [DecidableEq M] [DecidableEq Commit] [SampleableType Chal] (ro : QueryImpl (OracleSpec.ofFn fun (x : M × Commit) => Chal) (StateT (OracleSpec.ofFn fun (x : M × Commit) => Chal).QueryCache ProbComp)) (hro : ro = randomOracle) (pk : Stmt) (msg : M) (maxAttempts : ℕ) (w : Commit) (z : Resp) (cache : (OracleSpec.ofFn fun (x : M × Commit) => Chal).QueryCache) (c : Chal) (hcached : cache (msg, w) = some c) (hverify : ids.verify pk w c z = true) : (simulateQ (unifFwdImpl (OracleSpec.ofFn fun (x : M × Commit) => Chal) + ro) ((FiatShamirWithAbort ids hr M maxAttempts).verify pk msg (some (w, z)))).run' cache = pure true

When the random-oracle cache already contains the challenge for (msg, w), verification of signature (w, z) deterministically returns true.

theorem FiatShamirWithAbort.correct {Stmt Wit Commit PrvState Chal Resp : Type} {rel : Stmt → Wit → Bool} (ids : IdenSchemeWithAbort Stmt Wit Commit PrvState Chal Resp rel) (hr : GenerableRelation Stmt Wit rel) (M : Type) [DecidableEq M] [DecidableEq Commit] [SampleableType Chal] (hc : ids.Complete) (maxAttempts : ℕ) (δ : ENNReal) (h_abort : ∀ (pk : Stmt) (sk : Wit), rel pk sk = true → ∀ (msg : M), Pr[= none | (runtime M).evalDist ((FiatShamirWithAbort ids hr M maxAttempts).sign pk sk msg)] ≤ δ) : (FiatShamirWithAbort ids hr M maxAttempts).Complete (runtime M) δ

Correctness of the Fiat-Shamir with aborts signature scheme: the canonical keygen-sign-verify execution succeeds with probability at least 1 - δ, where δ bounds the per-key probability that signing aborts (returns none).

When the underlying IDS is complete, any non-aborting signature verifies correctly (by RO consistency and IdenSchemeWithAbort.verify_of_complete). So the only source of verification failure is signing abort, and the completeness error equals the abort probability.

The hypothesis h_abort bounds the abort probability for each valid key pair separately. It can be discharged using sign_abortPrefixProbability_eq_signAttemptAbortProbability_pow, which gives Pr[sign = none] = signAttemptAbortProbability ^ maxAttempts for fixed keys.

Unlike the CRYPTO 2023 paper and EasyCrypt formalization (which use an unbounded signing loop and do not state a correctness theorem), this formulation uses a bounded loop with maxAttempts iterations, matching FIPS 204 Algorithm 7 (ML-DSA.Sign_internal).