Propositional encoding of direct and inverse round transformations in attacks on some block ciphers
We suggest an attack on block ciphers, which is based on the well-known meet-in-the-middle strategy. To solve the corresponding cryptanalysis equations, algorithms for solving the Boolean satisfiability problem (SAT) are used. The main know-how consists in the usage in the propositional encoding of the considered cipher not only information about direct round transformations, but also information about inverse round transformations. Using the suggested type of encodings, we have constructed runtime estimations of guess-and-determine attacks on several block ciphers with reduced number of rounds (6-round DES, 6-round PRESENT, 6-round and 8-round GOST 2814789). It turned out that in some cases these attacks are several times more effective than attacks, in which standard methods of propositional encodings are used.
Keywords
Boolean satisfiability problem,
DES,
PRESENT,
block cipher,
GOST 28147-89,
криптоанализ,
задача булевой выполнимости,
PRESENT,
DES,
ГОСТ 28147-89,
блочный шифрAuthors
| Otpuschennikov I. V. | Institute of Dynamics of Systems and Control Theory V.M. Matrosov SB RAS | otilya@yandex.ru |
| Semenov A. A. | Institute of Dynamics of Systems and Control Theory V.M. Matrosov SB RAS | biclop.rambler@yandex.ru |
| Zaikin O. S. | Institute of Dynamics of Systems and Control Theory V.M. Matrosov SB RAS | zaikin.icc@gmail.com |
Всего: 3
References
Kochemazov S. and Zaikin O. ALIAS: A modular tool for finding backdoors for SAT // Proc. SAT Conf. 2018. (to be published)
Yeo S., Li Z., Khoo K., and Low Y. An enhanced binary characteristic set algorithm and its applications to algebraic cryptanalysis // LNCS. 2017. V. 10355. P. 518-536.
Заикин О. С., Семенов А. А. Применение метода Монте-Карло к прогнозированию параллельного времени решения проблемы булевой выполнимости // Вычислительные методы и программирование. 2014. Т. 15. С. 22-35.
Massacci F. and Marraro L. Logical cryptanalysis as a SAT problem // J. Automated Reasoning. 2000. V. 24(1/2). P. 165-203.
Bard G. V. Algebraic Cryptanalysis. Springer, 2009.
Courtois N. T., Gawinecki J. A, and Song G. Contradiction immunity and guess-then-determine attacks on GOST // Tatra Mountains Math. Publ. 2012. V.53(1). P. 2-13.
Semenov A., Zaikin O., Otpuschennikov I., et al. On cryptographic attacks using backdoors for SAT // Proc. AAAI Conf. 2018. P. 6641-6648.
Semenov A. and Zaikin O. Algorithm for finding partitionings of hard variants of Boolean satisfiability problem with application to inversion of some cryptographic functions // SpringerPlus. 2016. V.5(1). P. 1-16.
Otpuschennikov I., Semenov A., Gribanova I., et al. Encoding cryptographic functions to SAT using Transalg system // Frontiers in Artificial Intelligence and Applications. 2016. V. 285. P. 1594-1595.
Отпущенников И.В., Семенов А. А. Технология трансляции комбинаторных проблем в булевы уравнения // Прикладная дискретная математика. 2011. №1. С. 96-115.
Biere A., Heule M., van Maaren H., and Walsh T. (eds.) Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications. V. 185. IOS Press, 2009.
