Geodesic
Propositional encoding of direct and inverse round transformations in attacks on some block ciphers
Prikladnaya Diskretnaya Matematika. Supplement, no. 11 (2018), pp. 76-79.

Voir la notice de l'article provenant de la source Math-Net.Ru

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 28147-89). 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: block cipher, GOST 28147-89, PRESENT, Boolean satisfiability problem.
Mots-clés : DES 
@article{PDMA_2018_11_a23,
     author = {I. V. Otpuschennikov and A. A. Semenov and O. S. Zaikin},
     title = {Propositional encoding of direct and inverse round transformations in attacks on some block ciphers},
     journal = {Prikladnaya Diskretnaya Matematika. Supplement},
     pages = {76--79},
     publisher = {mathdoc},
     number = {11},
     year = {2018},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/PDMA_2018_11_a23/}
}
TY  - JOUR
AU  - I. V. Otpuschennikov
AU  - A. A. Semenov
AU  - O. S. Zaikin
TI  - Propositional encoding of direct and inverse round transformations in attacks on some block ciphers
JO  - Prikladnaya Diskretnaya Matematika. Supplement
PY  - 2018
SP  - 76
EP  - 79
IS  - 11
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/PDMA_2018_11_a23/
LA  - ru
ID  - PDMA_2018_11_a23
ER  - 
%0 Journal Article
%A I. V. Otpuschennikov
%A A. A. Semenov
%A O. S. Zaikin
%T Propositional encoding of direct and inverse round transformations in attacks on some block ciphers
%J Prikladnaya Diskretnaya Matematika. Supplement
%D 2018
%P 76-79
%N 11
%I mathdoc
%U http://geodesic.mathdoc.fr/item/PDMA_2018_11_a23/
%G ru
%F PDMA_2018_11_a23
I. V. Otpuschennikov; A. A. Semenov; O. S. Zaikin. Propositional encoding of direct and inverse round transformations in attacks on some block ciphers. Prikladnaya Diskretnaya Matematika. Supplement, no. 11 (2018), pp. 76-79. http://geodesic.mathdoc.fr/item/PDMA_2018_11_a23/

[1] Biere A., Heule M., van Maaren H., Walsh T. (eds.), Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, 185, IOS Press, 2009 | Zbl

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

[3] Otpuschennikov I., Semenov A., Gribanova I., et al., “Encoding cryptographic functions to SAT using Transalg system”, Frontiers in Artificial Intelligence and Applications, 285 (2016), 1594–1595

[4] Massacci F., Marraro L., “Logical cryptanalysis as a SAT problem”, J. Automated Reasoning, 24:1/2 (2000), 165–203 | DOI | MR | Zbl

[5] Bard G. V., Algebraic Cryptanalysis, Springer, 2009 | MR | Zbl

[6] Courtois N. T., Gawinecki J. A., Song G., “Contradiction immunity and guess-then-determine attacks on GOST”, Tatra Mountains Math. Publ., 53:1 (2012), 2–13 | MR

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

[8] Semenov A., Zaikin O., “Algorithm for finding partitionings of hard variants of Boolean satisfiability problem with application to inversion of some cryptographic functions”, SpringerPlus, 5:1 (2016), 1–16 | DOI

[9] Zaikin O. S., Semenov A. A., “Primenenie metoda Monte-Karlo k prognozirovaniyu parallelnogo vremeni resheniya problemy bulevoi vypolnimosti”, Vychislitelnye metody i programmirovanie, 15:1 (2014), 22–35

[10] Kochemazov S., Zaikin O., “ALIAS: A modular tool for finding backdoors for SAT”, Proc. SAT Conf., 2018 (to appear)

[11] Yeo S., Li Z., Khoo K., Low Y., “An enhanced binary characteristic set algorithm and its applications to algebraic cryptanalysis”, LNCS, 10355, 2017, 518–536 | MR