Comparative Analysis of SMT Solvers for Differential Cryptanalysis of SHA-2
Barlik, M. & Brain, M. 
ORCID: 0000-0003-4216-7151 (2025).
Comparative Analysis of SMT Solvers for Differential Cryptanalysis of SHA-2.
In:
CEUR Workshop Proceedings.
SMT 2025: 23rd International Workshop on Satisfiability Modulo Theories, 10-11 Aug 2025, Glasgow, UK.
Abstract
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.
| Publication Type: | Conference or Workshop Item (Paper) |
|---|---|
| Additional Information: | © 2025 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0). |
| Publisher Keywords: | Satisfiability Modulo Theory, Differential Cryptanalysis, Cryptographic Hash Function, SHA-2, Theory of BitVectors |
| Subjects: | Q Science > QA Mathematics > QA75 Electronic computers. Computer science |
| Departments: | School of Science & Technology School of Science & Technology > Department of Computer Science |
| SWORD Depositor: |
Available under License Creative Commons: Attribution International Public License 4.0.
Download (1MB) | Preview
Export
Downloads
Downloads per month over past year
Metadata
MetadataActions (login required)
Admin Login