SAT-based analysis of SHA-3 competition finalists


  • Oleg S. Zaikin
  • Vadim V. Davydov
  • Anastasia P. Kiryanova


Boolean satisfiability problem
SAT solver
model checking
cryptographic hash function
preimage attack
SHA-3 competition


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.





Methods and algorithms of computational mathematics and their applications

Author Biographies

Oleg S. Zaikin

Vadim V. Davydov

Anastasia P. Kiryanova

ITMO University
• student


  1. T. H. Cormen, C. E. Leiserson, R. L. Rivest, and C. Stein, Introduction to Algorithms (MIT Press, Cambridge, 2001; Williams, Moscow, 2013).
  2. A. P. Alferov, A. Yu. Zubov, A. S. Kuz’min, and A. V. Cheremushkin, Fundamentals of Cryptography (Gelios ARV, Moscow, 2002) [in Russian].
  3. G. V. Bard, Algebraic Cryptanalysis (Springer, New York, 2009).
    doi 10.1007/978-0-387-88757-9
  4. 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
  5. M. R. Garey and D. S. Johnson, Computers and Intractability: a Guide to the Theory of NP-Completeness (W. H. Freeman, San Francisco, 1979).
  6. 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
  7. 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
  8. 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
  9. First SHA-3 Candidate Conference. . Cited June 21, 2024.
  10. 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
  11. J. A. Buchmann, Introduction to Cryptography (Springer, New York, 2004).
    doi 10.1007/978-1-4419-9003-7
  12. 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
  13. H. Feistel, “Cryptography and Computer Privacy,” Sci. Am. 228 (5), 15-23 (1973).
    doi 10.1038/scientificamerican0573-15
  14. 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
  15. 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
  16. 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
  17. 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
  18. R. F. Kayser, “Announcing Request for Candidate Algorithm Nominations for a New Cryptographic Hash Algorithm (SHA-3) Family,” Federal Register. 72 (212), 62 (2007).
  19. 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
  20. 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
  21. P. Gauravaram, L. R. Knudsen, K. Matusiewicz, et al., Gro stl -- a SHA-3 Candidate, . Cited June 21, 2024.
  22. N. Ferguson, S. Lucks, B. Schneier, et al., The Skein Hash Function Family. Submission to NIST (Round 3). 2010.
  23. H. Wu, The Hash Function JH. Submission to NIST (Round 3). 2011.
  24. 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
  25. SHA-3 Finalists Announced by NIST. Cited June 21, 2024.
  26. D. J. Bernstein, ChaCha, a Variant of Salsa20. . Cited June 21, 2024.
  27. E. Biham and O. Dunkelman, “A Framework for Iterative Hash Functions -- HAIFA,” Cryptology ePrint Archive, Paper 2007/278. . Cited June 21, 2024.
  28. 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
  29. J. Daemen and V. Rijmen, The Design of Rijndael (Springer, Berlin, 2002).
    doi 10.1007/978-3-662-04722-4
  30. 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.
  31. 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
  32. 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
  33. 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
  34. 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
  35. BLAKE. . Cited June 21, 2024.
  36. GROSTL. . Cited June 21, 2024.
  37. Hash Function JH. June 21, 2024.
  38. SHA-3 Keccak. . Cited June 21, 2024.
  39. The Skein Hash Function Family.
    https:// . Cited June 21, 2024.