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.
F. Massacci and L. Marraro, “Logical Cryptanalysis as a SAT Problem,” J. Autom. Reason. 24 (1-2), 165-203 (2000). doi 10.1023/A: 1006326723002
M. R. Garey and D. S. Johnson, Computers and Intractability: a Guide to the Theory of NP-Completeness (W. H. Freeman, San Francisco, 1979).
J. P. Marques-Silva and K. A. Sakallah, “GRASP -- a New Search Algorithm for Satisfiability,” in Proc. Int. Conf. on Computer Aided Design, San Jose, USA, November 10-14, 1996. doi 10.1109/ICCAD.1996.569607
R. Impagliazzo, L. A. Levin, and M. Luby, “Pseudo-Random Generation from One-Way Functions,” in Proc. Twenty-First Annual ACM Symposium on Theory of Computing, Washington, Seattle, USA, May 14-17, 1989. doi 10.1145/73007.73009
I. Mironov and L. Zhang, “Applications of SAT Solvers to Cryptanalysis of Hash Functions,” in Lecture Notes in Computer Science (Springer, Berlin, 2006), Vol. 4121, pp. 102-115. doi 10.1007/11814948_13
E. Homsirikamol, P. Morawiecki, M. Rogawski, and M. Srebrny, “Security Margin Evaluation of SHA-3 Contest Finalists through SAT-Based Attacks,” in Lecture Notes in Computer Science (Springer, Berlin, 2012), Vol. 7564, pp. 56-67. doi 10.1007/978-3-642-33260-9_4
J. A. Buchmann, Introduction to Cryptography (Springer, New York, 2004). doi 10.1007/978-1-4419-9003-7
P. Rogaway and T. Shrimpton, “Cryptographic Hash-Function Basics: Definitions, Implications, and Separations for Preimage Resistance, Second-Preimage Resistance, and Collision Resistance,” in Lecture Notes in Computer Science (Springer, Berlin, 2004), Vol. 3017, pp. 371-388. doi 10.1007/978-3-540-25937-4_24
C. E. Shannon, “Communication Theory of Secrecy Systems,” Bell Syst. Tech. J. 28 (4), 656-715 (1949). doi 10.1002/j.1538-7305.1949.tb00928.x
R. C. Merkle, “A Certified Digital Signature,” in Lecture Notes in Computer Science (Springer, New York, 2001), Vol. 435, pp. 218-238. doi 10.1007/0-387-34805-0_21
I. B. Damgaard, “A Design Principle for Hash Functions,” in Lecture Notes in Computer Science (Springer, New York, 2001), Vol. 435, pp. 416-427. doi 10.1007/0-387-34805-0_39
C. Paar and J. Pelzl, “Hash Functions,” in Understanding Cryptography (Springer, Berlin, 2010), pp. 293-317. doi 10.1007/978-3-642-04101-3_11
R. F. Kayser, “Announcing Request for Candidate Algorithm Nominations for a New Cryptographic Hash Algorithm (SHA-3) Family,” Federal Register. 72 (212), 62 (2007).
G. Bertoni, J. Daemen, M. Peeters, and G. Van Assche, “Keccak,” in Lecture Notes in Computer Science (Springer, Berlin, 2013), Vol. 7881, pp. 313-314. doi 10.1007/978-3-642-38348-9_19
J.-P. Aumasson, W. Meier, R. C.-W. Phan, and L. Henzen, The Hash Function BLAKE (Springer, Berlin, 2014). doi 10.1007/978-3-662-44757-4
N. Ferguson, S. Lucks, B. Schneier, et al., The Skein Hash Function Family. Submission to NIST (Round 3). 2010.
H. Wu, The Hash Function JH. Submission to NIST (Round 3). 2011.
B. Preneel, “The State of Hash Functions and the NIST SHA-3 Competition,” in Lecture Notes in Computer Science (Springer, Berlin, 2009), Vol. 5487, pp. 1-11. doi 10.1007/978-3-642-01440-6_1
E. Biham and O. Dunkelman, “A Framework for Iterative Hash Functions -- HAIFA,” Cryptology ePrint Archive, Paper 2007/278. https://eprint.iacr.org/2007/278 . Cited June 21, 2024.
S. Lucks, “A Failure-Friendly Design Principle for Hash Functions,” in Lecture Notes in Computer Science (Springer, Berlin, 2005), Vol. 3788, pp. 474-494. doi 10.1007/11593447_26
J. Daemen and V. Rijmen, The Design of Rijndael (Springer, Berlin, 2002). doi 10.1007/978-3-662-04722-4
A. Biere and M. Fleury, “Gimsatul, IsaSAT and Kissat Entering the SAT Competition 2022,” in Proc. SAT Competition 2022 - Solver and Benchmark Descriptions , Vol. B-2022-1, pp. 10-11. University of Helsinki, 2022.
V. S. Kondratiev, A. A. Semenov, and O. S. Zaikin, “Duplicates of Conflict Clauses in CDCL Derivation and Their Usage to Invert Some Cryptographic Functions,” Numerical Methods and Programming. 20 (1), 54-66 (2019). doi 10.26089/NumMet.v20r106
O. Zaikin, “Inverting 43-Step MD4 via Cube-and-Conquer,” in Proc. IJCAI-ECAI, Vienna, Austria, July 23-29, 2022. doi 10.24963/ijcai.2022/263
E. Clarke, D. Kroening, and F. Lerda, “A Tool for Checking ANSI-C Programs,” in Lecture Notes in Computer Science (Springer, Berlin, 2004), Vol. 2988, pp. 168-176. doi 10.1007/978-3-540-24730-2_15
A. Semenov, I. Otpuschennikov, I. Gribanova, et al., “Translation of Algorithmic Descriptions of Discrete Functions to SAT with Applications to Cryptanalysis Problems,” Log. Methods Comput. Sci. 16 (1), 1-29 (2020). doi 10.23638/LMCS-16(1: 29)2020