GPV Hash-and-Sign Framework

This file defines a generic hash-and-sign signature scheme following the GPV (Gentry–Peikert– Vaikuntanathan) framework [GPV08]. The construction is parameterized by a preimage sampleable function (PSF), a many-to-one function equipped with a probabilistic trapdoor that samples short preimages.

The GPV framework is the hash-and-sign analogue of the Fiat-Shamir transform:

Interactive protocol	Fiat-Shamir → SignatureAlg
Trapdoor PSF	GPVHashAndSign → SignatureAlg

Main Definitions

• PreimageSampleableFunction — a function eval with a probabilistic trapdoor sampler and a shortness predicate on preimages.
• GPVHashAndSign — builds a SignatureAlg in the random-oracle model from a PSF, a generable key relation, and a salt type.

Security

The PFDH (Probabilistic Full-Domain Hash) variant of the GPV scheme uses a random salt per signing query. The precise EUF-CMA bound from [FGdG+25] Theorem 1 is:

Adv^{UF-CMA}(A) ≤ (r_u^{C_s} · (r_p^{C_s} · Adv^{ISIS}(B))^{...})^{...} + tail_bound + Q_s · (C_s + Q_H) / 2^k

where the salt-collision term Q_s · (C_s + Q_H) / 2^k bounds the probability that a fresh salt collides with any prior RO query. The simpler birthday bound qSign² / (2 · |Salt|) from GPV08 Prop 6.2 is slightly looser but still valid and is the one we formalize here.

The proof decomposes into:

• GPVHashAndSign.reduction: the collision-finding adversary (sign-then-hash simulation)
• GPVHashAndSign.programmedPreimageReduction: the exact-match branch reduction
• GPVHashAndSign.collisionBound: the salt-collision birthday bound
• GPVHashAndSign.forgery_yields_collision: the core distinct-preimage game-hop
• GPVHashAndSign.forgery_yields_collision_or_exact_match: the explicit split bound

References

• [FGdG+25]: Fouque, Gajland, de Groote, Janneck, Kiltz. "A Closer Look at Falcon." ePrint 2024/1769. First concrete proof for Falcon+ (Theorem 1).
• [Jia+26]: Jia, Zhang, Yu, Tang. "Revisiting the Concrete Security of Falcon-type Signatures." ePrint 2026/096. Tightens Rényi loss to < 0.2 bits.
• GPV08: Gentry, Peikert, Vaikuntanathan. STOC 2008, Propositions 6.1–6.2.
• BDF+11: Boneh et al. "Random Oracles in a Quantum World." ASIACRYPT 2011.

Preimage Sampleable Functions

structure PreimageSampleableFunction (PK SK Domain Range : Type) : Type

A preimage sampleable function (PSF) consists of:

• A public evaluation map eval : PK → Domain → Range.
• A probabilistic trapdoor sampler trapdoorSample that, given the secret key and a target in the range, produces a preimage in the domain.
• A shortness predicate isShort that the verifier checks on purported preimages.

This abstracts the core primitive in the GPV hash-and-sign framework. Unlike TrapdoorPermutation (in OneWay.lean), a PSF is many-to-one, the inversion is probabilistic, and acceptance depends on a quality predicate rather than exact inversion.

• eval : PK → Domain → Range
• trapdoorSample : PK → SK → Range → ProbComp Domain
• isShort : Domain → Bool

def PreimageSampleableFunction.Correct {PK SK Domain Range : Type} (psf : PreimageSampleableFunction PK SK Domain Range) : Prop

A PSF is correct if the trapdoor sampler always produces a valid preimage that is accepted by the shortness predicate.

GPV Hash-and-Sign Construction

def GPVHashAndSign {m : Type → Type v} [Monad m] {PK SK Domain Range : Type} (psf : PreimageSampleableFunction PK SK Domain Range) {p : PK → SK → Bool} (hr : GenerableRelation PK SK p) (M Salt : Type) [DecidableEq M] [DecidableEq Salt] [SampleableType Salt] [DecidableEq Range] [SampleableType Range] [MonadLiftT ProbComp m] [HasQuery (OracleSpec.ofFn fun (x : Salt × M) => Range) m] : SignatureAlg m M PK SK (Salt × Domain)

The GPV hash-and-sign signature scheme in the random-oracle model.

Given a preimage sampleable function psf, a generable key relation hr, and a salt type Salt, the construction builds a SignatureAlg where:

• keygen: sample a key pair from hr.gen.
• sign pk sk m: sample a random salt r, query the random oracle at (r, m) to obtain a target c, use trapdoorSample to find a short preimage s of c, and return (r, s).
• verify pk m (r, s): recompute c from the random oracle at (r, m), then check that eval pk s = c and isShort s.

