Partial mathematical modeling and analysis of the AES system

• Autorzy: Stachowiak Sylwia , Kurkowski Mirosław

Identyfikatory

DOI

10.17512/jamcm.2023.4.06

• Języki publikacji: EN

Abstrakty

EN

Many types of decision problems can be solved using mathematical modeling and analysis. Such techniques are also developed on the border of mathematical logic and computer science. A good example is the translation of the issues examined into the Satisfiability Problem (SAT) of a logical propositional formula. Unfortunately, this method is not always practical, considering the high computational complexity of solving the SAT problem. It often happens that in the studied cases, the encoding formulas contain even hundreds of thousands of clauses and propositional variables. However, even in these cases, modern SAT solvers can sometimes successfully solve these problems. This approach can be used to cryptanalyze some symmetric ciphers or parts/modifications. In this case, the encryption algorithm is first translated into a boolean formula. Then additional formulas are created to encode randomly selected plaintext and the key bits. Using the SAT solver; we can count the values of the ciphertext bits. Then, using the SAT solver again, we proceed to the cryptanalysis of the cipher with the selected plaintext and proper ciphertext, looking for the bits of the encryption key. In this paper, we will present the new results of how SAT techniques behave against representative fragments of the AES cipher, the current standard for symmetric encryption. We also compare the results obtained in this case by several SAT solvers. In addition, we present the results of the SAT-solver CryptoMiniSat obtained during the attack on the 1st round of the AES-128 cipher.

Słowa kluczowe

EN

mathematical modeling; AES algorithm; symmetric cipher; satisfiability; sat-based cryptanalysis

PL

modelowanie matematyczne; algorytm AES; kryptoanaliza

• Wydawca: Wydawnictwo Politechniki Częstochowskiej
• Czasopismo: Journal of Applied Mathematics and Computational Mechanics
• Rocznik: 2023
• Tom: Vol. 22, nr 4
• Strony: 64--78
• Opis fizyczny: Bibliogr. 28 poz., rys., tab.

Twórcy

autor

Stachowiak Sylwia

• Department of Computer Science, University SWPS Warsaw, Poland

autor

Kurkowski Mirosław

• Institute of Computer Sciences, Cardinal Stefan Wyszynski University Warsaw, Poland

Bibliografia

