ИССЛЕДОВАНИЕ НАДЕЖНОСТИ БЛОЧНЫХ КРИПТОГРАФИЧЕСКИХ АЛГОРИТМОВ С ПОМОЩЬЮ МЕТОДОЛОГИИ SAT

Е. А. Маро

Е. А. Маро Южный Федеральный Университет

Ключевые слова: Задача выполнимости булевых формул, алгебраический криптоанализ, алгоритм шифрования PRESENT, блок замены, S-блоки

Аннотация

В вопросах обеспечения информационной безопасности важной задачей является ис-следование методов оценки защищенности конфиденциальной информации. Для многих систем защиты информации оценка защищенности информации может быть сведена к поиску решений систем булевых нелинейных уравнений и анализу трудоемкости различных методов решения подобных систем (алгебраическому методу анализа). Алгебраические методы анализа применяются, например, к следующим задачам, возникающим в сфере обеспечения информационной безопасности: – аудит состояния защищаемого объекта; – проверка корректности функционирования программ; – анализ надежности систем за-щиты конфиденциальной информации (в том числе при использовании криптографических преобразований). В данной статье представлен предлагаемый подход к применению поиска задачи выполнимости булевых формул (satisfiability problem, SAT) для анализа надежности блочных алгоритмов шифрования, на примере стандарта легковесного шифрования - шиф-ра PRESENT (ISO/IEC 29192-2:2019). Исследование надежности криптографических алго-ритмов к алгебраическим методам анализа заключается в представлении алгоритма шиф-рования в виде системы нелинейных уравнений, связывающей секретный ключ шифрования с открытым и зашифрованным текстом. В качестве метода решения нелинейной систе-мы уравнений в работе рассматривается метод сведения к поиску выполняющих наборов для соответствующей SAT-задачи. Для 3 раундов алгоритма шифрования PRESENT при использовании 6 известных пар текстов был найден секретный ключ шифрования за 1005,68 сек. (поиск выполняющего набора занял 5,01 сек.). Для 4 раундов алгоритма шифро-вания PRESENT при использовании 8 известных пар текстов были найдены 16 возможных ключей шифрования за 3268,42 сек. (для поиска всех выполняющих наборов потребовалось 527,51 сек.). Предложена методика проведения оценки надежности симметричных блоч-ных шифров на основе сведения к поиску SAT-решений с применением SAT-решателей Plingeling и CaDiCaL. Полученные на основе алгебраических методов анализа оценки на-дежности криптографических средств защиты информации целесообразно учитывать при разработке новых и усовершенствовании существующих криптографических систем.

Литература

1. Pavlenko A., Semenov A., Ulyantsev V. Evolutionary Computation Techniques for Constructing SAT-Based Attacks in Algebraic Cryptanalysis, Theory and Applications of Models of Computa-tion, Part of the Lecture Notes in Computer Science book series (LNCS, volume 11454).
2. Slonkina I. Issledovanie algoritmov razvertivania klucha blochnykh shifrsistem, rednaznachennie dlya is ol’zovaniya v sreda h s ogranichennymi resursami, s omosh’uy metodologii SAT [Investigation of key cryptographic systems key deployment algorithms for use in resource-limited environments using the SAT methodology], Materialy Ezhegodnoy nauchno-practicheskoy konferentsii «RusCrypto’2019» [Materials of the annual international scientific- ractical conference «RusCry to’2019»]. Available at: https://www.ruscrypto.ru/ re-source/archive/rc2019/files/18_Slonkina.pdf.
3. Marshalko G.B., Mkhitaryan A.G. Logicheskiy criptoanaliz funktsii kheshirovaniya GOST R 34.11-2012 [Logical cryptanalysis of the hashing function GOST R 34.11-2012], Materialy Ezhegodnoy nauchno-practicheskoy konferentsii «RusCrypto’2019» [Materials of the annual international scientific- ractical conference «RusCry to’2019»], Available at: https://www.ruscrypto.ru/resource/archive/rc2019/files/02_Marshalko_Mkhitaryan.pdf.
4. Dwivedi A.D., Klouček M., Morawiecki P., Wójtowicz S., Pieprzyk J., Nikolić I. SAT-based Cryptanalysis of Authenticated Ciphers from the CAESAR Competition, The 14th Interna-tional Conference on Security and Cryptography (SECRYPT 2017), Madrid, Spain.
5. Semenov A., Zaikin O., Otpuschennikov I., Kochemazov S. and Ignatiev A. On cryptographic attacks using backdoors for SAT, In the Thirty-Second AAAIConference on Artificial Intelli-gence, AAAI’2018, 2018, pp. 6641-6648.
6. Рипатти А.В. Алгоритмы расщепления и числа Ван-дер-Вардена. Available at: https://habrahabr.ru/post/224069/.
7. Semenov A.A. Primenenie algoritmov resheniya problem bulevoy vypolnimosti (SAT) k kombinatornym zadacham [Application of algorithms for solving Boolean satisfiability prob-lems (SAT) to combinatorial problems], XII Vserossiyskoe soveshchanie po problemam upravleniya [XII All-Russian Meeting on Management Problems], 2014, pp. 7361-7374.
8. Soos M., Nohl K., Castelluccia C. Extending SAT Solvers to Cryptographic Problems, Theory and Applications of Satisfiability Testing – SAT, 2009, pp. 244-257.
9. Soos M. CryptoMiniSat 2.5.1. Available at: http://www.msoos.org/wordpress/wp-content/uploads/2010/08/cryptominisat-2.5.1.pdf.
10. Bogdanov A., Knudsen L.R., Leander G., Paar C., Poschmann A., Robshaw M.J., Seurin B., Vikkelsoe C. PRESENT: An ultra-light--weight block cipher, Cryptographic Hardware and Embedded Systems- -CHES ’07, 9th International Workshop, Vienna, Austria, 2007, Vol. 4727, pp. 450-466.
11. ISO/IEC 29192-2:2019 Information security – Lightweight cryptography – Part 2: Block ci-phers. Available at: https://www.iso.org/standard/78477.html.
12. Bard G. Algebraic Cryptanalysis, 2009, 356 p.
13. Nakahara J., Sepehrdad P., Zhang B., Wang M. Linear (Hull) and Algebraic Cryptanalysis of the Block Cipher PRESENT, 8th International Conference on Cryptology and Network Securi-ty, CANS ’09, New York, 2009, pp. 58-75.
14. Sage Tutorial in Russian. Выпуск 7.0. Available at: http://doc.sagemath.org/pdf/ru/ tutori-al/SageTutorial_ru.pdf.
15. Sage Reference Manual: Sat. Release 5.10. Available at: ftp://ftp.iitb.ac.in/packages/ sagemath/doc/en/reference/sat/sat.pdf.
16. Biere A., Heule M., Van Maaren H., Walsh T. Handbook of Satisfiability. IOS Press, 2009, 980 p.
17. Babenko L.K., Maro E.A., Anikeev M.V. Application of Algebraic Cryptanalysis to MAGMA and PRESENT Block Encryption Standards, Proceedings of the 11th IEEE International Conference on Application of Information and Communication Technologies (AICT 2017), pp. 272-278.
18. Lingeling, Plingeling and Treengeling. Available at: http://fmv.jku.at/lingeling/.
19. CaDiCaL Simplified Satisfiability Solver. Available at: http://fmv.jku.at/cadical/.
20. Marijn J.H. Heule, Matti Järvisalo, and Martin Suda. Proceedings of SAT COMPETITION 2018 Solver and Benchmark Descriptions. Available at: https://helda.helsinki.fi/bitstream/ handle/10138/237063/sc2018_proceedings.pdf.