The signature type is Salt × Domain (salt paired with the short preimage). The oracle spec is unifSpec + (Salt × M →ₒ Range) (uniform sampling + random oracle).

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

Runtime bundle for the GPV hash-and-sign random-oracle world.

def GPVHashAndSign.hashQueryBound {Range : Type} (M Salt : Type) {S' α : Type} (oa : OracleComp ((unifSpec + OracleSpec.ofFn fun (x : Salt × M) => Range) + OracleSpec.ofFn fun (x : M) => S') α) (Q : ℕ) : Prop

Structural bound that counts only random-oracle queries in a GPV EUF-CMA adversary.

def GPVHashAndSign.signHashQueryBound {Range : Type} (M Salt : Type) {S' α : Type} (oa : OracleComp ((unifSpec + OracleSpec.ofFn fun (x : Salt × M) => Range) + OracleSpec.ofFn fun (x : M) => S') α) (qSign qHash : ℕ) : Prop

Structural query bound for GPV EUF-CMA adversaries that tracks both signing-oracle queries (qSign) and random-oracle queries (qHash). Uniform-sampling queries are unrestricted.

@[reducible, inline]

abbrev GPVHashAndSign.CollisionAdversary {PK Domain : Type} : Type

A collision-finding adversary receives a public key and must produce two distinct short preimages with the same image under psf.eval.

def GPVHashAndSign.collisionFindingExp {PK SK Domain Range : Type} {p : PK → SK → Bool} [DecidableEq Range] (psf : PreimageSampleableFunction PK SK Domain Range) (hr : GenerableRelation PK SK p) [DecidableEq Domain] (adversary : CollisionAdversary) : ProbComp Bool

Keyed collision-finding experiment for a preimage sampleable function.

noncomputable def GPVHashAndSign.collisionFindingAdvantage {PK SK Domain Range : Type} {p : PK → SK → Bool} [DecidableEq Range] (psf : PreimageSampleableFunction PK SK Domain Range) (hr : GenerableRelation PK SK p) [DecidableEq Domain] (adversary : CollisionAdversary) : ENNReal

Success probability in the keyed collision-finding experiment.

@[reducible, inline]

abbrev GPVHashAndSign.ProgrammedPreimageAdversary {PK Domain Range : Type} : Type

A programmed-preimage adversary receives a public key and a programmed target y, and tries to reproduce the challenger's hidden short preimage sampled for y.

def GPVHashAndSign.programmedPreimageExp {PK SK Domain Range : Type} {p : PK → SK → Bool} [SampleableType Range] (psf : PreimageSampleableFunction PK SK Domain Range) (hr : GenerableRelation PK SK p) [DecidableEq Domain] (adversary : ProgrammedPreimageAdversary) : ProbComp Bool

Exact-match experiment for the hidden programmed-preimage branch of the GPV proof.

The challenger samples an honest key pair, then chooses a uniformly random target y and a hidden short preimage x ← trapdoorSample pk sk y. The adversary sees only (pk, y) and succeeds iff it reproduces exactly the hidden programmed preimage x.

noncomputable def GPVHashAndSign.programmedPreimageAdvantage {PK SK Domain Range : Type} {p : PK → SK → Bool} [SampleableType Range] (psf : PreimageSampleableFunction PK SK Domain Range) (hr : GenerableRelation PK SK p) [DecidableEq Domain] (adversary : ProgrammedPreimageAdversary) : ENNReal

Success probability in the exact-match programmed-preimage experiment.

Proof Decomposition

The EUF-CMA security proof proceeds by a game-hopping argument:

Game 0: The real EUF-CMA experiment with a lazy random oracle and the honest signing oracle (trapdoor sampler).

Game 1: Replace signing with "sign-then-hash": for each signing query on message m, sample a short preimage s ← D_short, set c := psf.eval pk s, program the RO at (r, m) := c, and return (r, s). This is indistinguishable from Game 0 when the PSF sampler is correct (the output distribution conditioned on the target is the same).

Bad event: A salt collision occurs (two distinct signing queries or the forgery reuse the same (salt, message) pair as a prior RO entry). Under the birthday bound, this happens with probability at most q_S² / (2 · |Salt|).

Game 2 (reduction): The simulator programs the random oracle with hidden short preimages. If the adversary forges on a fresh (salt, message) pair and the forged short preimage differs from the simulator's hidden programmed preimage at that point, the pair forms a collision under psf.eval.

The exact-match branch, where the forgery reproduces the simulator's programmed preimage, is a separate one-way/min-entropy obligation and is intentionally not encoded in the collision game below.

