Security of Merkle signatures

A forgery against MerkleSignature.scheme S H depth either contains a collision of H k, or it is a one-time forgery against S at the leaf it names. Two reductions turn this into a bound with an explicit loss, for every forger A and every security parameter n:

Pr[A forges] ≤ 2 ^ depth n * Pr[oneTimeForger A forges against S] + Pr[collisionFinder A finds a collision of H].

• MerkleSignature.collisionFinder generates all keys itself, answers A's signing queries honestly, and extracts a collision from the forgery. If the forged verification key differs from the one at the named leaf, both open the same position of the tree, and extractMerkleCollision finds a collision in the tree. Otherwise, if the leaf already signed another message with the same digest, those two messages collide.
• MerkleSignature.oneTimeForger plants its challenge key at a uniform leaf i, generates the other keys itself, and answers the query at leaf i with its one-time signing oracle. Because the indexed game never signs twice at one leaf, it makes at most one query, and its simulation of the signing oracle is exact. A forgery at leaf i that is not a collision is a one-time forgery on a new digest. The factor 2 ^ depth n is exact: the leaf is drawn from exactly 2 ^ depth n values.

Merkle ([Mer90], Section 6) gives the construction with an informal argument. The bound is the composition, original to this library, of the plug-and-pray argument for indexed signatures from one-time signatures ([BS23], Section 14.6.1, referring to Exercise 13.2), the collision extraction behind [BS23], Theorem 8.8, for the shrunken public key, and the hash-and-sign bound of [BS23], Theorem 13.1, for the digest.

Main definitions

• Cslib.Crypto.MerkleSignature.collisionOf, Cslib.Crypto.MerkleSignature.collisionFinder: the reduction to collision finding.
• Cslib.Crypto.MerkleSignature.leafIndex, Cslib.Crypto.MerkleSignature.plantKeys, Cslib.Crypto.MerkleSignature.plantedHandler, Cslib.Crypto.MerkleSignature.oneTimeForgerAt, Cslib.Crypto.MerkleSignature.oneTimeForger: the reduction to one-time forgery.

Main results

• Cslib.Crypto.MerkleSignature.succProbability_indexedEufCmaGame_le: the explicit bound.
• Cslib.Crypto.MerkleSignature.isPPT_collisionFinder, Cslib.Crypto.MerkleSignature.isOraclePPT_oneTimeForger: the reductions are efficient.
• Cslib.Crypto.MerkleSignature.eval_leafIndex, Cslib.Crypto.MerkleSignature.isPPTOn_leafIndex: the leaf is exactly uniform and sampled efficiently.
• Cslib.Crypto.SignatureScheme.OneTimeEUFCMA.indexedEUFCMA_merkle: one-time security of S and collision resistance of H give indexed EUF-CMA security.
• Cslib.Crypto.OneWay.exists_indexedEUFCMA: a one-way function and a collision-resistant hash family give indexed EUF-CMA secure signatures of every polynomial capacity 2 ^ depth n.

References

• R. C. Merkle, A Certified Digital Signature, Section 6.
• D. Boneh, V. Shoup, A Graduate Course in Applied Cryptography, Sections 8.9, 13.2 and 14.6.1.

The reduction to collision finding

def Cslib.Crypto.MerkleSignature.collisionOf (H : List Bool → List Bool → List Bool) (k : List Bool) (keys : List (List Bool × List Bool)) (out : (ℕ × List Bool × List Bool) × List (ℕ × List Bool)) : List Bool × List Bool

The candidate collision of H k in a forgery out = ((u, msg, sig), signed) against the keys keys: a collision in the tree if the forged verification key is not the one at leaf u, and otherwise the forged message with a message signed at leaf u with the same digest.

