Geodesic
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 
@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},
     publisher = {mathdoc},
     volume = {25},
     number = {3},
     year = {2024},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/VMP_2024_25_3_a1/}
}
TY  - JOUR
AU  - O. S. Zaikin
AU  - V. V. Davydov
AU  - A. P. Kiryanova
TI  - SAT-based analysis of SHA-3 competition finalists
JO  - Numerical methods and programming
PY  - 2024
SP  - 259
EP  - 273
VL  - 25
IS  - 3
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/VMP_2024_25_3_a1/
LA  - ru
ID  - VMP_2024_25_3_a1
ER  - 
%0 Journal Article
%A O. S. Zaikin
%A V. V. Davydov
%A A. P. Kiryanova
%T SAT-based analysis of SHA-3 competition finalists
%J Numerical methods and programming
%D 2024
%P 259-273
%V 25
%N 3
%I mathdoc
%U http://geodesic.mathdoc.fr/item/VMP_2024_25_3_a1/
%G ru
%F 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/