The Merkle–Damgård transform

Given a keyed 2n → n collision-resistant compression family h : List Bool → List Bool → List Bool, the Merkle–Damgård transform ([BS23], Section 8.4, Figure 8.5 and Theorem 8.3) constructs a collision-resistant hash family on arbitrary-length messages by iterating h k over a sequence of n-bit blocks starting from a fixed n-bit initialization vector 0^n.

We formalize the transform and its collision-extraction reduction at two levels:

1. Block-chain level (merkleDamgardChain, extractChainCollision): Iterating h k over a list of n-bit blocks produces an n-bit digest. Whenever two block lists bs₁ and bs₂ of n-bit blocks produce the same final digest under merkleDamgardChain and neither block list is a suffix of the other (¬ (bs₁ <:+ bs₂) ∧ ¬ (bs₂ <:+ bs₁)), scanning the compression inputs backward from the final step (extractChainCollision) deterministically finds a 2n-bit collision (x₁, x₂) for h k in polynomial time. In particular, this covers both cases of the classical length-strengthened Merkle–Damgård proof ([BS23], Theorem 8.3):

   • isCollision_extractChainCollision_of_getLast?_ne: the final (length-encoding) blocks of bs₁ and bs₂ differ;
   • isCollision_extractChainCollision_of_length_eq: bs₁ and bs₂ have the same number of blocks and bs₁ ≠ bs₂. Consequently, any polynomial-time suffix-free block encoding turns a CompressionFamily into a collision-resistant hash family (CompressionFamily.collisionResistantOn_merkleDamgardChain).

2. Unrestricted bit-string level (mdBlocks, merkleDamgard, extractMerkleDamgardCollision): Encoding an arbitrary bit string msg : List Bool as the initial marker block 0^n followed by one n-bit data block 1 ‖ b ‖ 0^{n-2} per bit b of msg produces a suffix-free block encoding of all bit strings for every n ≥ 2, with no upper bound on message length. Iterating h over mdBlocks k.length msg yields merkleDamgard h : List Bool → List Bool → List Bool, which is collision-resistant on all arbitrary-length bit strings (CompressionFamily.collisionResistant_merkleDamgard, CompressionFamily.hashFamily_merkleDamgard).

Main definitions

• Cslib.Crypto.padOrTake: fixed-width bit-string normalization to exact length n.
• Cslib.Crypto.merkleDamgardChain: block-level iterated compression blocks.foldl (fun acc b => h k (acc ++ b)) iv.
• Cslib.Crypto.chainTraceStep, Cslib.Crypto.chainTrace, Cslib.Crypto.extractChainCollision: polynomial-time backward scan extracting a 2n-bit compression collision from colliding block chains.
• Cslib.Crypto.mdEndBlock, Cslib.Crypto.mdDataBlock, Cslib.Crypto.mdBlocks: suffix-free n-bit block encoding of arbitrary bit strings.
• Cslib.Crypto.merkleDamgard, Cslib.Crypto.extractMerkleDamgardCollision: domain-extended keyed hash family and its deterministic collision extractor.

Main results

• Cslib.Crypto.length_merkleDamgardChain, Cslib.Crypto.length_merkleDamgard: digest length preservation.
• Cslib.Crypto.isCollision_extractChainCollision_of_not_suffix, Cslib.Crypto.isCollision_extractChainCollision_of_getLast?_ne, Cslib.Crypto.isCollision_extractChainCollision_of_length_eq: fundamental Merkle–Damgård chain collision extraction lemmas.
• Cslib.Crypto.CompressionFamily.collisionResistantOn_merkleDamgardChain: collision resistance for any polynomial-time suffix-free block encoding.
• Cslib.Crypto.mdBlocks_suffix_iff: suffix-freeness of mdBlocks n for n ≥ 2.
• Cslib.Crypto.isCollision_extractMerkleDamgardCollision: deterministic collision extraction for merkleDamgard.
• Cslib.Crypto.CompressionFamily.collisionResistant_merkleDamgard, Cslib.Crypto.CompressionFamily.hashFamily_merkleDamgard: any 2n → n collision-resistant compression family yields an unrestricted collision-resistant hash family on List Bool.