noncomputable def Cslib.Crypto.MerkleSignature.collisionFinder (S : SignatureScheme) (H : List Bool → List Bool → List Bool) (depth : ℕ → ℕ) (hH : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : List Bool × List Bool) => H p.1 p.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits) (hlen : ∀ (k m : List Bool), (H k m).length = k.length) (hcap : Turing.MultiTapeTM.ComputableInPolyTime (fun (n : ℕ) => 2 ^ depth n) Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (adversary : IndexedForger) : CollisionFinder

The collision finder: given the hash key k, generate the one-time keys, answer the forger's signing queries honestly, and return collisionOf its forgery.

The reduction to one-time forgery

noncomputable def Cslib.Crypto.MerkleSignature.leafIndex (depth : ℕ → ℕ) (n : ℕ) : ProbComp ℕ

A uniform leaf below 2 ^ depth n, from depth n fair bits.

noncomputable def Cslib.Crypto.MerkleSignature.plantKeys (S : SignatureScheme) (depth : ℕ → ℕ) (n i : ℕ) (vk : List Bool) : ProbComp (List Bool × List (List Bool × List Bool))

Sample a hash key and the one-time keys of every leaf except leaf i, where the verification key vk is planted with an empty secret key.

def Cslib.Crypto.MerkleSignature.plantedHandler (S : SignatureScheme) (H : List Bool → List Bool → List Bool) (depth : ℕ → ℕ) (n : ℕ) (k : List Bool) (keys : List (List Bool × List Bool)) (i bound : ℕ) (request : Unit × List Bool) : StateT (List (ℕ × List Bool)) (Probability.WordOracleComp Unit) (List Bool)

The one-time forger's answer to a signing request: as the indexed signing oracle, except that leaf i is signed by an external query to the one-time signing oracle, whose reply is truncated to bound bits.

noncomputable def Cslib.Crypto.MerkleSignature.oneTimeForgerAt (S : SignatureScheme) (H : List Bool → List Bool → List Bool) (depth bound : ℕ → ℕ) (adversary : IndexedForger) (i : ℕ) : Forger

The one-time forger with its challenge planted at leaf i.

noncomputable def Cslib.Crypto.MerkleSignature.oneTimeForger (S : SignatureScheme) (H : List Bool → List Bool → List Bool) (depth bound : ℕ → ℕ) (adversary : IndexedForger) : Forger

The one-time forger: plant the challenge at a uniform leaf.

Exact simulation by the one-time forger

theorem Cslib.Crypto.MerkleSignature.eval_leafIndex (depth : ℕ → ℕ) (n : ℕ) : (leafIndex depth n).eval = PMF.map Fin.val (Probability.PMF.uniformOfFintype (Fin (2 ^ depth n)))

The leaf is exactly uniform below 2 ^ depth n, the law of ProbComp.sampleBinaryNat (depth n) (ProbComp.eval_sampleBinaryNat). leafIndex reads its bits with BitString.boundedBinaryValue, whose cap 2 ^ depth n never binds, because the reduction needs the leaf in unary (isPPTOn_leafIndex), and Probability.isPPTOn_sampleBinaryNat outputs it in binary.

The explicit bound

theorem Cslib.Crypto.MerkleSignature.succProbability_indexedEufCmaGame_le {S : SignatureScheme} {H : List Bool → List Bool → List Bool} {depth : ℕ → ℕ} (hH : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : List Bool × List Bool) => H p.1 p.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits) (hlen : ∀ (k m : List Bool), (H k m).length = k.length) (hcap : Turing.MultiTapeTM.ComputableInPolyTime (fun (n : ℕ) => 2 ^ depth n) Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) {bound : ℕ → ℕ} {n : ℕ} (hbound : ∀ x ∈ (S.keyGen n).eval.support, ∀ (msg : List Bool), msg.length = n → ∀ σ ∈ (S.sign x.2 msg).eval.support, σ.length ≤ bound n) (adversary : IndexedForger) : Game.succProbability ((scheme S H depth hH hlen hcap).indexedEufCmaGame adversary n).eval ≤ 2 ^ depth n * Game.succProbability (S.eufOneTimeGame (oneTimeForger S H depth bound adversary) n).eval + Game.succProbability (collisionGame H (fun (x : ℕ) (x_1 : List Bool) => true) (collisionFinder S H depth hH hlen hcap adversary) n).eval

