Comparative Analysis of SMT Solvers for Differential Cryptanalysis of SHA-2

This work presents an experimental investigation on the performance differences among various SMT solvers in generating differential cryptanalysis collisions for the SHA-2 family of cryptographic hash functions, a widely adopted hash function, critical for maintaining data integrity and security of protocols like TLS. The research involved examining different parameters with these solvers, and their effects on the overall solving performance. These findings provide both a methodological baseline and actionable insights regarding solver effectiveness tailored towards helping shape future research in automated cryptanalysis.