Применение алгоритмов решения проблемы булевой выполнимости для анализа финалистов конкурса SHA-3

О. С. Заикин; В. В. Давыдов; А. П. Кирьянова

doi:10.26089/NumMet.v25r320

Authors

Oleg S. Zaikin Novosibirsk State University; Matrosov Institute for System Dynamics and Control Theory SB RAS (IDSTU SB RAS) https://orcid.org/0000-0002-0145-5010 (unauthenticated)
Vadim V. Davydov Saint Petersburg State University of Aerospace Instrumentation; QApp https://orcid.org/0000-0002-5544-2434 (unauthenticated)
Anastasia P. Kiryanova ITMO University https://orcid.org/0009-0006-0344-5111 (unauthenticated)

DOI:

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

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.

Author Biographies

Oleg S. Zaikin, Novosibirsk State University; Matrosov Institute for System Dynamics and Control Theory SB RAS (IDSTU SB RAS)

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

Saint-Petersburg State University of Aerospace Instrumentation;
QApp
• Assistant Professor
Anastasia P. Kiryanova, ITMO University

ITMO University
• student

References

T. H. Cormen, C. E. Leiserson, R. L. Rivest, and C. Stein, Introduction to Algorithms (MIT Press, Cambridge, 2001; Williams, Moscow, 2013).

A. P. Alferov, A. Yu. Zubov, A. S. Kuz’min, and A. V. Cheremushkin, Fundamentals of Cryptography (Gelios ARV, Moscow, 2002) [in Russian].

G. V. Bard, Algebraic Cryptanalysis (Springer, New York, 2009).
doi 10.1007/978-0-387-88757-9

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

First SHA-3 Candidate Conference.
https://csrc.nist.gov/events/2009/first-sha-3-candidate-conference . Cited June 21, 2024.

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

H. Feistel, “Cryptography and Computer Privacy,” Sci. Am. 228 (5), 15-23 (1973).
doi 10.1038/scientificamerican0573-15

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

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.

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

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.

D. J. Bernstein, ChaCha, a Variant of Salsa20.
https://cr.yp.to/chacha/chacha-20080120.pdf . Cited June 21, 2024.

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

BLAKE.
https://github.com/veorq/BLAKE.git . Cited June 21, 2024.

GROSTL.
https://github.com/monero-project/monero . Cited June 21, 2024.

Hash Function JH.
https://www3.ntu.edu.sg/home/wuhj/research/jh/.Cited June 21, 2024.

SHA-3 Keccak.
https://github.com/davidsteinsland/keccak . Cited June 21, 2024.

The Skein Hash Function Family.
https:// www.schneier.com/wp-content/uploads/2015/01/skein.zip . Cited June 21, 2024.