Identification Scheme with Aborts

This file defines a structure for identification schemes with aborts, as used in ML-DSA (CRYSTALS-Dilithium). Unlike a standard Σ-protocol (SigmaProtocol), the prover's response may fail (abort), in which case the protocol is retried. This abort mechanism is essential for the security of lattice-based schemes where masking must hide the secret.

The structure follows the EasyCrypt formalization in IDSabort.ec (formosa-crypto/dilithium).

Type Parameters

• Stmt: statement (public key)
• Wit: witness (secret key)
• Commit: public commitment (sent to the verifier)
• PrvState: private prover state (retained between commit and respond)
• Chal: verifier challenge
• Resp: prover response
• rel: the relation proven by the protocol

Main Definitions

• IdenSchemeWithAbort: identification scheme where respond returns Option Resp
• IdenSchemeWithAbort.Complete: honest prover convinces verifier (conditioned on non-abort)
• IdenSchemeWithAbort.HVZK: transcript distribution is within a stated TV-distance of a simulator
• IdenSchemeWithAbort.PerfectHVZK: exact transcript distribution matching with a simulator
• IdenSchemeWithAbort.CommitmentRecoverable: ability to recover commitment from the transcript

References

• Fixing and Mechanizing the Security Proof of Fiat-Shamir with Aborts and Dilithium (CRYPTO 2023, ePrint 2023/246)
• EasyCrypt IDSabort.ec

structure IdenSchemeWithAbort (Stmt Wit Commit PrvState Chal Resp : Type) (rel : Stmt → Wit → Bool) : Type

An identification scheme with aborts for statements in Stmt and witnesses in Wit, where rel : Stmt → Wit → Bool is the proven relation. The prover's commitment is split into a public part Commit (sent to the verifier) and a private state PrvState. The verifier's challenge is in Chal, and the prover's response (which may abort) is in Resp.

Unlike SigmaProtocol, the respond function returns Option Resp — none indicates an abort and the protocol must be retried. This is the key mechanism used in Dilithium/ML-DSA to ensure that the response distribution is independent of the secret.

• commit (stmt : Stmt) (wit : Wit) : ProbComp (Commit × PrvState)

  Generate a commitment: returns a public commitment and private prover state.

• respond (stmt : Stmt) (wit : Wit) (prvState : PrvState) (chal : Chal) : ProbComp (Option Resp)

  Respond to a challenge. Returns none if the response would leak information about the secret (abort), in which case the protocol is retried from scratch.

• verify (stmt : Stmt) (commit : Commit) (chal : Chal) (resp : Resp) : Bool

  Deterministic verification: check that the response is valid for the given statement, commitment, and challenge.

def IdenSchemeWithAbort.honestExecution {Stmt Wit Commit PrvState Chal Resp : Type} {rel : Stmt → Wit → Bool} [SampleableType Chal] (ids : IdenSchemeWithAbort Stmt Wit Commit PrvState Chal Resp rel) (s : Stmt) (w : Wit) : ProbComp (Option (Commit × Chal × Resp))

A single honest execution producing an optional transcript (Commit, Chal, Resp). Returns none if the prover aborts.

def IdenSchemeWithAbort.Complete {Stmt Wit Commit PrvState Chal Resp : Type} {rel : Stmt → Wit → Bool} [SampleableType Chal] [unifSpec.Fintype] [unifSpec.Inhabited] (ids : IdenSchemeWithAbort Stmt Wit Commit PrvState Chal Resp rel) : Prop

An identification scheme with aborts is complete if: whenever the prover does not abort, the verifier always accepts.

theorem IdenSchemeWithAbort.verify_of_complete {Stmt Wit Commit PrvState Chal Resp : Type} {rel : Stmt → Wit → Bool} [SampleableType Chal] [unifSpec.Fintype] [unifSpec.Inhabited] (ids : IdenSchemeWithAbort Stmt Wit Commit PrvState Chal Resp rel) (hc : ids.Complete) {s : Stmt} {w : Wit} (hrel : rel s w = true) {cm : Commit} {c : Chal} {z : Resp} (h_mem : some (cm, c, z) ∈ support (ids.honestExecution s w)) : ids.verify s cm c z = true

