Signatures from one-way functions: Merkle trees to Rompel

Posted by coordinator-claude-c4b0c164-20261023 at Samuel's direction (2026-10-25). It leads to the ROADMAP landmark Rompel's signature theorem.

Current state on `main`

OneWayToSignature.lean proves that one-way functions are equivalent to one-time signatures (Lamport), and that EUF-CMA signatures imply one-way functions.

Milestones

M0, design: exact statements and locators. Candidates are Merkle (CRYPTO 1989); Naor–Yung (STOC 1989); Rompel (STOC 1990); and Goldreich, Foundations of Cryptography Vol. 2, Chapter 6, pinned in M0.
M1, many-time signatures from one-time signatures and collision-resistant hashing: authentication trees for a polynomial number of messages, as a stateful scheme first. The security reduction has an explicit loss.
M2, stateless signatures: derive the tree nodes with the existing GGM PRF, the usual Goldreich construction.
M3, universal one-way hash functions: Naor–Yung from one-way permutations, then the hash-and-sign extension to arbitrary polynomial-length messages.
M4 (long-haul), Rompel: UOWHFs from any one-way function, which completes OWF ⇔ EUF-CMA signatures.

Rules

The #897 shared rules and #733 apply. Reuse the SignatureScheme, OneWay, GGM and collision-resistance APIs.

M0 design and claim. worker-claude-sigs-c4b0c164 (Claude), delegated by coordinator-claude-c4b0c164-20261023. Status: active on M0 and M1. Branch feat/merkle-signatures-1001, worktree /home/samuel/Code/complexitylib-wt/1001-1.

Summary

M1 is Merkle's tree signature: one-time keys at the leaves of a hash tree whose root is the public key, each leaf used once. The leaf counter is the signer's state. I model that state explicitly in two layers.

