Merkle signatures

Merkle's tree signature ([Mer90], Section 6) authenticates 2 ^ d one-time verification keys by the root of a Merkle tree, which is the public key. The signature at leaf u is the one-time key of leaf u, its one-time signature and its authentication path. Each leaf may be used once, so the scheme is an indexed signature scheme (IndexedSignatureScheme) whose index is the leaf ([BS23], Section 14.6.1, "Shrinking the public-key").

MerkleSignature.scheme S H depth builds it from any signature scheme S, used as a one-time scheme on n-bit messages, and a keyed hash H with n-bit digests under n-bit keys:

• key generation samples a hash key k ← {0, 1}^n and 2 ^ depth n key pairs of S, and publishes k and the Merkle root of the one-time verification keys;
• signing msg at leaf u signs the digest H k msg with the one-time key of leaf u (hash-and-sign, [BS23], Section 13.2), and attaches the verification key and the authentication path;
• verification checks the opening of leaf u with merkleVerify, which fixes the path length to depth n and checks u < 2 ^ depth n, and then the one-time signature on H k msg.

The capacity is 2 ^ depth n, required to be computable in unary in polynomial time, hence polynomial in n. Security is in Complexity.Crypto.Computational.MerkleSignature.Security.

The scheme is stateful in use: the signer must sign at most once per leaf, for instance with a counter. IndexedSignatureScheme makes the leaf an explicit input, and its security game refuses a repeated leaf.

Main definitions

• Cslib.Crypto.MerkleSignature.encodeSignature, Cslib.Crypto.MerkleSignature.signatureDecoder: the signature word.
• Cslib.Crypto.MerkleSignature.publicKey, Cslib.Crypto.MerkleSignature.secretKey, Cslib.Crypto.MerkleSignature.secretKeyDecoder: the key words.
• Cslib.Crypto.MerkleSignature.keyGen, Cslib.Crypto.MerkleSignature.signWith, Cslib.Crypto.MerkleSignature.sign, Cslib.Crypto.MerkleSignature.verify: the algorithms.
• Cslib.Crypto.MerkleSignature.scheme: the indexed signature scheme.

Main results

• Cslib.Crypto.MerkleSignature.verify_sign: completeness.
• Cslib.Crypto.MerkleSignature.isPPTOn_keyGen, Cslib.Crypto.MerkleSignature.isPPTOn_sign, Cslib.Crypto.MerkleSignature.computableInPolyTime_verify: efficiency.

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.

Words

def Cslib.Crypto.MerkleSignature.encodeSignature (vk ots : List Bool) (path : List (List Bool)) : List Bool

A Merkle signature: the one-time verification key, the one-time signature and the authentication path.

def Cslib.Crypto.MerkleSignature.signatureDecoder : Turing.MultiTapeTM.Decoder (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits)))

Read the one-time verification key, the one-time signature and the authentication path of a signature word.

def Cslib.Crypto.MerkleSignature.secretKey (k : List Bool) (keys : List (List Bool × List Bool)) : List Bool

The secret key: the hash key and the one-time key pairs.

def Cslib.Crypto.MerkleSignature.secretKeyDecoder : Turing.MultiTapeTM.Decoder (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits)))

Read the hash key and the one-time key pairs of a secret key word.

def Cslib.Crypto.MerkleSignature.publicKey (H : List Bool → List Bool → List Bool) (k : List Bool) (keys : List (List Bool × List Bool)) : List Bool

The public key: the hash key and the Merkle root of the one-time verification keys.

Algorithms

noncomputable def Cslib.Crypto.MerkleSignature.keyGen (S : SignatureScheme) (H : List Bool → List Bool → List Bool) (depth : ℕ → ℕ) (n : ℕ) : ProbComp (List Bool × List Bool)

Key generation: a uniform n-bit hash key and 2 ^ depth n key pairs of S.

def Cslib.Crypto.MerkleSignature.signWith (S : SignatureScheme) (H : List Bool → List Bool → List Bool) (k : List Bool) (keys : List (List Bool × List Bool)) (u : ℕ) (msg : List Bool) : ProbComp (List Bool)

