Partial mathematical modeling and analysis of the AES system
Partial mathematical modeling and analysis of the AES system
StatusVoR
Alternative title
Authors
Stachowiak, Sylwia
Kurkowski, Mirosław
Monograph
Monograph (alternative title)
Date
2023-11
Publisher
Journal title
Journal of Applied Mathematics and Computational Mechanics
Issue
4
Volume
22
Pages
Pages
64-78
ISSN
2299-9965
ISSN of series
Access date
2023-11
Abstract PL
Abstract 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.
Abstract other
Keywords PL
Keywords EN
mathematical modeling
AES
symmetric ciphers
satisfiability
SAT-based cryptanalysis
AES
symmetric ciphers
satisfiability
SAT-based cryptanalysis
Keywords other
Exhibition title
Place of exhibition (institution)
Exhibition curator
Type
License type
Funder
Time range from
Time range to
Contact person name
Related publication
Related publication
Grant/project name
Collections
Views
11Acquisition Date5.10.2024
Downloads
13Acquisition Date5.10.2024
Altmetrics©
Dimensions
Google Scholar
