"""3c. The 9-step local collision of SHA-256 (Chabaud-Joux style, Gilbert-Handschuh 2003 structure), C3/C4. Linearised model ---------------- Replace every modular addition of the step by XOR and assume the Boolean functions Ch and Maj *absorb* every difference (their output difference is 0 whenever only one input word carries a difference; this is a bit condition, e.g. for Ch(e,f,g) with a difference in e it requires f = g on the differing bits). The difference propagation then becomes GF(2)-linear in (state difference, message-word difference): 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) with S0 = Sigma0, S1 = Sigma1 (both GF(2)-linear) and "+" = XOR. Derivation of the corrections for a perturbation d in W_i (state difference zero before step i): step i : dW_i = d -> state_{i+1}: a = d, e = d step i+1 : da' = S1(d) + dW + S0(d), de' = S1(d) + dW. Both cannot vanish (S0(d) != 0); choose dW_{i+1} = S0(d) + S1(d) so that the *a*-difference dies and e receives S0(d) -> state_{i+2}: b = d, e = S0(d), f = d step i+2 : dW_{i+2} = S1(S0(d)) -> state_{i+3}: c = d, f = S0(d), g = d step i+3 : dW_{i+3} = 0 -> state_{i+4}: d = d, g = S0(d), h = d step i+4 : da' = dh + dW = d + dW, de' = dd + dh + dW = dW. Choose dW_{i+4} = d (kills a, e gets d) -> state_{i+5}: e = d, h = S0(d) step i+5 : dW_{i+5} = S0(d) + S1(d) -> state_{i+6}: f = d step i+6 : dW_{i+6} = 0 -> state_{i+7}: g = d step i+7 : dW_{i+7} = 0 -> state_{i+8}: h = d step i+8 : dW_{i+8} = d -> state_{i+9}: 0. Pattern: (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 at i+1 (d), i+2 (S0(d)) and i+5 (d). This is the 9-step structure of Gilbert & Handschuh (SAC 2003) under the "all Boolean-function differences absorbed" assumption; the table is derived here and verified below by linear algebra over GF(2) (numpy, 256x256 and 256x32 matrices) for all 32 single-bit d (and hence, by linearity, all d). Experiments ----------- (i) linear-algebra verification of the pattern (exhaustive over the 32 single-bit perturbations); (ii) with the REAL step function: probability that the XOR pattern applied to W_i..W_{i+8} gives a state collision after 9 steps, over N random (state, W) samples per bit position (numpy uint32 vectorised, cross-checked against wp34.sha256.step on a subsample); also the step-by-step survival of the intended XOR difference; (iii) SAT (CaDiCaL): find a state and words W_i..W_{i+8} conforming to the local collision with the real step function for d at every bit position (reproduces that conforming pairs exist under message conditions); verified with the reference. """ from __future__ import annotations import argparse, json, random, sys, time import numpy as np from common import S, provenance, peak_rss_mb, MASK, bootstrap_ci import cnf_sha256 as C import solvers as SV # ------------------------------------------------------------------------------------------- GF(2) linear model def word_matrix(fn) -> np.ndarray: """32x32 GF(2) matrix of a GF(2)-linear word function (column j = fn(1<> i) & 1 return M def vec(w: int) -> np.ndarray: return np.array([(w >> i) & 1 for i in range(32)], dtype=np.uint8) def unvec(v) -> int: return int(sum(int(b) << i for i, b in enumerate(v))) def linear_step_matrices(): """A (256x256) and B (256x32): dstate' = A dstate + B dW over GF(2), registers ordered a,b,c,d,e,f,g,h.""" I = np.eye(32, dtype=np.uint8); Z = np.zeros((32, 32), dtype=np.uint8) S0, S1 = word_matrix(S.Sigma0), word_matrix(S.Sigma1) rows = [ [S0, Z, Z, Z, S1, Z, Z, I], # a' = S0(a) + S1(e) + h (+W) [I, Z, Z, Z, Z, Z, Z, Z], # b' = a [Z, I, Z, Z, Z, Z, Z, Z], [Z, Z, I, Z, Z, Z, Z, Z], [Z, Z, Z, I, S1, Z, Z, I], # e' = d + S1(e) + h (+W) [Z, Z, Z, Z, I, Z, Z, Z], [Z, Z, Z, Z, Z, I, Z, Z], [Z, Z, Z, Z, Z, Z, I, Z], ] A = np.block(rows) % 2 B = np.vstack([I, Z, Z, Z, I, Z, Z, Z]) return A, B def pattern(d: int) -> list[int]: s = S.Sigma0(d) ^ S.Sigma1(d) return [d, s, S.Sigma1(S.Sigma0(d)), 0, d, s, 0, 0, d] def verify_linear(d: int): A, B = linear_step_matrices() x = np.zeros(256, dtype=np.uint8) traj = [] for dw in pattern(d): x = (A @ x + B @ vec(dw)) % 2 traj.append([unvec(x[32 * r:32 * (r + 1)]) for r in range(8)]) return bool(not x.any()), traj # ----------------------------------------------------------------------------------- vectorised real step (numpy) def np_rotr(x, k): return ((x >> np.uint32(k)) | (x << np.uint32(32 - k))).astype(np.uint32) def np_step(st, k, w): a, b, c, d, e, f, g, h = st S1 = np_rotr(e, 6) ^ np_rotr(e, 11) ^ np_rotr(e, 25) ch = (e & f) ^ (~e & g) T1 = (h + S1 + ch + np.uint32(k) + w).astype(np.uint32) S0 = np_rotr(a, 2) ^ np_rotr(a, 13) ^ np_rotr(a, 22) mj = (a & b) ^ (a & c) ^ (b & c) T2 = (S0 + mj).astype(np.uint32) return [(T1 + T2).astype(np.uint32), a, b, c, (d + T1).astype(np.uint32), e, f, g] def empirical(d_bit: int, n: int, rng: np.random.Generator, start: int, check_ref: int = 50): d = 1 << d_bit pat = pattern(d) st = [rng.integers(0, 2**32, n, dtype=np.uint32) for _ in range(8)] Ws = [rng.integers(0, 2**32, n, dtype=np.uint32) for _ in range(9)] _, lin = verify_linear(d) s1, s2 = list(st), list(st) survival = [] alive = np.ones(n, dtype=bool) for j in range(9): k = S.K[start + j] s1 = np_step(s1, k, Ws[j]) s2 = np_step(s2, k, (Ws[j] ^ np.uint32(pat[j])).astype(np.uint32)) diff_ok = np.ones(n, dtype=bool) for r in range(8): diff_ok &= (s1[r] ^ s2[r]) == np.uint32(lin[j][r]) alive &= diff_ok survival.append(int(alive.sum())) coll = np.ones(n, dtype=bool) for r in range(8): coll &= s1[r] == s2[r] n_coll = int(coll.sum()) # cross-check the vectorised step against the reference on a subsample with np.errstate(over="ignore"): pass for idx in range(min(check_ref, n)): a = tuple(int(x[idx]) for x in st) b = a for j in range(9): a = S.step(a, S.K[start + j], int(Ws[j][idx])) b = S.step(b, S.K[start + j], int(Ws[j][idx]) ^ pat[j]) assert a == tuple(int(x[idx]) for x in s1) and b == tuple(int(x[idx]) for x in s2), "vectorised step mismatch" return {"bit": d_bit, "n": n, "n_collisions": n_coll, "p_collision": n_coll / n, "p_upper95_rule_of_three": 3 / n if n_coll == 0 else None, "survival_by_step": survival, "survival_fraction_by_step": [s / n for s in survival], "pattern_hex": ["%08x" % w for w in pat], "pattern_weight": sum(bin(w).count("1") for w in pat)} # ------------------------------------------------------------------------------------------------------- SAT (iii) def sat_conforming(d_bit: int, start: int, timeout: float, seed: int): d = 1 << d_bit pat = pattern(d) cnf = C.CNF() st = [cnf.word() for _ in range(8)] W1 = [cnf.word() for _ in range(9)] W2 = [[(-b if (pat[j] >> i) & 1 else b) for i, b in enumerate(W1[j])] for j in range(9)] s1, s2 = tuple(st), tuple(st) for j in range(9): s1 = cnf.step(s1, S.K[start + j], W1[j]) s2 = cnf.step(s2, S.K[start + j], W2[j]) for x, y in zip(s1, s2): cnf.eq_w(x, y) t0 = time.time() out = SV.run_cadical(cnf.clauses, timeout, n_vars=cnf.nv, seed=seed) model = out.pop("model", None) res = {"bit": d_bit, **cnf.stats(), **out, "seed": seed} if out["status"] == "sat": state = [C.decode_word(model, w) for w in st] w1 = [C.decode_word(model, w) for w in W1] w2 = [w ^ p for w, p in zip(w1, pat)] a, b = tuple(state), tuple(state) for j in range(9): a = S.step(a, S.K[start + j], w1[j]); b = S.step(b, S.K[start + j], w2[j]) res.update({"state_hex": "".join("%08x" % v for v in state), "W_hex": ["%08x" % v for v in w1], "W_prime_hex": ["%08x" % v for v in w2], "verified": a == b and w1 != w2, "final_state_hex": "".join("%08x" % v for v in a)}) return res def main(): ap = argparse.ArgumentParser() ap.add_argument("--seed", type=int, default=1) ap.add_argument("--n", type=int, default=100_000) ap.add_argument("--start", type=int, default=0, help="step index i of the perturbation (uses K[i..i+8])") ap.add_argument("--sat-bits", default="all", help="comma list of bit positions for the SAT search, or 'all'") ap.add_argument("--sat-timeout", type=float, default=300) ap.add_argument("--out", default="results/reduced_round_sha256/local_collision.json") a = ap.parse_args() t0 = time.time() # (i) linear verification lin = {} for b in range(32): ok, traj = verify_linear(1 << b) lin[b] = {"cancels_after_9_steps": ok, "pattern_hex": ["%08x" % w for w in pattern(1 << b)], "register_difference_trajectory_hex": [["%08x" % v for v in s] for s in traj]} # the generic (symbolic) check: the map d -> final difference is linear, so 32 basis vectors suffice; # also check a few random multi-bit d rng = random.Random(a.seed) multi_ok = all(verify_linear(rng.getrandbits(32))[0] for _ in range(20)) print("(i) linear model: all 32 single-bit perturbations cancel:", all(v["cancels_after_9_steps"] for v in lin.values()), "; 20 random multi-bit:", multi_ok, file=sys.stderr) # (ii) empirical with real step nrng = np.random.default_rng(a.seed) emp = [] for b in range(32): r = empirical(b, a.n, nrng, a.start) emp.append(r) print(f"(ii) bit {b:2d}: collisions {r['n_collisions']}/{a.n} survival by step {r['survival_by_step']}", file=sys.stderr) # (iii) SAT bits = list(range(32)) if a.sat_bits == "all" else [int(x) for x in a.sat_bits.split(",")] sat = [] for b in bits: r = sat_conforming(b, a.start, a.sat_timeout, a.seed) sat.append(r) print(f"(iii) bit {b:2d}: {r['status']} in {r['wall_s']} s, conflicts {r.get('conflicts')}, verified {r.get('verified')}", file=sys.stderr) meas = {"linear_model": lin, "linear_model_random_multibit_ok": multi_ok, "empirical": emp, "sat": sat, "pattern_formula": "(d, S0(d)^S1(d), S1(S0(d)), 0, d, S0(d)^S1(d), 0, 0, d)"} stats = {"wall_s": round(time.time() - t0, 3), "peak_rss_mb": peak_rss_mb(), "step_evaluations_real": 2 * 9 * a.n * 32} provenance.record("sha256_local_collision_9step", {"n_per_bit": a.n, "start_step": a.start, "sat_bits": bits, "sat_timeout_s": a.sat_timeout, "model": "GH03 structure, absorbing Boolean functions"}, meas, seed=a.seed, extra={"op_stats": stats}, out=a.out, started=t0) print("wrote", a.out, stats) if __name__ == "__main__": main()