References

• D. Boneh, V. Shoup, A Graduate Course in Applied Cryptography, Section 8.4 (Figure 8.5 and Theorem 8.3).
• J. Katz, Y. Lindell, Introduction to Modern Cryptography, Section 5.2.

Fixed-width normalization

def Cslib.Crypto.padOrTake (n : ℕ) (w : List Bool) : List Bool

Normalize a bit string to exact length n by right-padding with false or truncating. On words already of length n, this is the identity.

@[simp]

theorem Cslib.Crypto.length_padOrTake (n : ℕ) (w : List Bool) : (padOrTake n w).length = n

@[simp]

theorem Cslib.Crypto.padOrTake_eq_self {n : ℕ} {w : List Bool} (hw : w.length = n) : padOrTake n w = w

theorem Cslib.Crypto.computableInPolyTime_padOrTake : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ℕ × List Bool) => padOrTake p.1 p.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits

Normalizing a word to unary length n is computable in plain polynomial time.

Block-level Merkle–Damgård chain and collision extraction

def Cslib.Crypto.merkleDamgardChain (h : List Bool → List Bool → List Bool) (k iv : List Bool) (blocks : List (List Bool)) : List Bool

Block-level Merkle–Damgård iterated compression ([BS23], Section 8.4, Figure 8.5): starting from the initial chaining value iv, fold over blocks by feeding acc ++ b to h k at each step.

@[simp]

theorem Cslib.Crypto.merkleDamgardChain_nil (h : List Bool → List Bool → List Bool) (k iv : List Bool) : merkleDamgardChain h k iv [] = iv

@[simp]

theorem Cslib.Crypto.merkleDamgardChain_cons (h : List Bool → List Bool → List Bool) (k iv b : List Bool) (blocks : List (List Bool)) : merkleDamgardChain h k iv (b :: blocks) = merkleDamgardChain h k (h k (iv ++ b)) blocks

@[simp]

theorem Cslib.Crypto.merkleDamgardChain_append (h : List Bool → List Bool → List Bool) (k iv : List Bool) (bs₁ bs₂ : List (List Bool)) : merkleDamgardChain h k iv (bs₁ ++ bs₂) = merkleDamgardChain h k (merkleDamgardChain h k iv bs₁) bs₂

theorem Cslib.Crypto.merkleDamgardChain_concat (h : List Bool → List Bool → List Bool) (k iv : List Bool) (blocks : List (List Bool)) (b : List Bool) : merkleDamgardChain h k iv (blocks ++ [b]) = h k (merkleDamgardChain h k iv blocks ++ b)

theorem Cslib.Crypto.length_merkleDamgardChain {h : List Bool → List Bool → List Bool} {k iv : List Bool} {blocks : List (List Bool)} (hlen : ∀ (x : List Bool), x.length = 2 * k.length → (h k x).length = k.length) (hiv : iv.length = k.length) (hblocks : ∀ b ∈ blocks, b.length = k.length) : (merkleDamgardChain h k iv blocks).length = k.length

If the initial vector and every block have length k.length, and h k maps 2 * k.length-bit inputs to k.length-bit outputs, then merkleDamgardChain produces a k.length-bit digest.

def Cslib.Crypto.chainTraceStep (h : List Bool → List Bool → List Bool) (k : List Bool) (state : List Bool × List (List Bool)) (b : List Bool) : List Bool × List (List Bool)

Single step of chainTrace: normalize the current chaining value and block to k.length bits, compress their concatenation under h k, and prepend the 2 * k.length-bit compression input to the reverse-chronological trace.

def Cslib.Crypto.chainTrace (h : List Bool → List Bool → List Bool) (k iv : List Bool) (blocks : List (List Bool)) : List Bool × List (List Bool)

