1/-2 WP34 — XOR-linearised SHA-256 and the 9-step local collision3 (Chabaud–Joux 1998 linearisation technique; Gilbert–Handschuh 2003 local collision for SHA-256).45 Linearised model. Every modular addition of the step function is replaced by XOR; Σ0 and Σ16 are already GF(2)-linear (`Sigma0_xor`, `Sigma1_xor`). The two Boolean functions are replaced7 by a GF(2)-linear substitute `boolf`; we prove the local collision for two standard choices:89 * `absorb` : Ch, Maj ↦ 0. This is the difference-domain reading of Gilbert–Handschuh 200310 (SAC 2003, "Security analysis of SHA-256 and sisters", §4): their 9-step local collision is11 computed under the conditions that the Boolean functions *absorb* every incoming difference12 (a difference in exactly one input of Ch/Maj is cancelled when the other two inputs are13 equal on the active bits / when the relevant bit of the selector has the right value); the14 corrections then only have to cancel the Σ0 / Σ1 images, which are linear. In a linear model15 "Ch and Maj absorb all differences" is exactly "Ch = Maj = 0".16 * `xor3` : Ch, Maj ↦ x ^ y ^ z. This is the Chabaud–Joux 1998 (CRYPTO) linearisation used17 for SHA-0, where the IF / MAJ functions are replaced by the XOR of their inputs. The18 corrections differ (derived below) but a 9-step local collision still exists.1920 Derivation (model `absorb`; δ is the perturbation, ΔW the correction injected in W):21 step i : ΔW = δ → Δa = δ, Δe = δ22 step i+1 : a has δ ⇒ ΔT2 = Σ0(δ); e has δ ⇒ Σ1(δ) in ΔT1.23 Choose ΔW = Σ1(δ) ^ Σ0(δ) so that ΔT1 = Σ0(δ) = ΔT2 ⇒ Δa_new = 0, Δe_new = Σ0(δ)24 (the Σ1(δ) term alone — "through the e-register" — would leave Σ0(δ) in `a`).25 step i+2 : e has Σ0(δ) ⇒ ΔW = Σ1(Σ0(δ)) cancels ΔT1; registers: c = δ, f = Σ0(δ), g = δ26 step i+3 : ΔW = 0; registers: d = δ, g = Σ0(δ), h = δ27 step i+4 : h has δ ⇒ ΔW = δ (ΔT1 = 0); d has δ ⇒ Δe_new = δ. registers: e = δ, h = Σ0(δ)28 step i+5 : h = Σ0(δ), e = δ ⇒ ΔW = Σ0(δ) ^ Σ1(δ); registers: f = δ29 step i+6 : ΔW = 0; registers: g = δ30 step i+7 : ΔW = 0; registers: h = δ31 step i+8 : ΔW = δ ⇒ all registers zero.32 Correction vector (absorb): (δ, Σ1δ^Σ0δ, Σ1(Σ0δ), 0, δ, Σ0δ^Σ1δ, 0, 0, δ).33 Correction vector (xor3) : (δ, Σ1δ^Σ0δ, Σ1(Σ0δ^δ)^Σ0δ^δ, Σ1δ^Σ0δ, Σ1δ^Σ0δ, Σ0δ^Σ1δ, δ, 0, δ)34 (same bookkeeping with ΔCh = ΔMaj = XOR of the register differences).3536 Both vectors were first checked by simulation (`scripts/local_collision.py`); the theorems37 below are the universal statements, machine-checked by `bv_decide` for every state, every38 round-constant vector, every message-word vector and every δ.39-/40import Wp34.Sha256Step4142namespace Wp344344/-- Nine consecutive words (round constants `K_i..K_{i+8}` or message words `W_i..W_{i+8}`). -/45structure Words9 where46 w0 : Word47 w1 : Word48 w2 : Word49 w3 : Word50 w4 : Word51 w5 : Word52 w6 : Word53 w7 : Word54 w8 : Word55 deriving DecidableEq, Repr5657/-- Component-wise XOR (injecting a difference vector into the message words). -/58def Words9.xor (u v : Words9) : Words9 :=59 ⟨u.w0 ^^^ v.w0, u.w1 ^^^ v.w1, u.w2 ^^^ v.w2, u.w3 ^^^ v.w3, u.w4 ^^^ v.w4,60 u.w5 ^^^ v.w5, u.w6 ^^^ v.w6, u.w7 ^^^ v.w7, u.w8 ^^^ v.w8⟩6162/-- GF(2)-linearised step: every `+` of `step` becomes `^^^`, `Ch`/`Maj` become `boolf`. -/63def linStep (boolf : Word → Word → Word → Word) (s : State) (k w : Word) : State :=64 let T1 := s.h ^^^ Sigma1 s.e ^^^ boolf s.e s.f s.g ^^^ k ^^^ w65 let T2 := Sigma0 s.a ^^^ boolf s.a s.b s.c66 { a := T1 ^^^ T2, b := s.a, c := s.b, d := s.c, e := s.d ^^^ T1, f := s.e, g := s.f, h := s.g }6768/-- Linearisation "the Boolean functions absorb every difference" (Gilbert–Handschuh 2003). -/69def absorb (_x _y _z : Word) : Word := 070/-- Linearisation "Boolean function ↦ XOR of its inputs" (Chabaud–Joux 1998). -/71def xor3 (x y z : Word) : Word := x ^^^ y ^^^ z7273/-- Nine linearised steps `i, i+1, …, i+8`. -/74def lin9 (boolf : Word → Word → Word → Word) (s : State) (K W : Words9) : State :=75 linStep boolf (linStep boolf (linStep boolf (linStep boolf (linStep boolf (linStep boolf76 (linStep boolf (linStep boolf (linStep boolf s K.w0 W.w0) K.w1 W.w1) K.w2 W.w2) K.w3 W.w3)77 K.w4 W.w4) K.w5 W.w5) K.w6 W.w6) K.w7 W.w7) K.w8 W.w87879/-- Nine real (modular, non-linear) SHA-256 steps, for the negative control below. -/80def real9 (s : State) (K W : Words9) : State :=81 step (step (step (step (step (step (step (step (step s K.w0 W.w0) K.w1 W.w1) K.w2 W.w2)82 K.w3 W.w3) K.w4 W.w4) K.w5 W.w5) K.w6 W.w6) K.w7 W.w7) K.w8 W.w88384/-- Correction vector of the 9-step local collision in the `absorb` model. -/85def corrAbsorb (δ : Word) : Words9 :=86 ⟨δ, Sigma1 δ ^^^ Sigma0 δ, Sigma1 (Sigma0 δ), 0, δ, Sigma0 δ ^^^ Sigma1 δ, 0, 0, δ⟩8788/-- Correction vector of the 9-step local collision in the `xor3` model. -/89def corrXor3 (δ : Word) : Words9 :=90 ⟨δ, Sigma1 δ ^^^ Sigma0 δ, Sigma1 (Sigma0 δ ^^^ δ) ^^^ Sigma0 δ ^^^ δ,91 Sigma1 δ ^^^ Sigma0 δ, Sigma1 δ ^^^ Sigma0 δ, Sigma0 δ ^^^ Sigma1 δ, δ, 0, δ⟩9293/-! #### Proof strategy9495The 9-step statements are pure parity (XOR) identities: a direct `bv_decide` call times out96(CDCL solvers do not reason about XOR chains; see README). Instead we exploit linearity, exactly97as the Chabaud–Joux method does on paper:981. `linStep_xor_*` — one linearised step is a XOR-homomorphism in `(state, k, w)` (SAT, small);992. `lin9_xor_*` — hence nine steps are (rewriting, no SAT);1003. `corr*_xor` — the correction vector is linear in δ (SAT, small);1014. `diff_*_b0..b3` — the difference-only statement for δ restricted to each byte (SAT with 8 free102 variables);1035. `localCollision_*_diff` — the difference-only statement for every δ, by 3 + 4;1046. `localCollision_*` — the full-value statement, by 2 + 5.105-/106107/-- Component-wise XOR of states. -/108def State.xor (s t : State) : State :=109 ⟨s.a ^^^ t.a, s.b ^^^ t.b, s.c ^^^ t.c, s.d ^^^ t.d, s.e ^^^ t.e, s.f ^^^ t.f, s.g ^^^ t.g,110 s.h ^^^ t.h⟩111/-- The all-zero state. -/112def State.zero : State := ⟨0, 0, 0, 0, 0, 0, 0, 0⟩113/-- The all-zero word vector. -/114def Words9.zero : Words9 := ⟨0, 0, 0, 0, 0, 0, 0, 0, 0⟩115116theorem State.xor_zero (s : State) : s.xor State.zero = s := by117 cases s; simp only [State.xor, State.zero, State.mk.injEq]; bv_decide118theorem Words9.xor_zero (K : Words9) : K.xor Words9.zero = K := by119 cases K; simp only [Words9.xor, Words9.zero, Words9.mk.injEq]; bv_decide120121/-- One linearised step (`absorb` model) is a XOR-homomorphism in `(state, k, w)`. -/122theorem linStep_xor_absorb (s t : State) (k k' w w' : Word) :123 linStep absorb (s.xor t) (k ^^^ k') (w ^^^ w') =124 (linStep absorb s k w).xor (linStep absorb t k' w') := by125 cases s; cases t126 simp only [linStep, absorb, State.xor, State.mk.injEq, Sigma0, Sigma1, rotr]127 bv_decide128129/-- One linearised step (`xor3` model) is a XOR-homomorphism in `(state, k, w)`. -/130theorem linStep_xor_xor3 (s t : State) (k k' w w' : Word) :131 linStep xor3 (s.xor t) (k ^^^ k') (w ^^^ w') =132 (linStep xor3 s k w).xor (linStep xor3 t k' w') := by133 cases s; cases t134 simp only [linStep, xor3, State.xor, State.mk.injEq, Sigma0, Sigma1, rotr]135 bv_decide136137/-- Nine linearised steps are a XOR-homomorphism (pure rewriting with `linStep_xor_absorb`). -/138theorem lin9_xor_absorb (s t : State) (K K' W W' : Words9) :139 lin9 absorb (s.xor t) (K.xor K') (W.xor W') =140 (lin9 absorb s K W).xor (lin9 absorb t K' W') := by141 cases K; cases K'; cases W; cases W'142 simp only [lin9, Words9.xor, linStep_xor_absorb]143144theorem lin9_xor_xor3 (s t : State) (K K' W W' : Words9) :145 lin9 xor3 (s.xor t) (K.xor K') (W.xor W') =146 (lin9 xor3 s K W).xor (lin9 xor3 t K' W') := by147 cases K; cases K'; cases W; cases W'148 simp only [lin9, Words9.xor, linStep_xor_xor3]149150/-- The correction vectors are GF(2)-linear in δ (rewriting with `Sigma0_xor`/`Sigma1_xor`151then associativity–commutativity of XOR; no SAT — the `xor3` instance is a 24-literal parity152problem on which `bv_decide` times out). -/153theorem corrAbsorb_xor (x y : Word) : corrAbsorb (x ^^^ y) = (corrAbsorb x).xor (corrAbsorb y) := by154 simp only [corrAbsorb, Words9.xor, Words9.mk.injEq, Sigma0_xor, Sigma1_xor]155 repeat' apply And.intro156 all_goals (first | trivial | ac_rfl)157theorem corrXor3_xor (x y : Word) : corrXor3 (x ^^^ y) = (corrXor3 x).xor (corrXor3 y) := by158 simp only [corrXor3, Words9.xor, Words9.mk.injEq, Sigma0_xor, Sigma1_xor]159 repeat' apply And.intro160 all_goals (first | trivial | ac_rfl)161162/-- The difference map `δ ↦ lin9 f 0 0 (corr δ)` is linear in δ. -/163theorem diff_xor_absorb (x y : Word) :164 lin9 absorb State.zero Words9.zero (corrAbsorb (x ^^^ y)) =165 (lin9 absorb State.zero Words9.zero (corrAbsorb x)).xor166 (lin9 absorb State.zero Words9.zero (corrAbsorb y)) := by167 rw [corrAbsorb_xor, ← lin9_xor_absorb, State.xor_zero, Words9.xor_zero]168theorem diff_xor_xor3 (x y : Word) :169 lin9 xor3 State.zero Words9.zero (corrXor3 (x ^^^ y)) =170 (lin9 xor3 State.zero Words9.zero (corrXor3 x)).xor171 (lin9 xor3 State.zero Words9.zero (corrXor3 y)) := by172 rw [corrXor3_xor, ← lin9_xor_xor3, State.xor_zero, Words9.xor_zero]173174-- Difference-only statement for δ restricted to one byte (8 free variables each).175theorem diff_absorb_b0 (δ : Word) :176 lin9 absorb State.zero Words9.zero (corrAbsorb (δ &&& 0x000000FF#32)) = State.zero := by177 simp only [lin9, linStep, absorb, corrAbsorb, State.zero, Words9.zero, State.mk.injEq,178 Sigma0, Sigma1, rotr]179 bv_decide180theorem diff_absorb_b1 (δ : Word) :181 lin9 absorb State.zero Words9.zero (corrAbsorb (δ &&& 0x0000FF00#32)) = State.zero := by182 simp only [lin9, linStep, absorb, corrAbsorb, State.zero, Words9.zero, State.mk.injEq,183 Sigma0, Sigma1, rotr]184 bv_decide185theorem diff_absorb_b2 (δ : Word) :186 lin9 absorb State.zero Words9.zero (corrAbsorb (δ &&& 0x00FF0000#32)) = State.zero := by187 simp only [lin9, linStep, absorb, corrAbsorb, State.zero, Words9.zero, State.mk.injEq,188 Sigma0, Sigma1, rotr]189 bv_decide190theorem diff_absorb_b3 (δ : Word) :191 lin9 absorb State.zero Words9.zero (corrAbsorb (δ &&& 0xFF000000#32)) = State.zero := by192 simp only [lin9, linStep, absorb, corrAbsorb, State.zero, Words9.zero, State.mk.injEq,193 Sigma0, Sigma1, rotr]194 bv_decide195theorem diff_xor3_b0 (δ : Word) :196 lin9 xor3 State.zero Words9.zero (corrXor3 (δ &&& 0x000000FF#32)) = State.zero := by197 simp only [lin9, linStep, xor3, corrXor3, State.zero, Words9.zero, State.mk.injEq,198 Sigma0, Sigma1, rotr]199 bv_decide200theorem diff_xor3_b1 (δ : Word) :201 lin9 xor3 State.zero Words9.zero (corrXor3 (δ &&& 0x0000FF00#32)) = State.zero := by202 simp only [lin9, linStep, xor3, corrXor3, State.zero, Words9.zero, State.mk.injEq,203 Sigma0, Sigma1, rotr]204 bv_decide205theorem diff_xor3_b2 (δ : Word) :206 lin9 xor3 State.zero Words9.zero (corrXor3 (δ &&& 0x00FF0000#32)) = State.zero := by207 simp only [lin9, linStep, xor3, corrXor3, State.zero, Words9.zero, State.mk.injEq,208 Sigma0, Sigma1, rotr]209 bv_decide210theorem diff_xor3_b3 (δ : Word) :211 lin9 xor3 State.zero Words9.zero (corrXor3 (δ &&& 0xFF000000#32)) = State.zero := by212 simp only [lin9, linStep, xor3, corrXor3, State.zero, Words9.zero, State.mk.injEq,213 Sigma0, Sigma1, rotr]214 bv_decide215216theorem byte_split (δ : Word) :217 δ = (δ &&& 0x000000FF#32) ^^^ (δ &&& 0x0000FF00#32) ^^^ (δ &&& 0x00FF0000#32)218 ^^^ (δ &&& 0xFF000000#32) := by bv_decide219220/-- **9-step local collision, `absorb` model, difference-only statement**: injecting the221correction vector into the zero state with zero constants yields the zero difference, for every δ. -/222theorem localCollision_absorb_diff (δ : Word) :223 lin9 absorb State.zero Words9.zero (corrAbsorb δ) = State.zero := by224 rw [byte_split δ, diff_xor_absorb, diff_xor_absorb, diff_xor_absorb,225 diff_absorb_b0, diff_absorb_b1, diff_absorb_b2, diff_absorb_b3, State.xor_zero,226 State.xor_zero, State.xor_zero]227228/-- **9-step local collision, `xor3` (Chabaud–Joux) model, difference-only statement.** -/229theorem localCollision_xor3_diff (δ : Word) :230 lin9 xor3 State.zero Words9.zero (corrXor3 δ) = State.zero := by231 rw [byte_split δ, diff_xor_xor3, diff_xor_xor3, diff_xor_xor3,232 diff_xor3_b0, diff_xor3_b1, diff_xor3_b2, diff_xor3_b3, State.xor_zero,233 State.xor_zero, State.xor_zero]234235/-- **9-step local collision, `absorb` model, full-value statement**: for every state `s`,236every round-constant vector `K`, every message-word vector `W` and every difference `δ`, the237linearised state after nine steps is unchanged when `W` is replaced by `W ⊕ corrAbsorb δ`238(an 8·32 + 9·32 + 9·32 + 32 = 864-bit universally quantified statement). -/239theorem localCollision_absorb (s : State) (K W : Words9) (δ : Word) :240 lin9 absorb s K W = lin9 absorb s K (W.xor (corrAbsorb δ)) := by241 have h := lin9_xor_absorb s State.zero K Words9.zero W (corrAbsorb δ)242 rw [State.xor_zero, Words9.xor_zero, localCollision_absorb_diff, State.xor_zero] at h243 exact h.symm244245/-- **9-step local collision, `xor3` (Chabaud–Joux) model, full-value statement.** -/246theorem localCollision_xor3 (s : State) (K W : Words9) (δ : Word) :247 lin9 xor3 s K W = lin9 xor3 s K (W.xor (corrXor3 δ)) := by248 have h := lin9_xor_xor3 s State.zero K Words9.zero W (corrXor3 δ)249 rw [State.xor_zero, Words9.xor_zero, localCollision_xor3_diff, State.xor_zero] at h250 exact h.symm251252/-- **Negative control (machine-checked counter-example).** The linearised local collision is253NOT a collision of the real step function: with the zero state, zero constants, zero words and254δ = 1, the real 9-step outputs differ (the XOR characteristic holds on the modular function only255with some probability — Gilbert–Handschuh estimate 2⁻³⁹ for a one-bit δ with modular256corrections; `scripts/local_collision.py` observes 0/20000 with XOR corrections). -/257theorem absorb_corrections_not_real_collision :258 real9 State.zero Words9.zero Words9.zero ≠259 real9 State.zero Words9.zero (Words9.zero.xor (corrAbsorb 1)) := by260 decide261262end Wp34263