SAT-based analysis of SHA-3 competition finalists
Numerical methods and programming, Tome 25 (2024) no. 3, pp. 259-273
Cet article a éte moissonné depuis la source Math-Net.Ru
SHA-3 competition was held to develop a new standard cryptographic hash funcion. In the present study, finalists of SHA-3 are considered. All of them are still preimage resistant — i.e., it is infeasible to find their outputs given inputs. Preimage resistance of round-reduced versions of the functions is investigated. The corresponding problems are reduced to the Boolean satisfiability problem (SAT) via the CBMC model checker for programs written in C. To solve the constructed SAT instances, the state-of-the-art SAT solver Kissat is applied. Compared to previously published results, for four out of five SHA-3 finalists preimages were found for harder round-reduced versions.
Keywords:
Boolean satisfiability problem, SAT solver, CBMC, model checking, cryptographic hash function, preimage attack, SHA-3 competition.
Mots-clés : Kissat
Mots-clés : Kissat
@article{VMP_2024_25_3_a1,
author = {O. S. Zaikin and V. V. Davydov and A. P. Kiryanova},
title = {SAT-based analysis of {SHA-3} competition finalists},
journal = {Numerical methods and programming},
pages = {259--273},
year = {2024},
volume = {25},
number = {3},
language = {ru},
url = {http://geodesic.mathdoc.fr/item/VMP_2024_25_3_a1/}
}
O. S. Zaikin; V. V. Davydov; A. P. Kiryanova. SAT-based analysis of SHA-3 competition finalists. Numerical methods and programming, Tome 25 (2024) no. 3, pp. 259-273. http://geodesic.mathdoc.fr/item/VMP_2024_25_3_a1/