TY - GEN

T1 - Towards Better SAT Encodings for Hash Function Inversion Problems

AU - Kochemazov, S. E.

AU - Zaikin, O. S.

N1 - Conference code: 47

PY - 2024

Y1 - 2024

N2 - Inversion of reduced-round hash functions is one of the areas of cryptography, in which Boolean satisfiability (SAT) solvers show good performance. Recent results on the inversion of 43 -step MD4 using SAT make it possible to believe that more progress can be achieved by careful solver engineering and SAT encodings manipulation. In the present paper we consider possible ways to improve the SAT encodings for inversion of hash functions from the MD and SHA families, in particular, MD4, and SHA-1. We study the available encodings, including the ones proposed by Vegard Nossum, and made by automatic encoding tools. We then show that it is possible to make the encodings better by constructing the integer sums in a different way or eliminating some of the auxiliary variables via Boolean minimization. In the computational experiments we consider a variety of benchmarks, which encode reduced-round variants of the considered hash functions.

AB - Inversion of reduced-round hash functions is one of the areas of cryptography, in which Boolean satisfiability (SAT) solvers show good performance. Recent results on the inversion of 43 -step MD4 using SAT make it possible to believe that more progress can be achieved by careful solver engineering and SAT encodings manipulation. In the present paper we consider possible ways to improve the SAT encodings for inversion of hash functions from the MD and SHA families, in particular, MD4, and SHA-1. We study the available encodings, including the ones proposed by Vegard Nossum, and made by automatic encoding tools. We then show that it is possible to make the encodings better by constructing the integer sums in a different way or eliminating some of the auxiliary variables via Boolean minimization. In the computational experiments we consider a variety of benchmarks, which encode reduced-round variants of the considered hash functions.

KW - SAT

KW - cryptography

KW - hash functions

UR - https://www.scopus.com/record/display.uri?eid=2-s2.0-85198227886&origin=inward&txGid=b7d787a09b77681bad838c29f2b73cd3

UR - https://www.mendeley.com/catalogue/a95058d7-47cf-3819-b53d-61cc7fd43e89/

U2 - 10.1109/MIPRO60963.2024.10569193

DO - 10.1109/MIPRO60963.2024.10569193

M3 - Conference contribution

SN - 9798350382495

T3 - 2024 47th ICT and Electronics Convention, MIPRO 2024 - Proceedings

SP - 25

EP - 30

BT - 2024 47th ICT and Electronics Convention, MIPRO 2024 - Proceedings

PB - Institute of Electrical and Electronics Engineers Inc.

T2 - 47th ICT and Electronics Convention

Y2 - 20 May 2024 through 24 May 2024

ER -