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

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

Авторы

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

Ключевые слова:

проблема булевой выполнимости
SAT-решатель
Kissat
CBMC
проверка свойств программ
криптографическая хеш-функция
поиск прообраза
конкурс SHA-3

Аннотация

Рассматриваются финалисты конкурса SHA-3, организованного для принятия нового стандарта криптографической хеш-функции. Все пять финалистов до сих пор являются стойкими к поиску прообраза, т.е. для них невозможно за реальное время найти вход по известному выходу. Исследуется возможность нахождения прообразов неполнораундовых версий рассмотренных криптографических хеш-функций. Соответствующие задачи сведены к проблеме булевой выполнимости (SAT) с помощью инструментального средства CBMC, предназначенного для проверки свойств программ на языке C. Для решения построенных экземпляров SAT использован современный решатель Kissat. В сравнении с ранее опубликованными результатами, для четырех из пяти функций-финалистов удалось найти прообразы более сложных неполнораундовых версий.

Загрузки

Опубликован

2024-07-09

Выпуск

Том 25 (2024): Выпуск 3.

Раздел

Методы и алгоритмы вычислительной математики и их приложения

Авторы

О. С. Заикин

Новосибирский государственный университет
ул. Пирогова, 2, 630090, Новосибирск;
Институт динамики систем и теории управления имени В. М. Матросова СО РАН (ИДСТУ СО РАН)
ул. Лермонтова, 134, 664033, Иркутск
• ведущий научный сотрудник

В. В. Давыдов

Санкт-Петербургский государственный университет аэрокосмического приборостроения
ул. Большая Морская, д. 67, 190000, Санкт-Петербург;
Компания QAPP
Большой бульвар, д. 30, стр. 1, 121205, Москва
• доцент

А. П. Кирьянова

Университет ИТМО
ул. Ломоносова, д. 9, 191002, Санкт-Петербург
• студент

Библиографические ссылки

  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.

Лицензия

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

Лицензия Creative Commons

Это произведение доступно по лицензии Creative Commons «Attribution» («Атрибуция») 4.0 Всемирная.