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