Automated Tool for Finding Practical Collisions on SPN-Based Hash Functions

In this paper, we present an automated tool for finding real colliding pairs in SPN-based hash functions. Our method enhances the value-difference modeling proposed by Liu et al. by extending it to direct verification of differential characteristics for collision even in structurally constrained settings, such as MMO (Matyas-Meyer-Oseas) and sponge-based schemes. Furthermore, it is applicable to bit-wise primitives such as PRESENT and GIFT, which are beyond the scope of existing rebound attacks. Our unified SAT-based tool eliminates manual steps by simultaneously searching for both differential characteristics and valid internal states. This enables us to exploit low-probability characteristics that were previously considered infeasible due to limited degrees of freedom. We demonstrate practical collision attacks on several lightweight hash functions, including the hashing modes of SKINNY, PRESENT, and GIFT, achieving either the best-known or entirely new collision results.