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

K. V. Antonov ; A. A. Semenov

Prikladnaya Diskretnaya Matematika. Supplement, no. 13 (2020), pp. 114-119.

Résumé

In the paper, we propose a new technique that is aimed at algebraic cryptanalysis problems. Using this technique we construct additional linear equations over $\rm{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.

Détail

Keywords: linearizing sets, guess-and-determine attack, quadratic systems over $\rm{GF}(2)$, pseudo-Boolean optimization
Mots-clés : Trivium.

Bibliographie

[1] Semenov A. A., Antonov K. V., Otpuschennikov I. V., “Poisk linearizuyuschikh mnozhestv v algebraicheskom kriptoanalize kak zadacha psevdobulevoi optimizatsii”, Prikladnaya diskretnaya matematika. Prilozhenie, 2019, no. 12, 130–134

[2] Biere A., “Bounded Model Checking”, Handbook of Satisfiability, IOS Press, Amsterdam, 2009, 457–481

[3] Otpuschennikov I. V., Semenov A. A., “Tekhnologiya translyatsii kombinatornykh problem v bulevy uravneniya”, Prikladnaya diskretnaya matematika, 2011, no. 1(11), 96–115

[4] 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, 285, 2016, 1594–1595

[5] Tseitin G. S., “O slozhnosti vyvoda v ischislenii vyskazyvanii”, Zapiski nauchnykh seminarov LOMI AN SSSR, 8, 1968, 234–259 | Zbl

[6] 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., 16:1 (2020), 29:1–29:42 | MR | Zbl

[7] Chen Ch., Li R., Matematicheskaya logika i avtomaticheskoe dokazatelstvo teorem, Nauka, M., 1983

[8] Agibalov G. P., “Logicheskie uravneniya v kriptoanalize generatorov klyuchevogo potoka”, Vestnik Tomskogo gosuniversiteta. Prilozhenie, 2003, no. 6, 31–41

[9] Semenov A., Zaikin O., Otpuschennikov I., et al., “On cryptographic attacks using backdoors for SAT”, Proc. 32nd AAAI Conf., 2018, 6641–6648

[10] Boros E., Hammer P., “Pseudo-Boolean optimization”, Discr. Appl. Math., 123:1–3 (2002), 155–225 | DOI | MR | Zbl

[11] Glover F., Laguna M., Tabu Search, Kluwer Academic Publishers, Norwell, 1997

[12] Antonov K. V., Semenov A. A., “Primenenie metaevristicheskikh algoritmov psevdobulevoi optimizatsii k poisku linearizuyuschikh mnozhestv v kriptoanalize kriptograficheskikh generatorov”, Materialy 6-i Mezhdunar. shkoly-seminara «Sintaksis i semantika logicheskikh sistem», IGU, Irkutsk, 2019, 13–18

[13] Pavlenko A., Semenov A., Ulyantsev V., “Evolutionary computation techniques for constructing SAT-based attacks in algebraic cryptanalysis”, LNCS, 11454, 2019, 237–253

[14] De Canniere C., “Trivium: A stream cipher construction inspired by block cipher design principles”, LNCS, 4176, 2006, 171–186 | Zbl

[15] Dinur I., Shamir A., “Cube attacks on tweakable black box polynomials”, LNCS, 5479, 2009, 278–299 | MR | Zbl

[16] TsKP Irkutskii superkompyuternyi tsentr SO RAN, http://hpc.icc.ru