DOI: https://doi.org/10.26089/NumMet.v25r320

SAT-based analysis of SHA-3 competition finalists

Authors

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

Keywords:

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

Abstract

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.

Downloads

Published

2024-07-09

Issue

Vol. 25 (2024): Issue 3.

Section

Methods and algorithms of computational mathematics and their applications

Author Biographies

Oleg S. Zaikin

Novosibirsk State University;
Matrosov Institute for System Dynamics and Control Theory SB RAS (IDSTU SB RAS)
• Leading Researcher

Vadim V. Davydov

Saint-Petersburg State University of Aerospace Instrumentation;
QApp
• Assistant Professor

Anastasia P. Kiryanova

ITMO University
• student

References

  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.
    https://csrc.nist.gov/events/2009/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,
    https://drops.dagstuhl.de/storage/16dagstuhl-seminar-proceedings/dsp-vol09031/DagSemProc.09031.7/DagSemProc.09031.7.pdf . 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.
    https://web.archive.org/web/20110709093032/
    http://crypto.junod.info/2010/12/10/sha-3-finalists-announced-by-nist/. Cited June 21, 2024.
  26. D. J. Bernstein, ChaCha, a Variant of Salsa20.
    https://cr.yp.to/chacha/chacha-20080120.pdf . Cited June 21, 2024.
  27. 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.
  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.
    https://github.com/veorq/BLAKE.git . Cited June 21, 2024.
  36. GROSTL.
    https://github.com/monero-project/monero . Cited June 21, 2024.
  37. Hash Function JH.
    https://www3.ntu.edu.sg/home/wuhj/research/jh/.Cited June 21, 2024.
  38. SHA-3 Keccak.
    https://github.com/davidsteinsland/keccak . Cited June 21, 2024.
  39. The Skein Hash Function Family.
    https:// www.schneier.com/wp-content/uploads/2015/01/skein.zip . Cited June 21, 2024.

License

Copyright (c) 2024 О. С. Заикин, В. В. Давыдов, А. П. Кирьянова

Creative Commons License

This work is licensed under a Creative Commons Attribution 4.0 International License.