Signature Algorithms

This file defines SignatureAlg m M PK SK S, a type representing a digital signature scheme with computations in the monad m, message space M, public/secret key spaces PK/SK, and signature space S.

structure SignatureAlg (m : Type → Type v) [Monad m] (M PK SK S : Type) : Type v

Signature algorithm with computations in the monad m, where M is the space of messages, PK/SK are the spaces of the public/private keys, and S is the type of the final signature.

• keygen : m (PK × SK)
• sign (pk : PK) (sk : SK) (msg : M) : m S
• verify (pk : PK) (msg : M) (σ : S) : m Bool

theorem SignatureAlg.ext_iff {m : Type → Type v} {inst✝ : Monad m} {M PK SK S : Type} {x y : SignatureAlg m M PK SK S} : x = y ↔ x.keygen = y.keygen ∧ x.sign = y.sign ∧ x.verify = y.verify

theorem SignatureAlg.ext {m : Type → Type v} {inst✝ : Monad m} {M PK SK S : Type} {x y : SignatureAlg m M PK SK S} (keygen : x.keygen = y.keygen) (sign : x.sign = y.sign) (verify : x.verify = y.verify) : x = y

def SignatureAlg.signingOracle {m : Type → Type v} [Monad m] {M PK SK S : Type} (sigAlg : SignatureAlg m M PK SK S) (pk : PK) (sk : SK) : QueryImpl (OracleSpec.ofFn fun (x : M) => S) (WriterT (OracleSpec.ofFn fun (x : M) => S).QueryLog m)

In the new API, QueryImpl (M →ₒ S) is just M → m S (since Domain = M). The old version used ⟨fun | query () msg => ...⟩ which matched the old struct-based API.

def SignatureAlg.map {m : Type → Type v} [Monad m] {n : Type → Type u} [Monad n] {M PK SK S : Type} (F : m →ᵐ n) (sigAlg : SignatureAlg m M PK SK S) : SignatureAlg n M PK SK S

Transport a signature scheme across a monad morphism by mapping each algorithmic component.

This is the basic reindexing operation used by naturality theorems for generic constructions: if a signature scheme was defined in a source monad m, then any monad morphism m →ᵐ n induces the corresponding scheme in n.

@[simp]

theorem SignatureAlg.map_keygen {m : Type → Type v} [Monad m] {n : Type → Type u} [Monad n] {M PK SK S : Type} (F : m →ᵐ n) (sigAlg : SignatureAlg m M PK SK S) : (map F sigAlg).keygen = (fun {α : Type} (x : m α) => F.toFun α x) sigAlg.keygen

@[simp]

theorem SignatureAlg.map_sign {m : Type → Type v} [Monad m] {n : Type → Type u} [Monad n] {M PK SK S : Type} (F : m →ᵐ n) (sigAlg : SignatureAlg m M PK SK S) (pk : PK) (sk : SK) (msg : M) : (map F sigAlg).sign pk sk msg = (fun {α : Type} (x : m α) => F.toFun α x) (sigAlg.sign pk sk msg)

@[simp]

theorem SignatureAlg.map_verify {m : Type → Type v} [Monad m] {n : Type → Type u} [Monad n] {M PK SK S : Type} (F : m →ᵐ n) (sigAlg : SignatureAlg m M PK SK S) (pk : PK) (msg : M) (σ : S) : (map F sigAlg).verify pk msg σ = (fun {α : Type} (x : m α) => F.toFun α x) (sigAlg.verify pk msg σ)

def SignatureAlg.Complete {m : Type → Type v} [Monad m] {M PK SK S : Type} (sigAlg : SignatureAlg m M PK SK S) (runtime : ProbCompRuntime m) (δ : ENNReal) : Prop

Completeness of a signature scheme with error δ: for every message, the canonical keygen-sign-verify execution accepts with probability at least 1 - δ.

The error δ captures all sources of failure, including both verification mismatches and signing failures (e.g., abort in schemes like Fiat-Shamir with aborts).

Complete sigAlg runtime 0 is equivalent to PerfectlyComplete sigAlg runtime.

def SignatureAlg.PerfectlyComplete {m : Type → Type v} [Monad m] {M PK SK S : Type} (sigAlg : SignatureAlg m M PK SK S) (runtime : ProbCompRuntime m) : Prop

Perfect completeness: the canonical keygen-sign-verify execution always accepts. This is the special case of Complete with zero error.

theorem SignatureAlg.perfectlyComplete_iff_complete_zero {m : Type → Type v} [Monad m] {M PK SK S : Type} (sigAlg : SignatureAlg m M PK SK S) (runtime : ProbCompRuntime m) : sigAlg.PerfectlyComplete runtime ↔ sigAlg.Complete runtime 0

theorem SignatureAlg.Complete.mono {m : Type → Type v} [Monad m] {M PK SK S : Type} {sigAlg : SignatureAlg m M PK SK S} {runtime : ProbCompRuntime m} {δ₁ δ₂ : ENNReal} (h : sigAlg.Complete runtime δ₁) (hle : δ₁ ≤ δ₂) : sigAlg.Complete runtime δ₂

theorem SignatureAlg.probOutput_bind_ge_of_forall_support {α β : Type} {a : β} {δ : ENNReal} (gen : ProbComp α) (f : α → ProbComp β) (h : ∀ x ∈ support gen, Pr[= a | f x] ≥ 1 - δ) : Pr[= a | gen >>= f] ≥ 1 - δ

