Generating additional constraints in algebraic cryptanalysis using sat oracles | Applied Discrete Mathematics. Supplement. 2021. № 14. DOI: 10.17223/2226308X/14/23

Generating additional constraints in algebraic cryptanalysis using sat oracles

We describe a new technique aimed to generate new constraints which augment with the original set of constraints for a problem of algebraic cryptanalysis. In case the original problem is reduced to a system of Multivariate Quadratic equations over GF(2), the generated constraints can be in the form of linear equations over two-element field. If the considered problem is reduced to SAT, then new constraints are in the form of logic equivalences, anti-equivalences or unit resolvents. In both cases we demonstrate that new constraints generated by the proposed technique can decrease the complexity estimation of attacks on considered functions.

Download file

Counter downloads: 26

Keywords

SAT oracle, MQ systems of equations over GF(2), Boolean satisfiability problem (SAT), algebraic cryptanalysis

Authors

Name	Organization	E-mail
Semenov A. A.	Institute for System Dynamics and Control Theory V.M. Matrosov SB RAS	biclop.rambler@yandex.ru
Antonov K. V.	National Research Nuclear University MEPhI	aknitr@mail.ru
Gribanova I. A.	Institute for System Dynamics and Control Theory V.M. Matrosov SB RAS	the42dimension@gmail.com

Всего: 3

References

Gribanova I. and Semenov A. Parallel guess-and-determine preimage attack with realistic complexity estimation for MD4-40 cryptographic hash function // Материалы конф. «Параллельные вычислительные технологии (ПаВТ) 2019» (Калининград, 2-4 апреля 2019). C. 8-18.

Gribanova I. and Semenov A. Using automatic generation of relaxation constraints to improve the preimage attack on 39-step MD4 // Proc. 41st Intern. Convention Inform. Commun. Technol. Electr. Microelectr. (MIPRO). IEEE, 2018. P. 1174-1179.

Антонов К. В., Семёнов А. А. Применение метаэвристических алгоритмов псевдобуле-вой оптимизации к поиску линеаризующих множеств в криптоанализе криптографических генераторов // Материалы 6-й Междунар. школы-семинара «Синтаксис и семантика логических систем». Иркутск: ИГУ, 2019. С. 13-18.

Beaulieu R., Shors D., Smith J., et al. The Simon and Speck lightweight block ciphers // Proc. 52nd Ann. Design Automation Conf. New York, USA, 2015. P. 175:1-175:6.

ЦКП Иркутский суперкомпьютерный центр СО РАН. http://hpc.icc.ru.

Грибанова И. А., Семёнов А. А. Об аргументации отсутствия свойств случайного оракула у некоторых криптографических хеш-функций // Прикладная дискретная математика. Приложение. 2019. №12. С. 95-98.

Антонов К.В., Семёнов А.А. Применение SAT-оракулов для генерации дополнительных линейных ограничений в задачах криптоанализа некоторых легковесных шифров. Прикладная дискретная математика. Приложение. 2020. №13. С. 114-119.

Семёнов А. А., Антонов К. В., Отпущенников И. В. Поиск линеаризующих множеств в алгебраическом криптоанализе как задача псевдобулевой оптимизации // Прикладная дискретная математика. Приложение. 2019. № 12. С. 130-134.

Яблонский С. В. Введение в дискретную математику. М.: Наука, 1986.

Dowling W. F. and Gallier J. H. Linear-time algorithms for testing the satisfiability of propositional horn formulae // J. Log. Program. 1984. No. 1(3). P. 267-284.

Biere A. The AIGER And-Inverter Graph (AIG) format version 20071012. Tech. Report 07/1. Institute for Formal Models and Verification, Johannes Kepler University. 2007.

Kipnis A. and Shamir A. Cryptanalysis of the HFE public key cryptosystem by relinearization // LNCS. 1999. V. 1666. P. 19-30.

Semenov A., Otpuschennikov I., Gribanova I., et al. Translation of algorithmic descriptions of discrete functions to SAT with application to cryptanalysis problems // Log. Methods Comput. Sci. 2020. V. 16. Iss. 1. P. 29:1-29:42.

Калгин К. В., Софронова Д.А. Компактный транслятор алгоритмов в булевы формулы для применения в криптоанализе // Прикладная дискретная математика. Приложение. 2020. №13. С. 135-136.

Otpuschennikov I., Semenov A., Gribanova I., et al. Encoding cryptographic functions to SAT using Transalg system // Frontiers Artificial Intell. Appl. 2016. V. 285. P. 1594-1595.

Erkok L., Carlsson M., and Wick A. Hardware/software co-verification of cryptographic algorithms using Cryptol // Proc. 9th Intern. Conf. FMCAD. IEEE, 2009. P. 188-191.

Clarke E., Kroening D., and Lerda F. A tool for checking ANSI-C programs // LNCS. 2004. V. 2988. P. 168-176.

Левин Л. А. Универсальные задачи перебора // Проблемы передачи информации. 1973. Т. 9. №3. С. 115-116.

Bard G. Algebraic Cryptanalysis. Springer, 2009.

Cook S. A. The complexity of theorem-proving procedures // Proc. 3rd Ann. ACM Symp. Theory Comput. 1971. P. 151-158.