noncomputable def GPVHashAndSign.reduction {PK SK Domain Range : Type} {p : PK → SK → Bool} [DecidableEq Range] [SampleableType Range] (psf : PreimageSampleableFunction PK SK Domain Range) (hr : GenerableRelation PK SK p) (M Salt : Type) [DecidableEq M] [DecidableEq Salt] [SampleableType Salt] (adv : (GPVHashAndSign psf hr M Salt).unforgeableAdv) : CollisionAdversary

The collision-branch GPV reduction adversary. Given a public key pk, the reduction internally simulates the CMA experiment for the adversary:

1. Program a lazy random oracle, storing for each entry the hidden short preimage used to define that entry.
2. Answer signing queries using the sign-then-hash strategy: sample a short preimage s via trapdoorSample, compute c = psf.eval pk s, and program the RO at (r, msg) := c. Return (r, s) as the signature.
3. Run the adversary and, on a successful fresh forgery, return the simulator's hidden programmed preimage together with the forged preimage as a candidate collision.

The key insight is that in the sign-then-hash game, the reduction controls the entire RO table. If the adversary forges on a fresh (r*, msg*) pair, the RO value at that point was set by the reduction, so the hidden programmed preimage and the forged preimage land at the same image under psf.eval.

The detailed construction simulates the adversary's oracle interactions by maintaining a programmable RO state, using PSF correctness to ensure consistency.

noncomputable def GPVHashAndSign.programmedPreimageReduction {PK SK Domain Range : Type} {p : PK → SK → Bool} [DecidableEq Range] [SampleableType Range] (psf : PreimageSampleableFunction PK SK Domain Range) (hr : GenerableRelation PK SK p) (M Salt : Type) [DecidableEq M] [DecidableEq Salt] [SampleableType Salt] (adv : (GPVHashAndSign psf hr M Salt).unforgeableAdv) : ProgrammedPreimageAdversary

The exact-match branch reduction adversary. Given a public key pk and programmed target y, the reduction embeds (pk, y) at one guessed programmed random-oracle entry. If the adversary later forges on that entry and exactly reproduces the simulator's hidden preimage, the reduction wins the programmed-preimage game.

Because the target must be embedded at one guessed programmed entry, this branch incurs an explicit multi-target loss proportional to the total number of programmed entries.

noncomputable def GPVHashAndSign.collisionBound (Salt : Type) [Fintype Salt] (qSign : ℕ) : ENNReal

The salt-collision birthday bound (GPV08, Proposition 6.2).

For qSign signing queries with salts drawn uniformly from a set of size |Salt|, the birthday bound gives collision probability at most qSign² / (2 · |Salt|).

For Falcon with 40-byte salts (|Salt| = 2^320) and qSign ≤ 2^64: collisionBound (Bytes 40) (2^64) = 2^128 / (2 · 2^320) = 2^{-193}

theorem GPVHashAndSign.forgery_yields_collision {PK SK Domain Range : Type} {p : PK → SK → Bool} [DecidableEq Range] [SampleableType Range] (psf : PreimageSampleableFunction PK SK Domain Range) (hr : GenerableRelation PK SK p) (M Salt : Type) [DecidableEq M] [DecidableEq Salt] [SampleableType Salt] [Fintype Salt] [DecidableEq Domain] (hcorrect : psf.Correct) (qSign qHash : ℕ) (adv : (GPVHashAndSign psf hr M Salt).unforgeableAdv) (hQ : ∀ (pk : PK), signHashQueryBound M Salt (adv.main pk) qSign qHash) : SignatureAlg.unforgeableAdv.advantage (runtime M Salt) adv ≤ collisionFindingAdvantage psf hr (reduction psf hr M Salt adv) + collisionBound Salt qSign

Collision branch of the GPV game-hop: when the PSF is correct and the adversary makes at most qSign signing queries and qHash random-oracle queries, the probability that it produces a fresh forgery whose preimage differs from the simulator's programmed preimage is bounded by the collision-finding advantage of the reduction plus the salt-collision birthday bound.

The argument proceeds in two steps:

Step 1 (sign-then-hash ≡ real). Replace the signing oracle with one that: (a) samples a fresh salt r ← Salt, (b) samples a short preimage s using the trapdoor sampler on a fresh random target, (c) programs the RO at (r, msg) := psf.eval pk s. By PSF correctness (hcorrect), the joint distribution (r, s, H(r, msg)) is identical to the real game. This step is exact (zero statistical distance).

Step 2 (extract collision). In the sign-then-hash game, every RO entry is programmed by the simulator together with a hidden short preimage. If the adversary's fresh forgery (msg*, (r*, s*)) lands on a programmed entry and s* differs from the simulator's hidden preimage for that entry, the pair is a valid collision under psf.eval. The salt-collision probability bounds the only way the programming can become inconsistent.

