Guess-and-determine attacks and automatic methods for their construction
In the paper, a brief review of approaches to construction of cryptographic attacks from the class "guess-and-determine" is presented. The main focus is done on recent works, in which some automatic methods for constructing SAT-based guess-and-determine attacks were proposed. With that purpose, the problems of constructing corresponding attacks are stated as optimization problems for specific evaluation functions over Boolean hypercube. To solve the latter, the meta-heuristic algorithms widely employed in discrete optimization are used. In the mentioned papers, two types of evaluation functions were formally introduced. Those can be viewed as concretizations of the notions of "UNSAT-immunity" and "SAT-immunity" informally introduced by N. Courtois in 2012. Within the report, several examples of constructing guess-and-determine attacks of the mentioned type on a number of block and stream ciphering algorithms will be given.
Download file
Counter downloads: 166
Keywords
SAT, Boolean satisfiability problem, SAT, guess-and-determine attacks, проблема булевой выполнимости, атаки из класса «угадывай и определяй»Authors
| Name | Organization | |
| Semenov A. A. | Institute of Dynamics of Systems and Control Theory V.M. Matrosov SB RAS | biclop.rambler@yandex.ru |
References
Courtois N. T. Algebraic Complexity Reduction and Cryptanalysis of GOST. Preprint. 20102013. https://eprint.iacr.org/2011/626.pdf
Semenov A., Zaikin O., Otpuschennikov I., et al. On cryptographic attacks using backdoors for SAT // The Thirty-Second AAAI Conf. on Artificial Intelligence, AAAI'2018. New Orleans, Louisiana, USA, 2018. P. 6641-6648.
Williams R., Gomes C. P., and Selman B. Backdoors to typical case complexity // Proc. of IJCAI. Acapulco, Mexico, 2003. P. 1173-1178.
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. No. 1. P. 1-16.
Semenov A. and Zaikin O. Using Monte Carlo method for searching partitionings of hard variants of Boolean satisfiability problem // LNCS. 2015. V.9251. P. 222-230.
Courtois N. T., Gawinecki J. A, and Song G. Contradiction immunity and guess-then-determine attacks on GOST // Tatra Mountains Mathematical Publications. 2012. V. 53. No. 1. P. 2-13.
Bard G. Algebraic Cryptanalysis. Springer, 2009.
Semenov A., Zaikin O., Bespalov D., and Posypkin M. Parallel logical cryptanalysis of the generator A5/1 in BNB-Grid system // LNCS. 2011. V.6873. P. 473-483.
Посыпкин М. А., Заикин О. С., Беспалов Д. В., Семенов А. А. Решение задач криптоанализа поточных шифров в распределенных вычислительных средах // Труды ИСА РАН. 2009. №46. С. 119-137.
De D., Kumarasubramanian A, and Venkatesan R. Inversion attacks on secure hash functions using SAT solvers // LNCS. 2007. V.4501. P. 377-382.
Courtois N. and Pieprzyk J. Cryptanalysis of block ciphers with overdefined systems of equations // LNCS. 2003. V.2501. P. 267-287.
Marques-Silva J., Lynce I., and Malik S. CDCL Solvers. Handbook of Satisfiability. IOS Press, 2009. P. 131-153.
Mironov I. and Zhang L. Applications of SAT solvers to cryptanalysis of hash functions // LNCS. 2006. V. 4121. P. 102-115.
Тимошевская Н. Е. Задачи о кратчайшем линеаризационном множестве // Вестник Томского государственного университета. Приложение. 2005. №4. С. 79-83.
Golic J. Dj. Cryptanalysis of alleged A5 stream cipher // LNCS. 1997. V. 1233. P. 239-255.
Агибалов Г. П. Логические уравнения в криптоанализе генераторов ключевого потока // Вестник Томского государственного университета. Приложение. 2003. №6. С. 31-41.
Bulavintsev V., Semenov A., Zaikin O., and Kochemazov S. A bitslice implementation of Anderson's attack on A5/1 // Open Eng. 2018. V.8. P. 7-16.
Gendrullis T., Novotny M., and Rupp A. A real-world attack breaking A5/1 within hours // LNCS. 2008. V. 5154. P. 266-282.
Cook S. A. The complexity of theorem-proving procedures // Third Ann. ACM Symp. on Theory of Computing. 1971. P. 151-159.
Anderson R. A5 (Was: Hacking Digital Phones). Newsgroup Communication. 1994. http: //yarchive.net/phone/gsmcipher.html
Яблонский С. В. Введение в дискретную математику. М.: Наука, 1986.
Dowling W. and Gallier J. Linear-time algorithms for testing the satisfiability of propositional horn formulae // J. Logic Programming. 1984. V. 7. P. 267-284.
Цейтин Г. С. О сложности вывода в исчислении высказываний // Записки научных семинаров ЛОМИ АН СССР. 1968. Т. 8. С. 234-259.