If every key pair (pk, sk) in the support of a generator satisfies Pr[= a | f pk sk] ≥ 1 - δ, then the overall probability Pr[= a | gen >>= f] ≥ 1 - δ. This reduces a "for all keys" completeness statement to per-key bounds.

structure SignatureAlg.unforgeableAdv {ι : Type u} {spec : OracleSpec ι} {M PK SK S : Type} (_sigAlg : SignatureAlg (OracleComp spec) M PK SK S) : Type u

• main (pk : PK) : OracleComp (spec + OracleSpec.ofFn fun (x : M) => S) (M × S)

noncomputable def SignatureAlg.unforgeableExp {ι : Type u} {spec : OracleSpec ι} {M PK SK S : Type} {sigAlg : SignatureAlg (OracleComp spec) M PK SK S} (runtime : ProbCompRuntime (OracleComp spec)) (adv : sigAlg.unforgeableAdv) : SPMF Bool

Unforgeability experiment for a signature algorithm: runs the adversary and checks whether the adversary successfully forged a signature. The ambient oracle family is forwarded unchanged, the signing oracle is logged, and the final check requires both signature validity and that the forged message was never submitted to the signing oracle.

noncomputable def SignatureAlg.unforgeableAdv.advantage {ι : Type u} {spec : OracleSpec ι} {M PK SK S : Type} {sigAlg : SignatureAlg (OracleComp spec) M PK SK S} (runtime : ProbCompRuntime (OracleComp spec)) (adv : sigAlg.unforgeableAdv) : ENNReal

The success probability of a CMA adversary in the unforgeability experiment.

structure SignatureAlg.eufNmaAdv {ι : Type u} {spec : OracleSpec ι} {M PK SK S : Type} (_sigAlg : SignatureAlg (OracleComp spec) M PK SK S) : Type (max u u_1)

An EUF-NMA (existential unforgeability under no-message attack) adversary for a signature scheme. Unlike a CMA adversary (unforgeableAdv), the NMA adversary has NO access to a signing oracle — it must forge a signature having only seen the public key.

In the random oracle model, the adversary still has access to the scheme's oracle spec (e.g., the random oracle H), but never sees any legitimately generated signatures.

• main (pk : PK) : OracleComp spec (M × S)

def SignatureAlg.eufNmaExp {ι : Type u} {spec : OracleSpec ι} {M PK SK S : Type} {sigAlg : SignatureAlg (OracleComp spec) M PK SK S} (runtime : ProbCompRuntime (OracleComp spec)) (adv : sigAlg.eufNmaAdv) : SPMF Bool

The EUF-NMA experiment: generate a key pair, give the public key to the adversary (with no signing oracle), and check whether the adversary produced a valid forgery.

noncomputable def SignatureAlg.eufNmaAdv.advantage {ι : Type u} {spec : OracleSpec ι} {M PK SK S : Type} {sigAlg : SignatureAlg (OracleComp spec) M PK SK S} (runtime : ProbCompRuntime (OracleComp spec)) (adv : sigAlg.eufNmaAdv) : ENNReal

The success probability of an EUF-NMA adversary.

structure SignatureAlg.managedRoNmaAdv {ι : Type} {spec : OracleSpec ι} {M PK SK S : Type} (sigAlg : SignatureAlg (OracleComp spec) M PK SK S) : Type u_1

An EUF-NMA adversary with managed random oracle: the adversary returns a QueryCache alongside its forgery. The experiment verifies using withCacheOverlay, which resolves cached entries from the adversary's table and forwards misses to the real oracle.

This supports compositional CMA-to-NMA reductions: the CMA-to-NMA reduction programs hash entries for signing simulation into the cache, while forwarding the inner adversary's hash queries to the external oracle. The forking lemma (Fork.fork) can then replay the external oracle queries via seeded simulation, while the programmed entries are preserved deterministically.

• main (pk : PK) : OracleComp spec ((M × S) × spec.QueryCache)

def SignatureAlg.managedRoNmaExp {ι : Type} [DecidableEq ι] {spec : OracleSpec ι} {M PK SK S : Type} {sigAlg : SignatureAlg (OracleComp spec) M PK SK S} (runtime : ProbCompRuntime (OracleComp spec)) (adv : sigAlg.managedRoNmaAdv) : SPMF Bool

The managed-RO NMA experiment: generate a key pair, run the adversary to get a forgery and a QueryCache, then verify the forgery through withCacheOverlay so that programmed entries take priority over the real oracle.

noncomputable def SignatureAlg.managedRoNmaAdv.advantage {ι : Type} [DecidableEq ι] {spec : OracleSpec ι} {M PK SK S : Type} {sigAlg : SignatureAlg (OracleComp spec) M PK SK S} (runtime : ProbCompRuntime (OracleComp spec)) (adv : sigAlg.managedRoNmaAdv) : ENNReal

The success probability of a managed-RO NMA adversary.

def SignatureAlg.eufNmaAdv.toManagedRoNmaAdv {ι : Type} {spec : OracleSpec ι} {M PK SK S : Type} {sigAlg : SignatureAlg (OracleComp spec) M PK SK S} (adv : sigAlg.eufNmaAdv) : sigAlg.managedRoNmaAdv

Embed a standard NMA adversary as a managed-RO NMA adversary with an empty cache. The empty cache means all queries fall through to the real oracle, recovering the standard NMA experiment.