Indexed signatures (Boneh–Shoup's q-indexed signatures). Signing takes the leaf index as an explicit input, and the security game refuses to sign twice under one index. The syntax is stateless; the security notion is new and labelled as such.
Counter-stateful use (Boneh–Shoup's nonce-based Merkle signatures with a counter as the nonce). Here the oracle's state is the counter, and the signer, not the adversary, chooses the index. This gets its own clearly labelled game, CounterEUFCMA, derived from (1).

The stateless SignatureScheme.EUFCMA on main cannot express either layer, so it stays as it is. The M2 tree construction (Boneh–Shoup Theorem 14.6) consumes any secure indexed scheme as a black box and yields a stateless scheme for the existing EUFCMA. This is why the indexed notion is the right interface.

Sources I checked

Every locator below comes from the text itself.

Boneh–Shoup [BonehShoup2023], v0.6 (Jan 2023), the version in references.bib:
- §8.9: Merkle tree hash, Fig. 8.12 and (8.16) on p. 320–321; Definition 8.3 and Attack Game 8.2 on p. 323–324; Theorem 8.8 (Merkle trees are secure authenticated data structures under collision resistance) on p. 324.
- §13.2: hash-and-sign (13.1) and Theorem 13.1 (SIGadv[A,S'] ≤ SIGadv[B_S,S] + CRadv[B_H,H]) on p. 532–533. Also the TCR variant (13.2) and Theorem 13.2, relevant to M3.
- §14.6.1, p. 597: Definition 14.6 (q-indexed signatures); construction (14.4), q one-time key pairs with (u, m) signed by key u; "Shrinking the public-key" with a Merkle tree; security by plug-and-pray (Exercise 13.2).
- §14.6.2–14.6.3, p. 598–601: the many-time tree construction, Fig. 14.7, and Theorem 14.6: SIGadv ≤ PRFadv[B_F,F] + Qd·iSIGadv[B,S_q] + Q²/(2q^d).
- §14.6.4, p. 602–603: nonce-based Merkle signatures, where the nonce is the leaf number, possibly a counter.
Merkle, A Certified Digital Signature, CRYPTO '89, LNCS 435, pp. 218–238 (pages from Crossref, doi 10.1007/0-387-34805-0_21). I read the author's posted 1979 revised manuscript, which the posting says is the text published at CRYPTO '89 p. 218. Its §6, "Tree Authentication" (manuscript pp. 20–25), defines H(i,i,Y) = F(Y_i) and H(i,j,Y) = F(⟨H(i,(i+j−1)/2,Y), H((i+j+1)/2,j,Y)⟩), the authentication path, and tree signatures. Locators inside the LNCS typesetting: to be confirmed.
Goldreich, Foundations of Cryptography Vol. 2 (2004). I could only check the table of contents (Cambridge front matter): §6.4.1 One-Time Signature Schemes (p. 538), §6.4.2 From One-Time Signature Schemes to General Ones (p. 543), §6.4.3 Universal One-Way Hash Functions and Using Them (p. 560), §6.2.2–6.2.3 (pp. 508, 516). Construction and theorem numbers: to be confirmed.
Naor–Yung, STOC '89, pp. 33–43 (doi 10.1145/73007.73011), and Rompel, STOC '90, pp. 387–394. Bibliographic data from Crossref only. Every theorem locator: to be confirmed.

Supplier PR S: Merkle trees, shared with #999

New module Complexity/Crypto/Computational/MerkleTree.lean. Kilian's commitments in #999 need the same API, so it goes in its own PR. The hash is a keyed H : List Bool → List Bool → List Bool, reusing isCollision and CollisionResistant from CollisionResistant.lean.

Following Boneh–Shoup §8.9 and Merkle's H(i,j,Y), leaves are hashed, and an internal node hashes the pair encPair encBits encBits (left, right). That pairing is injective, so siblings need no length checks. The tree has depth d; missing leaves read as [].

def merkleRoot (H : List Bool → List Bool → List Bool) (k : List Bool) (d : ℕ)
    (leaves : List (List Bool)) : List Bool
def merklePath (H) (k) (d : ℕ) (leaves : List (List Bool)) (i : ℕ) : List (List Bool)
def merkleRootOfPath (H) (k) (leaf : List Bool) (i : ℕ) (path : List (List Bool)) : List Bool
def extractMerkleCollision (H) (k) (leaf₁ leaf₂ : List Bool) (i : ℕ)
    (path₁ path₂ : List (List Bool)) : List Bool × List Bool

theorem length_merklePath : (merklePath H k d leaves i).length = d
theorem merkleRootOfPath_merklePath (hi : i < 2 ^ d) :
    merkleRootOfPath H k (leaves.getD i []) i (merklePath H k d leaves i) =
      merkleRoot H k d leaves
/-- Two openings of one position to different leaves, with equal-length paths and the
same recomputed root, yield a collision (the core of Boneh–Shoup Theorem 8.8). -/
theorem isCollision_extractMerkleCollision (hlen : path₁.length = path₂.length)
    (hne : leaf₁ ≠ leaf₂)
    (hroot : merkleRootOfPath H k leaf₁ i path₁ = merkleRootOfPath H k leaf₂ i path₂) :
    isCollision H (fun _ _ => true) n k (extractMerkleCollision H k leaf₁ leaf₂ i path₁ path₂).1
      (extractMerkleCollision H k leaf₁ leaf₂ i path₁ path₂).2 = true

The PR also adds plain ComputableInPolyTime certificates for all four functions, assuming H is polynomial-time with (H k x).length = k.length.

M1: indexed and counter-stateful Merkle signatures

New module Complexity/Crypto/Computational/IndexedSignature.lean, following Boneh–Shoup Definition 14.6. It differs from the source in three labelled ways:

Randomized signing. Signing may be randomized. Boneh–Shoup require deterministic signing only because the M2 tree re-signs internal nodes; M2 will either assume determinism (Lamport's signer is deterministic) or derive the signing coins from the PRF, as their remark suggests.
Messages. Messages are arbitrary bit strings. M2 signs child public keys with the indexed scheme, so it needs that.
Refusal instead of restriction. Boneh–Shoup forbid the adversary to reuse an index. Here the oracle refuses a repeated or out-of-range index instead: it returns [] and records nothing. Every oracle adversary is then admissible.

abbrev IndexedForger := ℕ → List Bool → WordOracleComp Unit (ℕ × List Bool × List Bool)

structure IndexedSignatureScheme where
  capacity : ℕ → ℕ                                           -- q(n); indices u < capacity n
  keyGen : ℕ → ProbComp (List Bool × List Bool)
  sign : List Bool → ℕ → List Bool → ProbComp (List Bool)     -- sk, u, msg
  verify : List Bool → ℕ → List Bool → List Bool → Bool       -- pk, u, msg, sig
  capacity_polyTime : ComputableInPolyTime capacity encUnary encUnary
  keyGen_ppt : IsPPTOn encUnary (encPair encBits encBits) keyGen
  sign_ppt : IsPPTOn (encPair encBits (encPair encUnary encBits)) encBits
    (fun p => sign p.1 p.2.1 p.2.2)
  verify_polyTime : ComputableInPolyTime
    (fun p : List Bool × ℕ × List Bool × List Bool => verify p.1 p.2.1 p.2.2.1 p.2.2.2)
    (encPair encBits (encPair encUnary (encPair encBits encBits))) encBool
  verify_sign : ∀ n keys, keys ∈ (ProbComp.eval (keyGen n)).support → ∀ u < capacity n,
    ∀ msg sig, sig ∈ (ProbComp.eval (sign keys.2 u msg)).support → verify keys.1 u msg sig = true

-- request word = encPair encUnary encBits (u, msg); signs iff u < capacity n and u is unused
def IndexedSignatureScheme.indexedSigningOracle (S) (n : ℕ) (sk : List Bool)
    (request : Unit × List Bool) : StateT (List (ℕ × List Bool)) ProbComp (List Bool)
-- win: u* < capacity n, (u*, msg*) never signed, verify pk u* msg* sig*
def IndexedSignatureScheme.indexedEufCmaGame (S) (adversary : IndexedForger) (n : ℕ) : ProbComp Bool
def IndexedSignatureScheme.IndexedEUFCMA (S) : Prop :=
  Game.Indistinguishable (fun A n => ProbComp.eval (S.indexedEufCmaGame A n))
    (fun _ _ => PMF.pure false) (IsOraclePPT (encPair encUnary (encPair encBits encBits)))

The stateful layer follows Boneh–Shoup §14.6.4 with a counter as the nonce. The oracle's state is (j, signed). While j < capacity n it signs the next message with index j, returns encPair encUnary encBits (j, σ) and moves to (j + 1, msg :: signed). After that it refuses, returning [] and recording nothing. A forgery wins on any message never signed, of any length. That is stronger than EUFCMA's n-bit forgeries; the docstrings say so.

def IndexedSignatureScheme.counterSigningOracle (S) (n : ℕ) (sk : List Bool)
    (request : Unit × List Bool) : StateT (ℕ × List (List Bool)) ProbComp (List Bool)
def IndexedSignatureScheme.counterVerify (S) (pk msg sig : List Bool) : Bool :=
  S.verify pk (unframe sig).length msg (dropFrame sig)
def IndexedSignatureScheme.counterEufCmaGame (S) (adversary : Forger) (n : ℕ) : ProbComp Bool
def IndexedSignatureScheme.CounterEUFCMA (S) : Prop   -- against IsOraclePPT (encPair encBits encBits)
theorem IndexedSignatureScheme.IndexedEUFCMA.counterEUFCMA (h : S.IndexedEUFCMA) : S.CounterEUFCMA

New module Complexity/Crypto/Computational/MerkleSignature.lean builds the scheme from any SignatureScheme (used as one-time) and a keyed hash. capacity n = 2 ^ depth n, and one hypothesis hcap gives 2 ^ depth n in unary in polynomial time, so the capacity is polynomial. depth itself is then Nat.log 2 of it.

Key generation. Sample k ← {0,1}^n and 2 ^ depth n one-time key pairs. The public key is (k, merkleRoot H k (depth n) vks).
Signing. sign sk u m returns (vk_u, S.sign sk_u (H k m), merklePath … u). This is hash-and-sign (Boneh–Shoup (13.1)) at leaf u of construction (14.4), with the shrunken public key.
Verification. Recompute depth from k.length, then check the path length, u < 2 ^ depth, the root, and S.verify vk (H k m) σ.

def merkleIndexed (S : SignatureScheme) (H : List Bool → List Bool → List Bool) (depth : ℕ → ℕ)
    (hH : ComputableInPolyTime (fun p : List Bool × List Bool => H p.1 p.2)
      (encPair encBits encBits) encBits)
    (hlen : ∀ k m, (H k m).length = k.length)
    (hcap : ComputableInPolyTime (fun n => 2 ^ depth n) encUnary encUnary) : IndexedSignatureScheme

def merkleOneTimeForger … (adversary : IndexedForger) : Forger            -- plug-and-pray at i* ← sampleBinaryNat (depth n)
def merkleCollisionFinder … (adversary : IndexedForger) : CollisionFinder -- tree or message collision
theorem isOraclePPT_merkleOneTimeForger (hA : IsOraclePPT (encPair encUnary (encPair encBits encBits)) A) :
    IsOraclePPT (encPair encBits encBits) (merkleOneTimeForger … A)
theorem isPPT_merkleCollisionFinder (hA : …) : IsPPT (encPair encBits encBits) (merkleCollisionFinder … A)

/-- Explicit loss, for every forger and every n. -/
theorem succProbability_indexedEufCmaGame_merkleIndexed_le (A : IndexedForger) (n : ℕ) :
    Game.succProbability (ProbComp.eval ((merkleIndexed S H depth hH hlen hcap).indexedEufCmaGame A n)) ≤
      2 ^ depth n * Game.succProbability (ProbComp.eval (S.eufOneTimeGame (merkleOneTimeForger … A) n)) +
      Game.succProbability (ProbComp.eval (collisionGame H (fun _ _ => true) (merkleCollisionFinder … A) n))

theorem SignatureScheme.OneTimeEUFCMA.indexedEUFCMA_merkleIndexed (hS : S.OneTimeEUFCMA)
    (hcr : CollisionResistant H) : (merkleIndexed S H depth hH hlen hcap).IndexedEUFCMA
theorem exists_indexedEUFCMA_of_oneWay_of_hashFamily (hf : OneWay f) (hH : HashFamily H)
    (hcap : ComputableInPolyTime (fun n => 2 ^ depth n) encUnary encUnary) :
    ∃ S : IndexedSignatureScheme, (∀ n, S.capacity n = 2 ^ depth n) ∧ S.IndexedEUFCMA ∧ S.CounterEUFCMA

Proof plan for the loss. Let u* be the forged index and vk' the forged leaf key.

Collision case. If vk' ≠ vk_{u*}, the forged and honest paths reach one root, so extractMerkleCollision gives a collision. If vk' = vk_{u*} but H k m* = H k m_{u*} for the message already signed at u*, that is a collision too. merkleCollisionFinder runs the real game itself, so this case costs exactly the collision term.
One-time case. Otherwise the forgery is a one-time forgery at leaf u* on a new digest. The challenge key is planted at a uniform leaf i*. ProbComp.eval_replicate_splice (already public) makes the key list the same law with the challenge at i*. The forwarded query reaches the one-time oracle at most once, because indices never repeat. The simulation is perfect for each fixed i*, and averaging over i* gives the factor 2 ^ depth n exactly: index sampling is exact, unlike Lamport's dyadic padding.
Reply bound. Replies forwarded by the one-time forger are truncated to sign_ppt's length bound, as in limitToOneQuery.

The combined bound is my composition of the sourced pieces: plug-and-pray from §14.6.1 (Exercise 13.2), Theorem 8.8 for the shrunken key, and Theorem 13.1 for hashing. Docstrings will say so.

Reuse. I build on SignatureScheme and OneTimeEUFCMA (the one-time game unchanged), Forger, CollisionFinder, collisionGame, CollisionResistant, HashFamily, Game.Indistinguishable, IsOraclePPT with run_interpret_preprocess(_open), OracleComp.replicate with eval_replicate_splice, sampleBinaryNat, BitString.sampleList, and the unframe/dropFrame decoders. lamportScheme with OneWay.exists_oneTimeSignature gives the one-time scheme.

Plain-first. No tidy predicate appears in any statement. Proofs use the tidy certificate calculus internally, like the rest of Crypto today, and will move with #862.

Tests. Concrete runs:

a Merkle root and path on a small list with a concrete H, checked by decide;
extraction on a concrete forged opening under a deliberately weak H;
a signing and verification run of merkleIndexed (lamportScheme id …) with fixed coins;
nonvacuity instances of hcap, with constant depth and depth n = Nat.clog 2 (n + 1).

Size. If the M1 PR exceeds about 1.5k lines, the counter-stateful layer moves to a follow-up PR (M1b).

Later milestones (sketch, to be designed when reached)

M2. Boneh–Shoup §14.6.3, Theorem 14.6, black-box in an IndexedSignatureScheme with IndexedEUFCMA. Tree nodes get key-generation coins from a PRF on node identifiers, via the existing seeded-evaluator interface (IsPPTOn.exists_total_seeded_evaluator). The PRF is GGM (PseudorandomGenerator.exists_pseudorandomFunction). Leaves are uniform. The output is a stateless SignatureScheme with EUFCMA, and the loss is PRFadv + Q·d·iSIGadv + Q²/(2q^d). Signing must be deterministic, so M2 will either assume it or derive the signing coins from the PRF.
M3. UOWHFs (target collision resistance): Naor–Yung from one-way permutations (locators to be confirmed), then TCR hash-and-sign (Boneh–Shoup (13.2), Theorem 13.2, one-time case) and the plain list construction (14.4) of an indexed scheme. The result is an indexed scheme from one-way permutations, which feeds M2 unchanged. One known issue to resolve then: SignatureScheme fixes n-bit messages, and TCR hash-and-sign signs (r, H(r, m)), about 2n bits.
M4. Rompel: UOWHFs from any one-way function, which closes (∃ f, OneWay f) ↔ ∃ S : SignatureScheme, S.EUFCMA together with the necessity half already on main.

For Samuel

Stateful modelling. Is two-layer modelling of statefulness acceptable: indexed (Definition 14.6) plus a counter-state wrapper with its own CounterEUFCMA? The alternative is a general StatefulSignatureScheme with an arbitrary state word. That would need a state-growth bound for the game to be PPT, and a sequence-level completeness statement. M2 does not need it.
Headline. No catalogue or abstract entry for M1. The natural headline is M4, or M2 ((∃ OWF) ∧ (∃ CRHF) → ∃ EUF-CMA scheme).

worker-claude-sigs-c4b0c164: supplier PR #1023 (Merkle trees, branch feat/merkle-tree-1001) is awaiting review. M1 is active locally on feat/merkle-signatures-1001, stacked on #1023, in worktree /home/samuel/Code/complexitylib-wt/1001-2.

Coordinator notes (coordinator-claude-c4b0c164-20261023):

Locator checked against the Boneh–Shoup v0.6 text: Definition 14.6 is "q-indexed signature system", printed p. 597, followed by the derived q-indexed signature from one-time signatures. Modelling M1's statefulness this way follows Boneh–Shoup's own route to Merkle signatures; the coordinator accepts it unless Samuel prefers otherwise.
Shared Merkle trees: feat(Crypto): Merkle trees with authentication paths and collision extraction #1023's Merkle trees will also serve Kilian's succinct arguments: PCP + collision-resistant hashing ⇒ succinct arguments for NP #999 (Kilian's vector commitments). The Kilian's succinct arguments: PCP + collision-resistant hashing ⇒ succinct arguments for NP #999 worker has been asked to build on feat(Crypto): Merkle trees with authentication paths and collision extraction #1023 instead of a second tree.

doc(Crypto): document verifier obligations of Merkle openings; reuse …

worker-claude-sigs-c4b0c164: M1 is awaiting review in #1037 (stacked on #1024 → #1023). It contains indexed signatures, Merkle signatures and the explicit bound Pr[forge] ≤ 2^depth n · Pr[one-time forgery] + Pr[collision], with both reductions certified. It also includes the OWF + HashFamily corollary.

Still open on this track:

Counter layer. The counter-stateful CounterEUFCMA from the design is not in feat(Crypto): indexed signatures and Merkle signatures from one-time signatures #1037.
M2 to M4. Not started. Per the coordinator's scope change, I am stopping after M1, and I will answer review findings when resumed.

refactor(Crypto): use Decoder combinators for Merkle signature words (#…

doc(roadmap): add crypto frontier tracks and the OpenAI math results …

doc(roadmap): correct the openai/math license note and two crypto wor…

feat(Crypto): indexed signatures and Merkle signatures from one-time …

refactor(Crypto): use Decoder combinators for Merkle signature words (#…

feat(Crypto): Merkle trees with authentication paths and collision ex…

feat(Crypto): indexed signatures and Merkle signatures from one-time …

refactor(Crypto): use Decoder combinators for Merkle signature words (#…

feat(Crypto): indexed signatures and Merkle signatures from one-time …

Navigation Menu

Repository navigation

Signatures from one-way functions: Merkle trees to Rompel #1001

Current state on `main`

Milestones

Rules

Summary

Sources I checked

Supplier PR S: Merkle trees, shared with #999

M1: indexed and counter-stateful Merkle signatures

Later milestones (sketch, to be designed when reached)

For Samuel

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Signatures from one-way functions: Merkle trees to Rompel #1001

Description

Current state on main

Milestones

Rules

Activity

SamuelSchlesinger commented on Oct 25, 2026

Summary

Sources I checked

Supplier PR S: Merkle trees, shared with #999

M1: indexed and counter-stateful Merkle signatures

Later milestones (sketch, to be designed when reached)

For Samuel

SamuelSchlesinger commented on Oct 25, 2026

SamuelSchlesinger commented on Oct 25, 2026

SamuelSchlesinger commented on Oct 25, 2026

Metadata

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Issue actions

Current state on `main`