Geodesic
DPLL-like satisfiability problem solver over the system of ANF equations
Prikladnaya Diskretnaya Matematika. Supplement, no. 14 (2021), pp. 187-190.

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

In the paper, we describe SAT solver for problems in ANF and show how typical SAT techniques can be implemented to work with ANF. This solver is compared to a number of classic SAT solvers on cryptanalysis problems (such as “guess-and-determine” attack on Grain stream cipher). The solver uses such techniques as Propagation of Constants, Propagation of Synonyms, Watched Monomials (2WM), equations simplification and variable selection order. Our experiments show that for “init=no” case this ANF solver works similarly to typical CNF SAT solvers, but in the “init=yes” case the latter fail where the ANF solver finds a solution. Based on the data we've gathered we make a conclusion that it is impractical to use SAT solvers to attack Grain in “init=no” case. For the future research, we want to make experiments with more ciphers and solvers, explore why modern CNF SAT solvers work slower than the ANF solver and adapt more SAT techniques into our implementation.
Keywords: SAT solver, ANF, stream ciphers.
Mots-clés : cryptanalysis 
@article{PDMA_2021_14_a44,
     author = {A. V. Tkachev and K. V. Kalgin},
     title = {DPLL-like satisfiability problem solver over the system of {ANF} equations},
     journal = {Prikladnaya Diskretnaya Matematika. Supplement},
     pages = {187--190},
     publisher = {mathdoc},
     number = {14},
     year = {2021},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/PDMA_2021_14_a44/}
}
TY  - JOUR
AU  - A. V. Tkachev
AU  - K. V. Kalgin
TI  - DPLL-like satisfiability problem solver over the system of ANF equations
JO  - Prikladnaya Diskretnaya Matematika. Supplement
PY  - 2021
SP  - 187
EP  - 190
IS  - 14
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/PDMA_2021_14_a44/
LA  - ru
ID  - PDMA_2021_14_a44
ER  - 
%0 Journal Article
%A A. V. Tkachev
%A K. V. Kalgin
%T DPLL-like satisfiability problem solver over the system of ANF equations
%J Prikladnaya Diskretnaya Matematika. Supplement
%D 2021
%P 187-190
%N 14
%I mathdoc
%U http://geodesic.mathdoc.fr/item/PDMA_2021_14_a44/
%G ru
%F PDMA_2021_14_a44
A. V. Tkachev; K. V. Kalgin. DPLL-like satisfiability problem solver over the system of ANF equations. Prikladnaya Diskretnaya Matematika. Supplement, no. 14 (2021), pp. 187-190. http://geodesic.mathdoc.fr/item/PDMA_2021_14_a44/

[1] Cook S., “The complexity of theorem-proving procedures”, 3rd Ann. ACM Symp. Theory Comput., 1971, 151–158 | Zbl

[2] Choo D., Soos M., Chai K. M. A., Meel K. S., “BOSPHORUS: Bridging ANF and CNF solvers”, Proc. DATE Conf. Exhibition, 2019, 468–473

[3] Katebi H., Sakallah K., Silva J., “Empirical study of the anatomy of modern SAT Solvers”, LNCS, 6695, 2011, 343–356 | MR | Zbl

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

[5] Hell M., Johansson T., Meier W., “Grain: A stream cipher for constrained environments”, Intern. J. Wireless Mobile Comput., 2007, no. 2, 86–93 | DOI

[6] Yeo S., Le D. P., Khoo K., “Improved algebraic attacks on lightweight block ciphers”, J. Cryptogr. Eng., 2011, no. 11, 1–19

[7] Semenov A. A., Zaikin O. S., “Algorithm for finding partitionings of hard variants of Boolean satisfiability problem with application to inversion of some cryptographic functions”, SpringerPlus, 2016, 554, 16 pp. | DOI