theorem GPVHashAndSign.forgery_yields_collision_or_exact_match {PK SK Domain Range : Type} {p : PK → SK → Bool} [DecidableEq Range] [SampleableType Range] (psf : PreimageSampleableFunction PK SK Domain Range) (hr : GenerableRelation PK SK p) (M Salt : Type) [DecidableEq M] [DecidableEq Salt] [SampleableType Salt] [Fintype Salt] [DecidableEq Domain] (hcorrect : psf.Correct) (qSign qHash : ℕ) (adv : (GPVHashAndSign psf hr M Salt).unforgeableAdv) (hQ : ∀ (pk : PK), signHashQueryBound M Salt (adv.main pk) qSign qHash) : SignatureAlg.unforgeableAdv.advantage (runtime M Salt) adv ≤ collisionFindingAdvantage psf hr (reduction psf hr M Salt adv) + ↑(qSign + qHash) * programmedPreimageAdvantage psf hr (programmedPreimageReduction psf hr M Salt adv) + collisionBound Salt qSign

Full split GPV game-hop: every successful fresh forgery falls into one of two cases.

1. Distinct-preimage branch: the forgery differs from the simulator's hidden programmed preimage at the forged point, yielding a collision under psf.eval.
2. Exact-match branch: the forgery exactly reproduces the simulator's hidden programmed preimage at that point. To capture this branch, the reduction guesses one of the at most qSign + qHash programmed entries and turns success there into a win in the single-target programmed-preimage experiment.

The only additional failure mode is a salt collision, bounded by collisionBound.

theorem GPVHashAndSign.euf_cma_collision_bound {PK SK Domain Range : Type} {p : PK → SK → Bool} [DecidableEq Range] [SampleableType Range] (psf : PreimageSampleableFunction PK SK Domain Range) (hr : GenerableRelation PK SK p) (M Salt : Type) [DecidableEq M] [DecidableEq Salt] [SampleableType Salt] [Fintype Salt] [DecidableEq Domain] (hcorrect : psf.Correct) (qSign qHash : ℕ) (adv : (GPVHashAndSign psf hr M Salt).unforgeableAdv) (hQ : ∀ (pk : PK), signHashQueryBound M Salt (adv.main pk) qSign qHash) : ∃ (red : CollisionAdversary), SignatureAlg.unforgeableAdv.advantage (runtime M Salt) adv ≤ collisionFindingAdvantage psf hr red + collisionBound Salt qSign

Collision-style GPV PFDH bound in the random-oracle model.

For any adversary A making at most qSign signing queries against the GPV hash-and-sign scheme with a correct PSF and k-bit salts, and making at most qHash random-oracle queries, there exists a collision-finding reduction B such that:

Adv^{EUF-CMA}(A) ≤ Adv^{collision}(B) + qSign² / (2 · |Salt|)

This packages the distinct-preimage branch of the standard GPV argument. The complementary exact-match branch, where the forgery reproduces the simulator's programmed preimage, is to be discharged separately via a PSF preimage-min-entropy or one-wayness lemma.

The salt-collision term qSign² / (2 · |Salt|) is the birthday bound on reuse of the (salt, message) random-oracle input across signing queries. For Falcon with 40-byte salts (|Salt| = 2^320), this is 2^{-193} even for qSign = 2^64.

References: GPV08 Section 6; BDF+11 for the QROM extension.

theorem GPVHashAndSign.euf_cma_split_bound {PK SK Domain Range : Type} {p : PK → SK → Bool} [DecidableEq Range] [SampleableType Range] (psf : PreimageSampleableFunction PK SK Domain Range) (hr : GenerableRelation PK SK p) (M Salt : Type) [DecidableEq M] [DecidableEq Salt] [SampleableType Salt] [Fintype Salt] [DecidableEq Domain] (hcorrect : psf.Correct) (qSign qHash : ℕ) (adv : (GPVHashAndSign psf hr M Salt).unforgeableAdv) (hQ : ∀ (pk : PK), signHashQueryBound M Salt (adv.main pk) qSign qHash) : ∃ (collisionRed : CollisionAdversary) (exactMatchRed : ProgrammedPreimageAdversary), SignatureAlg.unforgeableAdv.advantage (runtime M Salt) adv ≤ collisionFindingAdvantage psf hr collisionRed + ↑(qSign + qHash) * programmedPreimageAdvantage psf hr exactMatchRed + collisionBound Salt qSign

Split GPV PFDH bound in the random-oracle model.

This theorem makes both branches of the GPV proof explicit:

• a collision term for the distinct-preimage branch,
• a programmed-preimage replay term for the exact-match branch, with the explicit multi-target factor qSign + qHash,
• and the birthday salt-collision term.

It is the most honest generic statement available from the current API, before any additional PSF-specific min-entropy lemma collapses the exact-match branch into the collision branch.