The School of Computer Science is pleased to present…
SHA-256 Collision Attack with Programmatic SAT
MSc Thesis Proposal by: Nahiyan Alamgir
Date: Wednesday November 29, 2023
Time: 9:30 AM – 10: 30 AM
Location: Essex Hall, Room 105
Abstract:
Cryptographic hash functions play a crucial role in ensuring data se-
curity and integrity. These functions take variable-length inputs and pro-
duce fixed-length hashes. A prominent hash function, SHA-256, is trusted
in digital signatures, certificates, and data integrity. One of its critical
properties is collision resistance, meaning that it should be infeasible to
find two different inputs giving the same hash. Currently, the best SHA-
256 collision attack in practice (Mendel et al., 2013) employs differential
cryptanalysis. This attack involves identifying relationships between the
hash function’s state and message bits and uses a search tool that cleverly
branches on the most constrained bits. In our study, we propose using a
satisfiability (SAT) solver as a search tool to assess SHA-256’s collision
resistance. SAT solvers take problems as Boolean formulas and search for
solutions satisfying those formulas. An advantage of SAT solvers is their
built-in conflict-analysis system, which enhances their effectiveness over
regular search tools for a wide range of problems. While SAT solvers have
been used in the context of differential cryptanalysis for collision attacks,
our approach will leverage programmatic SAT solving. This approach
involves dynamically guiding the SAT solver via differential analysis of
SHA-256. We utilize a Computer Algebra System (CAS) to detect incon-
sistencies, enforce high-level constraints between bits, and perform custom
branching on the most constrained bits. In summary, this research aims to
bridge SAT solving for the first time with the sophisticated cryptanalysis
techniques used by Mendel et al.
Keywords: SAT Solving, Differential Cryptanalysis, Cryptographic Hash Function, SHA-256
Thesis Committee:
Internal Reader: Dr. Saeed Samet
External Reader: Dr. Huapeng Wu
Advisor: Dr. Curtis Bright