Security of Merkle signatures, with an explicit loss. For every forger and every security parameter n, the forging probability against MerkleSignature.scheme S H depth is at most 2 ^ depth n times the success of oneTimeForger against S in the one-time game, plus the success of collisionFinder in the collision game of H. The bound bound n must cover the length of every one-time signature on an n-bit message under a supported key; the one-time forger truncates replies to it.

Efficiency of the reductions

theorem Cslib.Crypto.MerkleSignature.isPPT_collisionFinder {S : SignatureScheme} {H : List Bool → List Bool → List Bool} {depth : ℕ → ℕ} (hH : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : List Bool × List Bool) => H p.1 p.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits) (hlen : ∀ (k m : List Bool), (H k m).length = k.length) (hcap : Turing.MultiTapeTM.ComputableInPolyTime (fun (n : ℕ) => 2 ^ depth n) Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) {adversary : IndexedForger} (hadversary : Probability.IsOraclePPT (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits)) adversary) : Probability.IsPPT (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) (collisionFinder S H depth hH hlen hcap adversary)

The collision finder is uniformly strict PPT for every oracle-PPT forger.

theorem Cslib.Crypto.MerkleSignature.isPPTOn_leafIndex {depth : ℕ → ℕ} (hcap : Turing.MultiTapeTM.ComputableInPolyTime (fun (n : ℕ) => 2 ^ depth n) Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) : Probability.IsPPTOn Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary (leafIndex depth)

Sampling a uniform leaf is uniformly strict PPT.

theorem Cslib.Crypto.MerkleSignature.isOraclePPT_oneTimeForger {S : SignatureScheme} {H : List Bool → List Bool → List Bool} {depth : ℕ → ℕ} (hH : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : List Bool × List Bool) => H p.1 p.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits) (hlen : ∀ (k m : List Bool), (H k m).length = k.length) (hcap : Turing.MultiTapeTM.ComputableInPolyTime (fun (n : ℕ) => 2 ^ depth n) Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) {bound : ℕ → ℕ} (hboundPoly : Turing.MultiTapeTM.ComputableInPolyTime bound Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) {adversary : IndexedForger} (hadversary : Probability.IsOraclePPT (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits)) adversary) : Probability.IsOraclePPT (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) (oneTimeForger S H depth bound adversary)

The one-time forger is uniformly strict oracle PPT for every oracle-PPT indexed forger and every polynomial-time truncation bound.

Security

theorem Cslib.Crypto.SignatureScheme.OneTimeEUFCMA.indexedEUFCMA_merkle {S : SignatureScheme} (hS : S.OneTimeEUFCMA) {H : List Bool → List Bool → List Bool} (hcr : CollisionResistant H) (hH : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : List Bool × List Bool) => H p.1 p.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits) (hlen : ∀ (k m : List Bool), (H k m).length = k.length) {depth : ℕ → ℕ} (hcap : Turing.MultiTapeTM.ComputableInPolyTime (fun (n : ℕ) => 2 ^ depth n) Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) : (MerkleSignature.scheme S H depth hH hlen hcap).IndexedEUFCMA

Merkle signatures are secure ([Mer90], Section 6; [BS23], Section 14.6.1): if S is one-time EUF-CMA secure and H is collision resistant, then MerkleSignature.scheme S H depth is an indexed EUF-CMA secure signature scheme of capacity 2 ^ depth n. The reductions are oneTimeForger, with loss 2 ^ depth n, and collisionFinder, with loss 1 (succProbability_indexedEufCmaGame_le).

theorem Cslib.Crypto.OneWay.exists_indexedEUFCMA {f : List Bool → List Bool} (hf : OneWay f) {H : List Bool → List Bool → List Bool} (hH : HashFamily H) {depth : ℕ → ℕ} (hcap : Turing.MultiTapeTM.ComputableInPolyTime (fun (n : ℕ) => 2 ^ depth n) Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) : ∃ (S : IndexedSignatureScheme), (∀ (n : ℕ), S.capacity n = 2 ^ depth n) ∧ S.IndexedEUFCMA

Indexed signatures from one-way functions and collision-resistant hashing: Lamport's one-time scheme on any one-way function, under Merkle's tree with any collision-resistant hash family, gives an indexed EUF-CMA secure signature scheme of every polynomial capacity 2 ^ depth n.