We introduce an efficient SAT-based space partitioning technique that enables systematic exploration of large search spaces in cryptanalysis. The approach divides complex search spaces into manageable subsets through combinatorial necklace generation, allowing precise tracking of explored regions while maintaining search completeness.We demonstrate the technique’s effectiveness through extensive cryptanalysis of Ascon-Hash256. For differential-based collision attacks, we conduct an exhaustive search of 2-round collision trails, proving that no collision trail with weight less than 156 exists. Through detailed complexity analysis and parameter optimization, we present an improved 2-round collision attack with complexity 261.79. We also discover new Semi-Free-Start (SFS) collision trails that enable practical attacks on both 3-round and 4-round Ascon-Hash256, especially improving the best known 4-round SFS trail from weight 295 to 250.Furthermore, applying the technique to Meet-in-the-Middle structure search yields improved attacks on 3-round Ascon-Hash256. We reduce the collision attack complexity from 2116.74 to 2114.13 with memory complexity 2112 (improved from 2116), and the preimage attack complexity from 2162.80 to 2160.75 with memory complexity 2160 (improved from 2162).
Liu et al. (Thu,) studied this question.