SAT-based analysis of SHA-3 competition finalists
Numerical methods and programming, Tome 25 (2024) no. 3, pp. 259-273
Voir la notice de l'article provenant de 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
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/
@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/}
}