DPLL-подобный решатель задачи выполнимости над системой уравнений в АНФ

doi:10.17223/2226308X/14/44

Эндаумент фонд ТГУ!
Впиши своё имя в историю университета
- Сделать пожертвование -

Add to "Quick Collection"

Description	Size	Format
DPLL-подобный решатель задачи выполнимости над системой уравнений в АНФ	123 KB	Adobe Acrobat PDF	Read	Download
DOI Доступ к ресурсу на сайте издателя			10.17223/2226308X/14/44

#криптоанализ

#потоковые шифры

#SAT-решатели

#алгебраическая нормальная форма

Title: DPLL-подобный решатель задачи выполнимости над системой уравнений в АНФ
Creator: Ткачев, Александр Витальевич
|
Калгин, Константин Викторович
Date: 2021
DOI: 10.17223/2226308X/14/44
Description: Описаны 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.

Relationships: Show Relationship Browser for this Object
collection(s): Журналы ТГУ
Identifier: смотреть в электронном каталоге НБ ТГУ
Type: статьи в журналах
Source: Прикладная дискретная математика. Приложение. 2021. № 14. С. 187-190
Language: rus

Created: 14-10-2021

1011 Visitors

814 Hits

213 Downloads

Журналы ТГУ DPLL-подобный решатель задачи выполнимости над системой уравнений в АНФ