Sign msg at leaf u, given the hash key and the one-time key pairs: sign the digest H k msg with the one-time key of leaf u, and attach its verification key and authentication path.

def Cslib.Crypto.MerkleSignature.sign (S : SignatureScheme) (H : List Bool → List Bool → List Bool) (sk : List Bool) (u : ℕ) (msg : List Bool) : ProbComp (List Bool)

Sign msg at leaf u with a secret key word.

def Cslib.Crypto.MerkleSignature.verify (S : SignatureScheme) (H : List Bool → List Bool → List Bool) (depth : ℕ → ℕ) (pk : List Bool) (u : ℕ) (msg sig : List Bool) : Bool

Verify a signature on msg at leaf u under the public key pk = (k, root): the attached verification key opens leaf u of the depth-depth k.length tree with root root (merkleVerify, which checks the path length and u < 2 ^ depth k.length), and the one-time signature verifies on H k msg.

Completeness

theorem Cslib.Crypto.MerkleSignature.mem_support_keyGen {S : SignatureScheme} {H : List Bool → List Bool → List Bool} {depth : ℕ → ℕ} {n : ℕ} {keys : List Bool × List Bool} (h : keys ∈ (keyGen S H depth n).eval.support) : ∃ (k : List Bool) (otsKeys : List (List Bool × List Bool)), k.length = n ∧ otsKeys.length = 2 ^ depth n ∧ (∀ x ∈ otsKeys, x ∈ (S.keyGen n).eval.support) ∧ keys = (publicKey H k otsKeys, secretKey k otsKeys)

Every supported key generation produces an n-bit hash key and 2 ^ depth n supported one-time key pairs.

theorem Cslib.Crypto.MerkleSignature.verify_sign {S : SignatureScheme} {H : List Bool → List Bool → List Bool} {depth : ℕ → ℕ} (hlen : ∀ (k m : List Bool), (H k m).length = k.length) (n : ℕ) (keys : List Bool × List Bool) (hkeys : keys ∈ (keyGen S H depth n).eval.support) {u : ℕ} (hu : u < 2 ^ depth n) (msg sig : List Bool) (hsig : sig ∈ (sign S H keys.2 u msg).eval.support) : verify S H depth keys.1 u msg sig = true

Completeness: an honest signature at a leaf u < 2 ^ depth n verifies.

Efficiency

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

The depth is computable from the capacity.

theorem Cslib.Crypto.MerkleSignature.computableInPolyTime_publicKey {H : List Bool → List Bool → List Bool} (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) : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : List Bool × List (List Bool × List Bool)) => publicKey H p.1 p.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits))) Turing.MultiTapeTM.encBits

Computing the public key from the hash key and the one-time key pairs takes polynomial time.

theorem Cslib.Crypto.MerkleSignature.isPPTOn_keyGen {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) : Probability.IsPPTOn Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) (keyGen S H depth)

Merkle key generation is uniformly strict PPT.

theorem Cslib.Crypto.MerkleSignature.isPPTOn_sign {S : SignatureScheme} {H : List Bool → List Bool → List Bool} (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) : Probability.IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits)) Turing.MultiTapeTM.encBits fun (p : List Bool × ℕ × List Bool) => sign S H p.1 p.2.1 p.2.2

Merkle signing is uniformly strict PPT.

theorem Cslib.Crypto.MerkleSignature.computableInPolyTime_verify {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) : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : List Bool × ℕ × List Bool × List Bool) => verify S H depth p.1 p.2.1 p.2.2.1 p.2.2.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits))) Turing.MultiTapeTM.encBool

Merkle verification is computable in polynomial time.

noncomputable def Cslib.Crypto.MerkleSignature.scheme (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) : IndexedSignatureScheme

Merkle's tree signature ([Mer90], Section 6; [BS23], Section 14.6.1) as an indexed signature scheme of capacity 2 ^ depth n, from a signature scheme S used as a one-time scheme and a keyed hash H with digests of the key's length.