• [1] Cook, S.A. (1971). The complexity of theorem-proving procedures. Proceedings of the Third Annual ACM Symposium on Theory of Computing - STOC -71.
• [2] Cook, S., & Mitchell, D. (1997). Finding hard instances of the satisfiability problem: A survey. Satisfiability Problem: Theory and Applications, 1-17.
• [3] Steingartner, W., Polakova, A., Praznak, P., & Novitzka, V. (2015). Linear logic in computer science. Journal of Applied Mathematics and Computational Mechanics, 14(1), 91-100.
• [4] Steingartner, W., Radakovic, D., Valkosak, F., & Macko, P. (2016). Some properties of coalgebras and their role in computer science. Journal of Applied Mathematics and Computational Mechanics, 15(4), 145-156.
• [5] Andrzejczak, M., & Dudzic, W. (2019). SAT attacks on ARX ciphers with automated equations generation. Infocommunications Journal, 11(4), 2-7.
• [6] Dwivedi, A.D., Kloucek, M., Morawiecki, P., Nikolic, I., Pieprzyk, J., & Wojtowicz, S. (2017). ´ SAT-based cryptanalysis of authenticated ciphers from the caesar competition. Proceedings of the 14th International Joint Conference on E-Business and Telecommunications.
• [7] Dudzic, W., & Kanciak, K. (2020). Using SAT solvers to finding short cycles in cryptographic algorithms. International Journal of Electronics and Telecommunications, 66(3), 443-448.
• [8] Morawiecki, P., & Srebrny, M. (2013). A SAT-based preimage analysis of reduced Keccak hash functions. Information Processing Letters, 113(10-11), 392-397.
• [9] Lee, H., Kim, S., Kang, H., Hong, D., Sung, J., & Hong, S. (2016). Efficient differential trail searching algorithm for ARX block ciphers. Journal of the Korea Institute of Information Security and Cryptology, 26(6), 1421-1430.
• [10] Sun, L., Wang, W., & Wang, M. (2021). Accelerating the search of differential and linear characteristics with the SAT method. IACR Transactions on Symmetric Cryptology, 1, 269-315.
• [11] Courtois, N.T., & Pieprzyk, J. (2002). Cryptanalysis of block ciphers with overdefined systems of equations. Lecture Notes in Computer Science, 267-287.
• [12] Gwynne, M. (2014). Attacking AES via Sat. Academia.edu. https://www.academia.edu/ 2594954/Attacking AES via SAT
• [13] Stachowiak, S., Kurkowski, M., & Sobon, A. (2021). SAT vs. substitution boxes of DES like ciphers. 2021 IEEE 30th International Conference on Enabling Technologies: Infrastructure for Collaborative Enterprises (WETICE).
• [14] Stachowiak, S., Kurkowski, M., & Sobon, A. (2021). SAT-based cryptanalysis of Salsa20 cipher. ´Progress in Image Processing, Pattern Recognition and Communication Systems, 252-266.
• [15] Chowaniec, M., Kurkowski, M., & Mazur, M. (2018). New results in direct SAT-based cryptanalysis of DES-like ciphers. In: Advances in Soft and Hard Computing, 282-294.
• [16] Sobon, A., Kurkowski, M., & Stachowiak, S. (2019). Towards complete SAT-based cryptanalysis of RC5 cipher. 2019 IEEE 15th International Scientific Conference on Informatics, 397-402.
• [17] Dworkin, M.J., Barker, E.B., Nechvatal, J.R., Foti, J., Bassham, L.E., Roback, E., & Dray jr., J.F. (2001). Advanced Encryption Standard (AES). NIST. https://www.nist.gov/publications/advanced-encryption-standard-aes
• [18] Ashokkumar, C., Giri, R.P., & Menezes, B. (2016). Highly efficient algorithms for AES key retrieval in cache access attacks. 2016 IEEE European Symposium on Security and Privacy.
• [19] Davis, M., Logemann, G., & Loveland, D. (1962). A machine program for theorem-proving. Communications of the ACM, 5(7), 394-397.
• [20] Sobon, A., Kurkowski, M., & Stachowiak, S. (2020). Complete SAT based cryptanalysis of RC5 cipher. Journal of Information and Organizational Sciences, 44(2), 365-382.
• [21] Ferguson, N., Kelsey, J., Lucks, S., Schneier, B., Stay, M., Wagner, D., & Whiting, D. (2001). Improved cryptanalysis of Rijndael. Fast Software Encryption, 213-230.
• [22] Gilbert, H., & Minier, M. (2000). A Collision Attack on 7 Rounds of Rijndael. The Third Advanced Encryption Standard Candidate Conference, 230-241.
• [23] Biham, E., Dunkelman, O., & Keller, N. (2005). Related-key boomerang and rectangle attacks. Lecture Notes in Computer Science, 507-525.
• [24] Kim, J., Hong, S., & Preneel, B. (2007). Related-key rectangle attacks on reduced AES-192 and AES-256. Fast Software Encryption, 225-241.
• [25] Biryukov, A., Khovratovich, D., & Nikolic, I. (2009). Distinguisher and related-key attack on the full AES-256. Advances in Cryptology - CRYPTO 2009, 231-249.
• [26] Biryukov, A., Dunkelman, O., Keller, N., Khovratovich, D., & Shamir, A. (2010). Key recovery attacks of practical complexity on AES-256 variants with up to 10 rounds. Advances in Cryptology - EUROCRYPT 2010, 299-319.
• [27] Biryukov, A., & Khovratovich, D. (2009). Related-key cryptanalysis of the full AES-192 and AES-256. Advances in Cryptology - ASIACRYPT 2009, 1-18.
• [28] Committee, SAT Competition Organization (2022). The International SAT Competition Web Page. SAT Competitions. http://satcompetition.org/

Uwagi

Opracowanie rekordu ze środków MNiSW, umowa nr SONP/SP/546092/2022 w ramach programu "Społeczna odpowiedzialność nauki" - moduł: Popularyzacja nauki i promocja sportu (2024).