1"""3c. The 9-step local collision of SHA-256 (Chabaud-Joux style, Gilbert-Handschuh 2003 structure), C3/C4.23Linearised model4----------------5Replace every modular addition of the step by XOR and assume the Boolean functions Ch and Maj *absorb* every6difference (their output difference is 0 whenever only one input word carries a difference; this is a bit7condition, e.g. for Ch(e,f,g) with a difference in e it requires f = g on the differing bits). The difference8propagation then becomes GF(2)-linear in (state difference, message-word difference):9 da' = dh + S1(de) + dW + S0(da) de' = dd + dh + S1(de) + dW (db',dc',dd',df',dg',dh') = (da,db,dc,de,df,dg)10with S0 = Sigma0, S1 = Sigma1 (both GF(2)-linear) and "+" = XOR.1112Derivation of the corrections for a perturbation d in W_i (state difference zero before step i):13 step i : dW_i = d -> state_{i+1}: a = d, e = d14 step i+1 : da' = S1(d) + dW + S0(d), de' = S1(d) + dW. Both cannot vanish (S0(d) != 0); choose dW_{i+1} =15 S0(d) + S1(d) so that the *a*-difference dies and e receives S0(d) -> state_{i+2}: b = d, e = S0(d), f = d16 step i+2 : dW_{i+2} = S1(S0(d)) -> state_{i+3}: c = d, f = S0(d), g = d17 step i+3 : dW_{i+3} = 0 -> state_{i+4}: d = d, g = S0(d), h = d18 step i+4 : da' = dh + dW = d + dW, de' = dd + dh + dW = dW. Choose dW_{i+4} = d (kills a, e gets d)19 -> state_{i+5}: e = d, h = S0(d)20 step i+5 : dW_{i+5} = S0(d) + S1(d) -> state_{i+6}: f = d21 step i+6 : dW_{i+6} = 0 -> state_{i+7}: g = d22 step i+7 : dW_{i+7} = 0 -> state_{i+8}: h = d23 step i+8 : dW_{i+8} = d -> state_{i+9}: 0.24Pattern: (d, S0(d)+S1(d), S1(S0(d)), 0, d, S0(d)+S1(d), 0, 0, d). Register differences: a only at i+1; e at25i+1 (d), i+2 (S0(d)) and i+5 (d). This is the 9-step structure of Gilbert & Handschuh (SAC 2003) under the26"all Boolean-function differences absorbed" assumption; the table is derived here and verified below by linear27algebra over GF(2) (numpy, 256x256 and 256x32 matrices) for all 32 single-bit d (and hence, by linearity, all d).2829Experiments30-----------31(i) linear-algebra verification of the pattern (exhaustive over the 32 single-bit perturbations);32(ii) with the REAL step function: probability that the XOR pattern applied to W_i..W_{i+8} gives a state33 collision after 9 steps, over N random (state, W) samples per bit position (numpy uint32 vectorised,34 cross-checked against wp34.sha256.step on a subsample); also the step-by-step survival of the intended35 XOR difference;36(iii) SAT (CaDiCaL): find a state and words W_i..W_{i+8} conforming to the local collision with the real step37 function for d at every bit position (reproduces that conforming pairs exist under message conditions);38 verified with the reference.39"""40from __future__ import annotations41import argparse, json, random, sys, time42import numpy as np43from common import S, provenance, peak_rss_mb, MASK, bootstrap_ci44import cnf_sha256 as C45import solvers as SV4647# ------------------------------------------------------------------------------------------- GF(2) linear model48def word_matrix(fn) -> np.ndarray:49 """32x32 GF(2) matrix of a GF(2)-linear word function (column j = fn(1<<j))."""50 M = np.zeros((32, 32), dtype=np.uint8)51 for j in range(32):52 v = fn(1 << j)53 for i in range(32):54 M[i, j] = (v >> i) & 155 return M565758def vec(w: int) -> np.ndarray:59 return np.array([(w >> i) & 1 for i in range(32)], dtype=np.uint8)606162def unvec(v) -> int:63 return int(sum(int(b) << i for i, b in enumerate(v)))646566def linear_step_matrices():67 """A (256x256) and B (256x32): dstate' = A dstate + B dW over GF(2), registers ordered a,b,c,d,e,f,g,h."""68 I = np.eye(32, dtype=np.uint8); Z = np.zeros((32, 32), dtype=np.uint8)69 S0, S1 = word_matrix(S.Sigma0), word_matrix(S.Sigma1)70 rows = [71 [S0, Z, Z, Z, S1, Z, Z, I], # a' = S0(a) + S1(e) + h (+W)72 [I, Z, Z, Z, Z, Z, Z, Z], # b' = a73 [Z, I, Z, Z, Z, Z, Z, Z],74 [Z, Z, I, Z, Z, Z, Z, Z],75 [Z, Z, Z, I, S1, Z, Z, I], # e' = d + S1(e) + h (+W)76 [Z, Z, Z, Z, I, Z, Z, Z],77 [Z, Z, Z, Z, Z, I, Z, Z],78 [Z, Z, Z, Z, Z, Z, I, Z],79 ]80 A = np.block(rows) % 281 B = np.vstack([I, Z, Z, Z, I, Z, Z, Z])82 return A, B838485def pattern(d: int) -> list[int]:86 s = S.Sigma0(d) ^ S.Sigma1(d)87 return [d, s, S.Sigma1(S.Sigma0(d)), 0, d, s, 0, 0, d]888990def verify_linear(d: int):91 A, B = linear_step_matrices()92 x = np.zeros(256, dtype=np.uint8)93 traj = []94 for dw in pattern(d):95 x = (A @ x + B @ vec(dw)) % 296 traj.append([unvec(x[32 * r:32 * (r + 1)]) for r in range(8)])97 return bool(not x.any()), traj9899100# ----------------------------------------------------------------------------------- vectorised real step (numpy)101def np_rotr(x, k):102 return ((x >> np.uint32(k)) | (x << np.uint32(32 - k))).astype(np.uint32)103104105def np_step(st, k, w):106 a, b, c, d, e, f, g, h = st107 S1 = np_rotr(e, 6) ^ np_rotr(e, 11) ^ np_rotr(e, 25)108 ch = (e & f) ^ (~e & g)109 T1 = (h + S1 + ch + np.uint32(k) + w).astype(np.uint32)110 S0 = np_rotr(a, 2) ^ np_rotr(a, 13) ^ np_rotr(a, 22)111 mj = (a & b) ^ (a & c) ^ (b & c)112 T2 = (S0 + mj).astype(np.uint32)113 return [(T1 + T2).astype(np.uint32), a, b, c, (d + T1).astype(np.uint32), e, f, g]114115116def empirical(d_bit: int, n: int, rng: np.random.Generator, start: int, check_ref: int = 50):117 d = 1 << d_bit118 pat = pattern(d)119 st = [rng.integers(0, 2**32, n, dtype=np.uint32) for _ in range(8)]120 Ws = [rng.integers(0, 2**32, n, dtype=np.uint32) for _ in range(9)]121 _, lin = verify_linear(d)122 s1, s2 = list(st), list(st)123 survival = []124 alive = np.ones(n, dtype=bool)125 for j in range(9):126 k = S.K[start + j]127 s1 = np_step(s1, k, Ws[j])128 s2 = np_step(s2, k, (Ws[j] ^ np.uint32(pat[j])).astype(np.uint32))129 diff_ok = np.ones(n, dtype=bool)130 for r in range(8):131 diff_ok &= (s1[r] ^ s2[r]) == np.uint32(lin[j][r])132 alive &= diff_ok133 survival.append(int(alive.sum()))134 coll = np.ones(n, dtype=bool)135 for r in range(8):136 coll &= s1[r] == s2[r]137 n_coll = int(coll.sum())138 # cross-check the vectorised step against the reference on a subsample139 with np.errstate(over="ignore"):140 pass141 for idx in range(min(check_ref, n)):142 a = tuple(int(x[idx]) for x in st)143 b = a144 for j in range(9):145 a = S.step(a, S.K[start + j], int(Ws[j][idx]))146 b = S.step(b, S.K[start + j], int(Ws[j][idx]) ^ pat[j])147 assert a == tuple(int(x[idx]) for x in s1) and b == tuple(int(x[idx]) for x in s2), "vectorised step mismatch"148 return {"bit": d_bit, "n": n, "n_collisions": n_coll, "p_collision": n_coll / n,149 "p_upper95_rule_of_three": 3 / n if n_coll == 0 else None,150 "survival_by_step": survival, "survival_fraction_by_step": [s / n for s in survival],151 "pattern_hex": ["%08x" % w for w in pat], "pattern_weight": sum(bin(w).count("1") for w in pat)}152153154# ------------------------------------------------------------------------------------------------------- SAT (iii)155def sat_conforming(d_bit: int, start: int, timeout: float, seed: int):156 d = 1 << d_bit157 pat = pattern(d)158 cnf = C.CNF()159 st = [cnf.word() for _ in range(8)]160 W1 = [cnf.word() for _ in range(9)]161 W2 = [[(-b if (pat[j] >> i) & 1 else b) for i, b in enumerate(W1[j])] for j in range(9)]162 s1, s2 = tuple(st), tuple(st)163 for j in range(9):164 s1 = cnf.step(s1, S.K[start + j], W1[j])165 s2 = cnf.step(s2, S.K[start + j], W2[j])166 for x, y in zip(s1, s2):167 cnf.eq_w(x, y)168 t0 = time.time()169 out = SV.run_cadical(cnf.clauses, timeout, n_vars=cnf.nv, seed=seed)170 model = out.pop("model", None)171 res = {"bit": d_bit, **cnf.stats(), **out, "seed": seed}172 if out["status"] == "sat":173 state = [C.decode_word(model, w) for w in st]174 w1 = [C.decode_word(model, w) for w in W1]175 w2 = [w ^ p for w, p in zip(w1, pat)]176 a, b = tuple(state), tuple(state)177 for j in range(9):178 a = S.step(a, S.K[start + j], w1[j]); b = S.step(b, S.K[start + j], w2[j])179 res.update({"state_hex": "".join("%08x" % v for v in state), "W_hex": ["%08x" % v for v in w1],180 "W_prime_hex": ["%08x" % v for v in w2], "verified": a == b and w1 != w2,181 "final_state_hex": "".join("%08x" % v for v in a)})182 return res183184185def main():186 ap = argparse.ArgumentParser()187 ap.add_argument("--seed", type=int, default=1)188 ap.add_argument("--n", type=int, default=100_000)189 ap.add_argument("--start", type=int, default=0, help="step index i of the perturbation (uses K[i..i+8])")190 ap.add_argument("--sat-bits", default="all", help="comma list of bit positions for the SAT search, or 'all'")191 ap.add_argument("--sat-timeout", type=float, default=300)192 ap.add_argument("--out", default="results/reduced_round_sha256/local_collision.json")193 a = ap.parse_args()194 t0 = time.time()195 # (i) linear verification196 lin = {}197 for b in range(32):198 ok, traj = verify_linear(1 << b)199 lin[b] = {"cancels_after_9_steps": ok, "pattern_hex": ["%08x" % w for w in pattern(1 << b)],200 "register_difference_trajectory_hex": [["%08x" % v for v in s] for s in traj]}201 # the generic (symbolic) check: the map d -> final difference is linear, so 32 basis vectors suffice;202 # also check a few random multi-bit d203 rng = random.Random(a.seed)204 multi_ok = all(verify_linear(rng.getrandbits(32))[0] for _ in range(20))205 print("(i) linear model: all 32 single-bit perturbations cancel:", all(v["cancels_after_9_steps"] for v in lin.values()),206 "; 20 random multi-bit:", multi_ok, file=sys.stderr)207 # (ii) empirical with real step208 nrng = np.random.default_rng(a.seed)209 emp = []210 for b in range(32):211 r = empirical(b, a.n, nrng, a.start)212 emp.append(r)213 print(f"(ii) bit {b:2d}: collisions {r['n_collisions']}/{a.n} survival by step {r['survival_by_step']}", file=sys.stderr)214 # (iii) SAT215 bits = list(range(32)) if a.sat_bits == "all" else [int(x) for x in a.sat_bits.split(",")]216 sat = []217 for b in bits:218 r = sat_conforming(b, a.start, a.sat_timeout, a.seed)219 sat.append(r)220 print(f"(iii) bit {b:2d}: {r['status']} in {r['wall_s']} s, conflicts {r.get('conflicts')}, verified {r.get('verified')}", file=sys.stderr)221 meas = {"linear_model": lin, "linear_model_random_multibit_ok": multi_ok, "empirical": emp, "sat": sat,222 "pattern_formula": "(d, S0(d)^S1(d), S1(S0(d)), 0, d, S0(d)^S1(d), 0, 0, d)"}223 stats = {"wall_s": round(time.time() - t0, 3), "peak_rss_mb": peak_rss_mb(),224 "step_evaluations_real": 2 * 9 * a.n * 32}225 provenance.record("sha256_local_collision_9step", {"n_per_bit": a.n, "start_step": a.start, "sat_bits": bits,226 "sat_timeout_s": a.sat_timeout, "model": "GH03 structure, absorbing Boolean functions"},227 meas, seed=a.seed, extra={"op_stats": stats}, out=a.out, started=t0)228 print("wrote", a.out, stats)229230231if __name__ == "__main__":232 main()233