Application of sat oracles for generation of additional linear constraints in cryptanalysis of some lightweight ciphers | Applied Discrete Mathematics. Supplement. 2020. № 13. DOI: 10.17223/2226308X/13/34

Application of sat oracles for generation of additional linear constraints in cryptanalysis of some lightweight ciphers

In the paper, we propose a new technique that is aimed at algebraic cryptanalysis problems. Using this technique we construct additional linear equations over GF(2) which augment the system of algebraic equations presenting the cryptanalysis of the considered cipher. We use a SAT solver to generate such new linear equations. It was shown that the proposed technique allows one to increase the efficiency of guess-and-determine attacks which are based on the linearization sets. Effectiveness of the proposed technique was confirmed by computational experiments in which we considered the cryptanalysis of some variants of well-known stream cipher Trivium with a decreased number of steps in the initialization phase.

Download file

Counter downloads: 93

Keywords

линеаризующие множества, атаки из класса «угадывай и определяй», квадратичные системы над GF(2), псевдобулева оптимизация, Trivium, linearizing sets, guess-and-determine attack, quadratic systems over GF(2), pseudo-Boolean optimization, Trivium

Authors

Name	Organization	E-mail
Antonov K. V.	IMIT ISU	aknitr@mail.ru
Semenov A. A.	V.M. Matrosov Institute for System Dynamics and Control Theory SB RAS	biclop.rambler@yandex.ru

Всего: 2

References

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

Biere A. Bounded Model Checking // Handbook of Satisfiability. Amsterdam: IOS Press, 2009. P. 457-481.

Отпущенников И. В., Семёнов А. А. Технология трансляции комбинаторных проблем в булевы уравнения // Прикладная дискретная математика. 2011. №1 (11). С. 96-115.

Otpuschennikov I., Semenov A., Gribanova I., et al. Encoding cryptographic functions to SAT using TRANSALG system // Proc. 22nd European Conf. ECAI 2016. Frontiers in Artificial Intelligence and Applications. 2016. V.285. P. 1594-1595.

Цейтин Г. С. О сложности вывода в исчислении высказываний // Записки научных семинаров ЛОМИ АН СССР. 1968. Т. 8. С. 234-259.

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.

Чень Ч., Ли Р. Математическая логика и автоматическое доказательство теорем. М.: Наука, 1983.

Агибалов Г. П. Логические уравнения в криптоанализе генераторов ключевого потока // Вестник Томского госуниверситета. Приложение. 2003. №6. С. 31-41.

Semenov A., Zaikin O., Otpuschennikov I., et al. On cryptographic attacks using backdoors for SAT // Proc. 32nd AAAI Conf. 2018. P. 6641-6648.

Boros E. and Hammer P. Pseudo-Boolean optimization // Discr. Appl. Math. 2002. V. 123. Iss. 1-3. P. 155-225.

Glover F. and Laguna M. Tabu Search. Norwell: Kluwer Academic Publishers, 1997.

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

Pavlenko A., Semenov A., and Ulyantsev V. Evolutionary computation techniques for constructing SAT-based attacks in algebraic cryptanalysis // LNCS. 2019. V. 11454. P. 237-253.

De Canniere C. Trivium: A stream cipher construction inspired by block cipher design principles // LNCS. 2006. V.4176. P. 171-186.

Dinur I. and Shamir A. Cube attacks on tweakable black box polynomials // LNCS. 2009. V. 5479. P. 278-299.

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