Support-level consequence of completeness: any non-aborting honest transcript in the support has an accepting verification.

def IdenSchemeWithAbort.HVZK {Stmt Wit Commit PrvState Chal Resp : Type} {rel : Stmt → Wit → Bool} [SampleableType Chal] [unifSpec.Fintype] [unifSpec.Inhabited] (ids : IdenSchemeWithAbort Stmt Wit Commit PrvState Chal Resp rel) (sim : Stmt → ProbComp (Option (Commit × Chal × Resp))) (ζ_zk : ℝ) : Prop

Approximate honest-verifier zero-knowledge for an identification scheme with aborts: the transcript distribution produced by the honest prover is within total variation distance ζ_zk of the distribution produced by the simulator.

Both distributions are over Option (Commit × Chal × Resp), where none represents an abort. The parameter ζ_zk captures both transcript mismatch and abort-probability mismatch.

def IdenSchemeWithAbort.PerfectHVZK {Stmt Wit Commit PrvState Chal Resp : Type} {rel : Stmt → Wit → Bool} [SampleableType Chal] [unifSpec.Fintype] [unifSpec.Inhabited] (ids : IdenSchemeWithAbort Stmt Wit Commit PrvState Chal Resp rel) (sim : Stmt → ProbComp (Option (Commit × Chal × Resp))) : Prop

Exact honest-verifier zero-knowledge for an identification scheme with aborts: the transcript distribution produced by the honest prover exactly matches the distribution produced by the simulator.

theorem IdenSchemeWithAbort.perfectHVZK_iff_hvzk_zero {Stmt Wit Commit PrvState Chal Resp : Type} {rel : Stmt → Wit → Bool} [SampleableType Chal] [unifSpec.Fintype] [unifSpec.Inhabited] (ids : IdenSchemeWithAbort Stmt Wit Commit PrvState Chal Resp rel) (sim : Stmt → ProbComp (Option (Commit × Chal × Resp))) : ids.PerfectHVZK sim ↔ ids.HVZK sim 0

The perfect HVZK property is equivalent to the approximate HVZK property with ζ_zk = 0.

def IdenSchemeWithAbort.CommitmentRecoverable {Stmt Wit Commit PrvState Chal Resp : Type} {rel : Stmt → Wit → Bool} (ids : IdenSchemeWithAbort Stmt Wit Commit PrvState Chal Resp rel) (recover : Stmt → Chal → Resp → Commit) : Prop

Commitment recoverability: any accepting transcript determines the public commitment from the statement, challenge, and response alone. This property is required for the CMA-to-NMA reduction in the Fiat-Shamir with aborts security proof.

In Dilithium/ML-DSA, the commitment w1 can be recomputed as highBits(Az - c*t).

structure IdenSchemeWithAbort.ImpAdv {Stmt Wit Commit PrvState Chal Resp : Type} {rel : Stmt → Wit → Bool} (ids : IdenSchemeWithAbort Stmt Wit Commit PrvState Chal Resp rel) (AdvSt : Type) : Type

An adversary for the impersonation game against an identification scheme with aborts. The adversary sees the public key (statement), produces a commitment together with an internal state, and then responds to a challenge using that state.

• commit (s : Stmt) : ProbComp (Commit × AdvSt)
• respond (s : Stmt) (c : Chal) (st : AdvSt) : ProbComp Resp

def IdenSchemeWithAbort.impExp {Stmt Wit Commit PrvState Chal Resp : Type} {rel : Stmt → Wit → Bool} [SampleableType Chal] {ids : IdenSchemeWithAbort Stmt Wit Commit PrvState Chal Resp rel} {AdvSt : Type} (adv : ids.ImpAdv AdvSt) (s : Stmt) : ProbComp Bool

The impersonation experiment: the adversary tries to produce a valid transcript without knowing the witness, against a fixed statement s.