D. A. Sofronova, K. V. Kalgin, “A compact translator of algorithms into Boolean formulas for use in cryptanalysis”, Prikl. Diskr. Mat. Suppl., 2020, Issue 13,Pages <nobr>135

This article is cited in 1 paper

Computational methods in discrete mathematics

A compact translator of algorithms into Boolean formulas for use in cryptanalysis

D. A. Sofronova^ab, K. V. Kalgin^acd

^a Novosibirsk State University
^b JetBrains Research
^c Institute of Computational Mathematics and Mathematical Geophysics of Siberian Branch of Russian Academy of Sciences, Novosibirsk
^d Sobolev Institute of Mathematics, Siberian Branch of the Russian Academy of Sciences, Novosibirsk

Abstract: 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.

Keywords: cryptanalysis, SAT-solver, guess-and-determine attack.

UDC: 519.7

DOI: 10.17223/2226308X/13/40