Run the Merkle–Damgård block chain while recording, in reverse chronological order, the 2n-bit compression inputs fed to h k at each step. Each step normalizes the chaining value and block to k.length bits via padOrTake k.length, which is the identity on valid k.length-bit chains and guarantees polynomial state growth on all inputs.

@[simp]

theorem Cslib.Crypto.chainTrace_nil (h : List Bool → List Bool → List Bool) (k iv : List Bool) : chainTrace h k iv [] = (iv, [])

theorem Cslib.Crypto.computableInPolyTime_chainTrace {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 x : List Bool), x.length = 2 * k.length → (h k x).length = k.length) : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : List Bool × List Bool × List (List Bool)) => chainTrace h p.1 p.2.1 p.2.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits))) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits))

Computing chainTrace is polynomial-time for any polynomial-time compression function h.

def Cslib.Crypto.extractChainCollision (h : List Bool → List Bool → List Bool) (k iv : List Bool) (bs₁ bs₂ : List (List Bool)) : List Bool × List Bool

Extract a candidate 2n-bit collision (x₁, x₂) for h k from two block chains bs₁ and bs₂ by scanning their compression inputs backward from the final step and returning the first differing pair of inputs (or ([], []) if none differ).

theorem Cslib.Crypto.computableInPolyTime_extractChainCollision {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 x : List Bool), x.length = 2 * k.length → (h k x).length = k.length) : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : List Bool × List Bool × List (List Bool) × List (List Bool)) => extractChainCollision h p.1 p.2.1 p.2.2.1 p.2.2.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits) (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits)))) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits)

Extracting a compression collision from two block chains is computable in plain polynomial time.

theorem Cslib.Crypto.isCollision_extractChainCollision_of_not_suffix {h : List Bool → List Bool → List Bool} {k iv : List Bool} {bs₁ bs₂ : List (List Bool)} (hlen : ∀ (x : List Bool), x.length = 2 * k.length → (h k x).length = k.length) (hiv : iv.length = k.length) (hbs₁ : ∀ b ∈ bs₁, b.length = k.length) (hbs₂ : ∀ b ∈ bs₂, b.length = k.length) (hchain : merkleDamgardChain h k iv bs₁ = merkleDamgardChain h k iv bs₂) (hsuf₁ : ¬bs₁ <:+ bs₂) (hsuf₂ : ¬bs₂ <:+ bs₁) : isCollision h validCompressionInput k.length k (extractChainCollision h k iv bs₁ bs₂).1 (extractChainCollision h k iv bs₁ bs₂).2 = true

Fundamental Merkle–Damgård chain collision lemma (suffix-free form): if bs₁ and bs₂ are lists of k.length-bit blocks such that neither is a suffix of the other and merkleDamgardChain h k iv bs₁ = merkleDamgardChain h k iv bs₂, then extractChainCollision h k iv bs₁ bs₂ produces a valid 2 * k.length-bit collision for h k.

theorem Cslib.Crypto.isCollision_extractChainCollision_of_getLast?_ne {h : List Bool → List Bool → List Bool} {k iv : List Bool} {bs₁ bs₂ : List (List Bool)} (hlen : ∀ (x : List Bool), x.length = 2 * k.length → (h k x).length = k.length) (hiv : iv.length = k.length) (hbs₁ : ∀ b ∈ bs₁, b.length = k.length) (hbs₂ : ∀ b ∈ bs₂, b.length = k.length) (hne₁ : bs₁ ≠ []) (hne₂ : bs₂ ≠ []) (hlast : bs₁.getLast? ≠ bs₂.getLast?) (hchain : merkleDamgardChain h k iv bs₁ = merkleDamgardChain h k iv bs₂) : isCollision h validCompressionInput k.length k (extractChainCollision h k iv bs₁ bs₂).1 (extractChainCollision h k iv bs₁ bs₂).2 = true

Merkle–Damgård chain collision lemma (distinct final blocks, [BS23], Theorem 8.3 Case 1): if two non-empty k.length-bit block chains bs₁ and bs₂ differ in their last block (bs₁.getLast? ≠ bs₂.getLast?) and produce the same chain digest, then extractChainCollision returns a 2 * k.length-bit collision for h k.

