A Compact translator of algorithms into boolean formulas for use in cryptanalysis | Applied Discrete Mathematics. Supplement. 2020. № 13. DOI: 10.17223/2226308X/13/40

A Compact translator of algorithms into boolean formulas for use in cryptanalysis

The program for converting the description of the cryptographic task to CNF is presented. A SAT solver establishes the truth of the formula and finds the values of the variables after that. Features of this development are universality, a small code size (300 lines of C++), easily modifiable and extensible implementation.

Download file

Counter downloads: 107

Keywords

криптоанализ, SAT-решатель, атака «угадай-и-вычисли», cryptanalysis, SAT-solver, guess-and-determine attack

Authors

Name	Organization	E-mail
Sofronova D.A.	Novosibirsk State University; JetBrains Research Crypto Lab	d.sofronova1@g.nsu.ru
Kalgin K.V.	Institute of Computational Mathematics and Mathematical Geophysics SB RAS; S. L. Sobolev Institute of Mathematics SB RAS; Novosibirsk State University	kalginkv@gmail.com

Всего: 2

References

Otpuschennikov I., Semenov A., Gribanova I., et al. Encoding cryptographic functions to SAT using TRANSALG system // Proc. ECAI'16. IOS Press, 2016. P. 1594-1595.

Biere A., Heule M., Maaren H., and Walsh T. Handbook of Satisfiability. IOS Press, 2009. 966 p.

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.

Soos M., Nohl K., and Castelluccia C. Extending SAT solvers to cryptographic problems // LNCS. 2009. V. 5584. P. 244-257.

Soos M. Grain of salt - an automated way to test stream ciphers through SAT solvers // Tools. 2010. V. 10. P. 131-144.