#!/usr/bin/env python3 """ sat_tail_sr59.py — Phase 2 of the sr=59 hybrid collision attack on SHA-256. WHAT THIS DOES: Given an M[0] candidate where da[56]=0 (found by scan_m0.c, Phase 1), this script encodes a full 64-round SHA-256 collision as a SAT problem with gap placement: W[57..61] are free, W[62..63] are schedule-enforced. The SAT solver (kissat) finds values completing a verified collision. GAP PLACEMENT: Instead of leaving W[57..63] all free (sr=57), we leave only W[57..61] free and enforce the schedule equations for W[62] and W[63]: W[62] = sig1(W[60]) + W[55] + sig0(W[47]) + W[46] W[63] = sig1(W[61]) + W[56] + sig0(W[48]) + W[47] This works because W[60] and W[61] are free SAT variables. Freedom: 5 free words x 2 messages x 32 bits = 320 bits Collision condition: 256 bits Slack: ~2^64 solutions --> SAT in ~430 seconds (kissat) USAGE: python3 sat_tail_sr59.py --m0 0x17149975 # all-ones M[1..15] python3 sat_tail_sr59.py --m0 0xbd77497b --random-msg 42 # random M[1..15] python3 sat_tail_sr59.py --m0 0x17149975 --kissat /path/to/kissat REQUIREMENTS: - kissat SAT solver (https://github.com/arminbiere/kissat) - Python 3 (no pip dependencies) Authors: Robert Viragh and Claude (2026) """ import sys import os import time import argparse import subprocess import tempfile # -- SHA-256 constants and primitives ------------------------------------ MASK = 0xFFFFFFFF K = [ 0x428a2f98, 0x71374491, 0xb5c0fbcf, 0xe9b5dba5, 0x3956c25b, 0x59f111f1, 0x923f82a4, 0xab1c5ed5, 0xd807aa98, 0x12835b01, 0x243185be, 0x550c7dc3, 0x72be5d74, 0x80deb1fe, 0x9bdc06a7, 0xc19bf174, 0xe49b69c1, 0xefbe4786, 0x0fc19dc6, 0x240ca1cc, 0x2de92c6f, 0x4a7484aa, 0x5cb0a9dc, 0x76f988da, 0x983e5152, 0xa831c66d, 0xb00327c8, 0xbf597fc7, 0xc6e00bf3, 0xd5a79147, 0x06ca6351, 0x14292967, 0x27b70a85, 0x2e1b2138, 0x4d2c6dfc, 0x53380d13, 0x650a7354, 0x766a0abb, 0x81c2c92e, 0x92722c85, 0xa2bfe8a1, 0xa81a664b, 0xc24b8b70, 0xc76c51a3, 0xd192e819, 0xd6990624, 0xf40e3585, 0x106aa070, 0x19a4c116, 0x1e376c08, 0x2748774c, 0x34b0bcb5, 0x391c0cb3, 0x4ed8aa4a, 0x5b9cca4f, 0x682e6ff3, 0x748f82ee, 0x78a5636f, 0x84c87814, 0x8cc70208, 0x90befffa, 0xa4506ceb, 0xbef9a3f7, 0xc67178f2, ] H0 = [0x6a09e667, 0xbb67ae85, 0x3c6ef372, 0xa54ff53a, 0x510e527f, 0x9b05688c, 0x1f83d9ab, 0x5be0cd19] def rotr(x, n): return ((x >> n) | (x << (32 - n))) & MASK def sig0(x): return rotr(x, 7) ^ rotr(x, 18) ^ (x >> 3) def sig1(x): return rotr(x, 17) ^ rotr(x, 19) ^ (x >> 10) def S0(x): return rotr(x, 2) ^ rotr(x, 13) ^ rotr(x, 22) def S1(x): return rotr(x, 6) ^ rotr(x, 11) ^ rotr(x, 25) def Ch(e,f,g): return ((e & f) ^ ((~e) & g)) & MASK def Maj(a,b,c): return ((a & b) ^ (a & c) ^ (b & c)) & MASK def add(*args): s = 0 for a in args: s = (s + a) & MASK return s def sha256_compress(IV, W, rounds=64): a, b, c, d = IV[0], IV[1], IV[2], IV[3] e, f, g, h = IV[4], IV[5], IV[6], IV[7] for r in range(rounds): T1 = add(h, S1(e), Ch(e, f, g), K[r], W[r]) T2 = add(S0(a), Maj(a, b, c)) h, g, f, e = g, f, e, add(d, T1) d, c, b, a = c, b, a, add(T1, T2) return [add(a, IV[0]), add(b, IV[1]), add(c, IV[2]), add(d, IV[3]), add(e, IV[4]), add(f, IV[5]), add(g, IV[6]), add(h, IV[7])] # -- Self-contained CNF encoder ------------------------------------------ # Adapted from sha256_collision_cnf.py (verified correct encoder) class CNFEncoder: def __init__(self): self.nvars = 0 self.clauses = [] def new_var(self): self.nvars += 1 return self.nvars def new_word(self): return [self.new_var() for _ in range(32)] def const_word(self, val): w = self.new_word() for b in range(32): self.clauses.append([w[b] if (val >> b) & 1 else -w[b]]) return w def const_bit(self, val): v = self.new_var() self.clauses.append([v if val else -v]) return v def xor2(self, a, b): c = self.new_var() self.clauses.extend([[-a,-b,-c],[-a,b,c],[a,-b,c],[a,b,-c]]) return c def xor3(self, a, b, c): r = self.new_var() self.clauses.extend([ [a, b, c, -r], [a, -b, -c, -r], [-a, b, -c, -r], [-a, -b, c, -r], [a, b, -c, r], [a, -b, c, r], [-a, b, c, r], [-a, -b, -c, r] ]) return r def and2(self, a, b): c = self.new_var() self.clauses.extend([[a,-c],[b,-c],[-a,-b,c]]) return c def or2(self, a, b): c = self.new_var() self.clauses.extend([[-a,c],[-b,c],[a,b,-c]]) return c def maj3(self, a, b, c): r = self.new_var() self.clauses.extend([ [-a,-b,r], [-a,-c,r], [-b,-c,r], [a,b,-r], [a,c,-r], [b,c,-r] ]) return r def full_adder(self, a, b, cin): s = self.xor3(a, b, cin) cout = self.maj3(a, b, cin) return s, cout def add_words(self, A, B): result = [None]*32 carry = self.and2(A[0], B[0]) result[0] = self.xor2(A[0], B[0]) for i in range(1, 32): result[i], carry = self.full_adder(A[i], B[i], carry) return result def csa_words(self, A, B, C): S = [None]*32 Carry_raw = [None]*32 for i in range(32): S[i] = self.xor3(A[i], B[i], C[i]) Carry_raw[i] = self.maj3(A[i], B[i], C[i]) zero = self.const_bit(0) C_shifted = [zero] + Carry_raw[:31] return S, C_shifted def add5_words(self, A, B, C, D, E): S1, C1 = self.csa_words(A, B, C) S2, C2 = self.csa_words(S1, D, E) S3, C3 = self.csa_words(S2, C1, C2) return self.add_words(S3, C3) def rotr_word(self, W, n): return W[n:] + W[:n] def shr_word(self, W, n): zeros = [self.const_bit(0) for _ in range(n)] return W[n:] + zeros def xor_words(self, A, B): return [self.xor2(A[i], B[i]) for i in range(32)] def xor3_words(self, A, B, C): return [self.xor3(A[i], B[i], C[i]) for i in range(32)] def SIGMA0(self, W): return self.xor3_words(self.rotr_word(W,2), self.rotr_word(W,13), self.rotr_word(W,22)) def SIGMA1(self, W): return self.xor3_words(self.rotr_word(W,6), self.rotr_word(W,11), self.rotr_word(W,25)) def sigma0(self, W): return self.xor3_words(self.rotr_word(W,7), self.rotr_word(W,18), self.shr_word(W,3)) def sigma1(self, W): return self.xor3_words(self.rotr_word(W,17), self.rotr_word(W,19), self.shr_word(W,10)) def Ch_func(self, E, F, G): r = [None]*32 for i in range(32): r[i] = self.new_var() self.clauses.extend([ [-E[i], -F[i], r[i]], [-E[i], F[i], -r[i]], [E[i], -G[i], r[i]], [E[i], G[i], -r[i]] ]) return r def Maj_func(self, A, B, C): return [self.maj3(A[i], B[i], C[i]) for i in range(32)] def sha256_round(self, state, W, k_val): a,b,c,d,e,f,g,h = state Kw = self.const_word(k_val) T1 = self.add5_words(h, self.SIGMA1(e), self.Ch_func(e,f,g), Kw, W) T2 = self.add_words(self.SIGMA0(a), self.Maj_func(a,b,c)) return [self.add_words(T1,T2), a, b, c, self.add_words(d,T1), e, f, g] def equal_words(self, A, B): for i in range(32): self.clauses.extend([[-A[i],B[i]], [A[i],-B[i]]]) # -- Encoding and solving ------------------------------------------------ FREE_SET = {57, 58, 59, 60, 61} def encode_sr59(M1_vals, M2_vals, output_file): """ Encode a full 64-round SHA-256 collision with gap placement at sr=59. M1/M2 are fixed; W[57..61] are free; W[62..63] enforced by schedule. """ enc = CNFEncoder() # Fix message words as constants M1 = [enc.const_word(M1_vals[i]) for i in range(16)] M2 = [enc.const_word(M2_vals[i]) for i in range(16)] # Build schedule with gap placement W1 = list(M1) W2 = list(M2) free_w1 = {} free_w2 = {} for t in range(16, 64): if t in FREE_SET: w1 = enc.new_word() w2 = enc.new_word() W1.append(w1) W2.append(w2) free_w1[t] = w1 free_w2[t] = w2 else: W1.append(enc.add_words(enc.add_words(enc.add_words( W1[t-16], enc.sigma0(W1[t-15])), W1[t-7]), enc.sigma1(W1[t-2]))) W2.append(enc.add_words(enc.add_words(enc.add_words( W2[t-16], enc.sigma0(W2[t-15])), W2[t-7]), enc.sigma1(W2[t-2]))) # Fix IV as standard H0 IV = [enc.const_word(H0[i]) for i in range(8)] # 64 rounds of compression for both messages state1 = list(IV) state2 = list(IV) for r in range(64): state1 = enc.sha256_round(state1, W1[r], K[r]) state2 = enc.sha256_round(state2, W2[r], K[r]) # Davies-Meyer feedforward + collision condition H1 = [enc.add_words(IV[i], state1[i]) for i in range(8)] H2 = [enc.add_words(IV[i], state2[i]) for i in range(8)] for i in range(8): enc.equal_words(H1[i], H2[i]) # Write DIMACS CNF with open(output_file, 'w') as f: f.write(f"p cnf {enc.nvars} {len(enc.clauses)}\n") for t in sorted(free_w1.keys()): bits = ','.join(str(free_w1[t][b]) for b in range(32)) f.write(f"c W1[{t}] bits(LSB..MSB): {bits}\n") for t in sorted(free_w2.keys()): bits = ','.join(str(free_w2[t][b]) for b in range(32)) f.write(f"c W2[{t}] bits(LSB..MSB): {bits}\n") for cl in enc.clauses: f.write(' '.join(str(l) for l in cl) + ' 0\n') return enc.nvars, len(enc.clauses), free_w1, free_w2 def extract_word(assignment, var_list): val = 0 for b in range(32): if assignment.get(var_list[b], False): val |= (1 << b) return val # -- Main ---------------------------------------------------------------- def main(): parser = argparse.ArgumentParser( description='Phase 2: Solve gap-placed SAT tail for sr=59 collision') parser.add_argument('--m0', required=True, help='M[0] candidate from scan_m0 (hex, e.g., 0x17149975)') parser.add_argument('--random-msg', type=int, default=None, help='Random seed for M[1..15] (default: all-ones)') parser.add_argument('--kissat', default='kissat', help='Path to kissat binary (default: kissat in PATH)') parser.add_argument('--timeout', type=int, default=1800, help='SAT solver timeout in seconds (default: 1800)') args = parser.parse_args() m0 = int(args.m0, 16) if args.m0.startswith('0x') else int(args.m0) # Build M[1..15] if args.random_msg is not None: import random as rng rng.seed(args.random_msg) m_rest = [rng.getrandbits(32) for _ in range(15)] print(f"M[1..15]: random (seed {args.random_msg})") else: m_rest = [0xFFFFFFFF] * 15 print(f"M[1..15]: all-ones") # Build message blocks (MSB kernel) M1 = [m0] + m_rest M2 = list(M1) M2[0] ^= 0x80000000 M2[9] ^= 0x80000000 print(f"\nSR=59 Gap-Placed Collision Solver") print(f"==================================") print(f"M[0] = 0x{m0:08x}") print(f"dM[0] = dM[9] = 0x80000000 (MSB kernel)") print(f"Free: W[57..61] (5 words per message)") print(f"Enforced: W[16..56, 62, 63] (43 schedule equations)") # Quick check: verify da[56]=0 (prerequisite) W1_det = list(M1) W2_det = list(M2) for i in range(16, 57): W1_det.append(add(sig1(W1_det[i-2]), W1_det[i-7], sig0(W1_det[i-15]), W1_det[i-16])) W2_det.append(add(sig1(W2_det[i-2]), W2_det[i-7], sig0(W2_det[i-15]), W2_det[i-16])) a1, b1, c1, d1, e1, f1, g1, h1 = H0 a2, b2, c2, d2, e2, f2, g2, h2 = H0 for r in range(57): T1 = add(h1, S1(e1), Ch(e1, f1, g1), K[r], W1_det[r]) T2 = add(S0(a1), Maj(a1, b1, c1)) h1, g1, f1, e1 = g1, f1, e1, add(d1, T1) d1, c1, b1, a1 = c1, b1, a1, add(T1, T2) T1 = add(h2, S1(e2), Ch(e2, f2, g2), K[r], W2_det[r]) T2 = add(S0(a2), Maj(a2, b2, c2)) h2, g2, f2, e2 = g2, f2, e2, add(d2, T1) d2, c2, b2, a2 = c2, b2, a2, add(T1, T2) da56 = a1 ^ a2 print(f"\nPrecheck: da[56] = 0x{da56:08x}", end='') if da56 != 0: print(f" (HW={bin(da56).count('1')})") print(f"\nERROR: da[56] != 0. This M[0] is not a valid Phase 1 candidate.") sys.exit(1) print(f" OK") # Encode the full 64-round SAT problem cnf_path = tempfile.mktemp(suffix='.cnf') print(f"\nEncoding full 64-round collision with gap placement...") t0 = time.time() nv, nc, fw1, fw2 = encode_sr59(M1, M2, cnf_path) t_enc = time.time() - t0 print(f" {nv} vars, {nc} clauses ({t_enc:.1f}s)") # Solve with kissat print(f" Solving with kissat (timeout={args.timeout}s)...", flush=True) t0 = time.time() try: result = subprocess.run( [args.kissat, cnf_path, f'--time={args.timeout}'], capture_output=True, text=True, timeout=args.timeout + 60 ) except FileNotFoundError: print(f"\nERROR: kissat not found at '{args.kissat}'") print(f"Install: git clone https://github.com/arminbiere/kissat && cd kissat && ./configure && make") os.unlink(cnf_path) sys.exit(1) solve_time = time.time() - t0 os.unlink(cnf_path) if 's SATISFIABLE' not in result.stdout: if 's UNSATISFIABLE' in result.stdout: print(f" UNSAT ({solve_time:.1f}s) — unexpected if da[56]=0") else: print(f" UNKNOWN/TIMEOUT ({solve_time:.1f}s)") for line in result.stderr.split('\n')[-10:]: if line.strip(): print(f" {line.strip()}") sys.exit(1) print(f" SAT! Solved in {solve_time:.1f}s") # Extract solution assignment = {} for line in result.stdout.split('\n'): if line.startswith('v '): for lit in line.split()[1:]: v = int(lit) if v == 0: break assignment[abs(v)] = (v > 0) W1_free = {t: extract_word(assignment, fw1[t]) for t in sorted(fw1.keys())} W2_free = {t: extract_word(assignment, fw2[t]) for t in sorted(fw2.keys())} # Build full schedule and verify W1_full = list(M1[:16]) W2_full = list(M2[:16]) for t in range(16, 64): if t in FREE_SET: W1_full.append(W1_free[t]) W2_full.append(W2_free[t]) else: W1_full.append(add(sig1(W1_full[t-2]), W1_full[t-7], sig0(W1_full[t-15]), W1_full[t-16])) W2_full.append(add(sig1(W2_full[t-2]), W2_full[t-7], sig0(W2_full[t-15]), W2_full[t-16])) # Verify schedule compliance sr = 16 for t in range(16, 64): exp1 = add(sig1(W1_full[t-2]), W1_full[t-7], sig0(W1_full[t-15]), W1_full[t-16]) exp2 = add(sig1(W2_full[t-2]), W2_full[t-7], sig0(W2_full[t-15]), W2_full[t-16]) if exp1 == W1_full[t] and exp2 == W2_full[t]: sr += 1 # Verify collision H1 = sha256_compress(H0, W1_full) H2 = sha256_compress(H0, W2_full) collision = all(H1[i] == H2[i] for i in range(8)) print(f"\n{'='*60}") if collision and sr == 59: print(f"*** 64-ROUND SHA-256 COLLISION VERIFIED (sr=59) ***") elif collision: print(f"*** COLLISION VERIFIED (sr={sr}, expected 59) ***") else: print(f"*** VERIFICATION FAILED ***") print(f"{'='*60}") print(f"Schedule: {sr-16}/48 equations (sr={sr})") print(f"Solve time: {solve_time:.1f}s") print(f"\nM1[0..15]: {' '.join(f'{w:08x}' for w in M1)}") print(f"M2[0..15]: {' '.join(f'{w:08x}' for w in M2)}") print(f"\nFree words (gap positions 57-61):") for t in sorted(W1_free.keys()): print(f" W1[{t}] = 0x{W1_free[t]:08x} W2[{t}] = 0x{W2_free[t]:08x}") print(f"\nEnforced schedule words:") print(f" W1[62] = 0x{W1_full[62]:08x} W2[62] = 0x{W2_full[62]:08x}") print(f" W1[63] = 0x{W1_full[63]:08x} W2[63] = 0x{W2_full[63]:08x}") print(f"\nH: {' '.join(f'{w:08x}' for w in H1)}") if not collision: print(f"H1: {' '.join(f'{w:08x}' for w in H1)}") print(f"H2: {' '.join(f'{w:08x}' for w in H2)}") sys.exit(1) if __name__ == '__main__': main()