theorem Cslib.Crypto.isCollision_extractChainCollision_of_length_eq {h : List Bool → List Bool → List Bool} {k iv : List Bool} {bs₁ bs₂ : List (List Bool)} (hlen : ∀ (x : List Bool), x.length = 2 * k.length → (h k x).length = k.length) (hiv : iv.length = k.length) (hbs₁ : ∀ b ∈ bs₁, b.length = k.length) (hbs₂ : ∀ b ∈ bs₂, b.length = k.length) (hblen : bs₁.length = bs₂.length) (hne : bs₁ ≠ bs₂) (hchain : merkleDamgardChain h k iv bs₁ = merkleDamgardChain h k iv bs₂) : isCollision h validCompressionInput k.length k (extractChainCollision h k iv bs₁ bs₂).1 (extractChainCollision h k iv bs₁ bs₂).2 = true

Merkle–Damgård chain collision lemma (equal block lengths, [BS23], Theorem 8.3 Case 2): if two distinct k.length-bit block chains bs₁ ≠ bs₂ of equal length (bs₁.length = bs₂.length) produce the same chain digest, then extractChainCollision returns a 2 * k.length-bit collision for h k.

theorem Cslib.Crypto.CompressionFamily.collisionResistantOn_merkleDamgardChain {h : List Bool → List Bool → List Bool} (hh : CompressionFamily h) (encode : ℕ → List Bool → List (List Bool)) (valid : ℕ → List Bool → Bool) (hencode : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ℕ × List Bool) => encode p.1 p.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits) (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits)) (hblocks : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (m : List Bool), valid n m = true → ∀ b ∈ encode n m, b.length = n) (hsuffix : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (m₁ m₂ : List Bool), valid n m₁ = true → valid n m₂ = true → m₁ ≠ m₂ → ¬encode n m₁ <:+ encode n m₂) : CollisionResistantOn (fun (k msg : List Bool) => merkleDamgardChain h k (List.replicate k.length false) (encode k.length msg)) valid

General suffix-free block-encoding Merkle–Damgård reduction: for any polynomial-time block encoder encode : ℕ → List Bool → List (List Bool) that maps valid messages at parameter n (for all sufficiently large n) into suffix-free lists of n-bit blocks, iterating a collision-resistant CompressionFamily over encode k.length msg yields a collision-resistant hash family on valid.

Prefix-tagged bit-block encoding and unrestricted Merkle–Damgård hash family

def Cslib.Crypto.mdEndBlock (n : ℕ) : List Bool

The initial marker block 0^n placed at the start of mdBlocks n msg.

def Cslib.Crypto.mdDataBlock (n : ℕ) (b : Bool) : List Bool

Encode a single message bit b as an n-bit block 1 ‖ b ‖ 0^{n-2} (truncated to n bits when n < 2). For n ≥ 2, the leading tag bit true distinguishes every data block from mdEndBlock n, and the second bit b distinguishes the two bit values.

def Cslib.Crypto.mdBlocks (n : ℕ) (msg : List Bool) : List (List Bool)

Encode an arbitrary bit string msg : List Bool as a non-empty list of n-bit blocks: the initial marker block mdEndBlock n followed by one mdDataBlock n per bit of msg. Because mdEndBlock n starts with false and every mdDataBlock n b starts with true, no distinct message encoding can be a suffix of another whenever n ≥ 2.

@[simp]

theorem Cslib.Crypto.length_mdEndBlock (n : ℕ) : (mdEndBlock n).length = n

@[simp]

theorem Cslib.Crypto.length_mdDataBlock (n : ℕ) (b : Bool) : (mdDataBlock n b).length = n

theorem Cslib.Crypto.mdBlocks_suffix_iff {n : ℕ} (hn : 2 ≤ n) {m₁ m₂ : List Bool} : mdBlocks n m₁ <:+ mdBlocks n m₂ ↔ m₁ = m₂

For n ≥ 2, mdBlocks n m₁ is a suffix of mdBlocks n m₂ if and only if m₁ = m₂.

