E-catalog        

Библиогр.: 7 назв.

Описаны SAT-решатель, использующий системы булевых уравнений в алгебраической нормальной форме (АНФ) для внутреннего представления задачи, и особенности реализации типичных для SAT-решателей методик для работы с таким представлением. Приводится сравнение данного решателя с рядом классических SAT-решателей при решении некоторых задач криптоанализа (как, например, атака «guess-and-determine» на потоковый шифр Grain). 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.