RESEARCH RELIABILITY OF BLOCK CRYPTOGRAPHIC ALGORITHMS USING SAT METHODOLOGY

  • E. A. Maro Southern Federal University
Keywords: Satisfiability problem of Boolean formulas, algebraic cryptanalysis, PRESENT encryption algorithm, substitution block, S-box

Abstract

In matters of information security an important task is the development of methods for as-sessing security of confidential information. For many information protection systems information security assessment can be reduced to finding solutions of Boolean nonlinear equations systems and analyzing the complexity of various methods for solving such systems (algebraic analysis method). Algebraic methods of analysis are applied, for example, to the following tasks arising in the field of ensuring information security: – audit of the state of the protected object; – checking the correct functioning of programs; – analysis of the reliability of systems for protecting confi-dential information (including using cryptographic algorithms). This article presents proposed approach to the application of satisfiability problem (SAT) solvers for analyzing the reliability of block encryption algorithms, using as an example the lightweight encryption standard – PRESENT cipher. The research of the reliability of cryptographic algorithms for algebraic analysis methods consists in representing the encryption algorithm as a system of non-linear equations that connects the secret encryption key with plaintexts and ciphertexts. As a method for solving a nonlinear sys-tem of equations, paper considers the method of reducing to the search for performing sets of cor-responding SAT problem. For 3 rounds of the PRESENT encryption algorithm (using 6 known pairs of texts) a secret encryption key was found in 1005.68 sec. (search of the satisfiable value took 5.01 sec.). For 4 rounds of the PRESENT encryption algorithm, (using 8 known pairs of texts) 16 possible encryption keys were found in 3268.42 sec. (it took 527.51 seconds to find all the satis-fiable sets). A technique is proposed for assessing the reliability of symmetric block ciphers based on SAT-solutions using SAT-solvers Plingeling and CaDiCaL. Estimates of the reliability of cryp-tographic algorithms of information security obtained on the basis of algebraic analysis methods should be taken into account throw developing new and improving existing cryptographic systems.

References

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.
Published
2020-01-23
Issue
No 5 (2019)
Section
SECTION I. INFORMATION PROCESSING ALGORITHMS.