theorem Cslib.Crypto.computableInPolyTime_mdBlocks : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ℕ × List Bool) => mdBlocks p.1 p.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits) (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits)

Encoding a bit string into n-bit Merkle–Damgård blocks is computable in plain polynomial time.

def Cslib.Crypto.merkleDamgard (h : List Bool → List Bool → List Bool) (k msg : List Bool) : List Bool

The Merkle–Damgård hash family (merkleDamgard): hash an arbitrary-length bit string msg : List Bool under key k : List Bool by iterating the 2n → n compression function h k over mdBlocks k.length msg from the initial vector 0^{k.length}.

theorem Cslib.Crypto.length_merkleDamgard {h : List Bool → List Bool → List Bool} {k msg : List Bool} (hlen : ∀ (x : List Bool), x.length = 2 * k.length → (h k x).length = k.length) : (merkleDamgard h k msg).length = k.length

For any compression function h mapping 2 * k.length-bit inputs to k.length-bit outputs, merkleDamgard h k msg always has length k.length.

theorem Cslib.Crypto.computableInPolyTime_merkleDamgard {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 x : List Bool), x.length = 2 * k.length → (h k x).length = k.length) : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : List Bool × List Bool) => merkleDamgard h p.1 p.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits

Evaluating merkleDamgard h is computable in plain polynomial time whenever h is computable in polynomial time and compresses 2n-bit inputs to n-bit digests.

def Cslib.Crypto.extractMerkleDamgardCollision (h : List Bool → List Bool → List Bool) (k m₁ m₂ : List Bool) : List Bool × List Bool

Deterministically extract a 2 * k.length-bit compression collision for h k from two messages m₁, m₂ : List Bool that collide under merkleDamgard h k.

theorem Cslib.Crypto.computableInPolyTime_extractMerkleDamgardCollision {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 x : List Bool), x.length = 2 * k.length → (h k x).length = k.length) : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : List Bool × List Bool × List Bool) => extractMerkleDamgardCollision h p.1 p.2.1 p.2.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits)) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits)

Extracting a 2n-bit compression collision from a merkleDamgard h collision is computable in plain polynomial time.

theorem Cslib.Crypto.isCollision_extractMerkleDamgardCollision {h : List Bool → List Bool → List Bool} {k m₁ m₂ : List Bool} (hlen : ∀ (x : List Bool), x.length = 2 * k.length → (h k x).length = k.length) (hk : 2 ≤ k.length) (hne : m₁ ≠ m₂) (hcol : merkleDamgard h k m₁ = merkleDamgard h k m₂) : isCollision h validCompressionInput k.length k (extractMerkleDamgardCollision h k m₁ m₂).1 (extractMerkleDamgardCollision h k m₁ m₂).2 = true

Deterministic Merkle–Damgård collision extraction ([BS23], Theorem 8.3): for any key k of length ≥ 2 and any two distinct messages m₁ ≠ m₂ with merkleDamgard h k m₁ = merkleDamgard h k m₂, extractMerkleDamgardCollision h k m₁ m₂ outputs a valid 2 * k.length-bit collision (x₁, x₂) for h k.

theorem Cslib.Crypto.CompressionFamily.collisionResistant_merkleDamgard {h : List Bool → List Bool → List Bool} (hh : CompressionFamily h) : CollisionResistant (merkleDamgard h)

Security of the Merkle–Damgård transform ([BS23], Theorem 8.3): if h is a 2n → n collision-resistant compression family (CompressionFamily h), then merkleDamgard h is collision-resistant on all arbitrary-length bit strings (List Bool).

theorem Cslib.Crypto.CompressionFamily.hashFamily_merkleDamgard {h : List Bool → List Bool → List Bool} (hh : CompressionFamily h) : HashFamily (merkleDamgard h)

Domain extension from compression families to unrestricted hash families: every 2n → n collision-resistant CompressionFamily h induces a full-domain collision-resistant HashFamily (merkleDamgard h) on arbitrary bit strings.