id: H19 title: The 9-step local collision holds with probability 1 in the XOR-linearised model and with low, position-dependent probability in the real step function axis: C kind: sha256 statement: The Chabaud–Joux/Gilbert–Handschuh correction pattern cancels any single-bit difference after 9 linearised steps (machine-checked); with modular additions the same pattern succeeds with probability ≈ 2^-c (c measured per bit position, highest at the MSB), and SAT finds conforming message words in seconds. motivation: C3/C4. assumptions: Linearisation of Ch and Maj as in Gilbert–Handschuh 2003. expected_contribution: Reproduction of a classical result with a formal proof of the linear part. related_work:
- chabaud1998differential
- gilbert2003security
- nikolic2008collisions possible_counterexamples: Linearised cancellation failing for some δ (ruled out by bv_decide). verification_strategy: experiments/reduced_round_sha256/local_collision.py + formal/ Lean theorem. computational_budget: minutes status: evaluated classification: known_reproduced evidence:
- results/reduced_round_sha256/summary.json
- results/reduced_round_sha256/local_collision.json
- formal/README.md verdict: 'Pattern (δ, Σ0δ⊕Σ1δ, Σ1(Σ0δ), 0, δ, Σ0δ⊕Σ1δ, 0, 0, δ) cancels in the linearised model for all δ (GF(2) check + Lean theorem localCollision_absorb). Real step: 0 collisions in 32 × 100 000 samples (bound 3·10⁻⁵); survival after step i 0.25 (bits 0–30) / 1.0 (bit 31), after i+1 ≈ 10⁻⁴, after i+2 zero. SAT finds conforming pairs for all 32 positions in 4.4–118 s, all verified.'
H19 — The 9-step local collision holds with probability 1 in the XOR-linearised model and with low, position-dependent probability in the real step function
The Chabaud–Joux/Gilbert–Handschuh correction pattern cancels any single-bit difference after 9 linearised steps (machine-checked); with modular additions the same pattern succeeds with probability ≈ 2^-c (c measured per bit position, highest at the MSB), and SAT finds conforming message words in seconds.