Применение SAT-решателей к задаче поиска векторных булевых функций с требуемыми криптографическими свойствами

Представлен подход к решению задачи поиска почти совершенно нелинейной (APN) функции, основанный на её сведении к классической задаче выполнимости и использовании SAT-решателей. Описано построение формул, определяющих APN-функцию. Введены два представления функции: разреженное и плотное, в которых описана задача поиска взаимно однозначной векторной булевой функции и APN-функции. Также в работе представлен новый подход к решению задачи построения векторных булевых APN-функций, обладающих дополнительными свойствами. В основе подхода лежит идея представления неизвестной векторной булевой функции в виде суммы известной APN-функции и двух неизвестных булевых функций: $\mathbf{G} = \mathbf{F}\oplus \mathbf{c}\cdot g_1 \oplus \mathbf{d}\cdot g_2$, где $\mathbf{F}$  — известная APN-функция. Показано, что для функций от $n=6,7$ переменных такой подход имеет большую эффективность в сравнении с прямым построением APN-функции при помощи SAT. Как итог, описанным в работе методом удалось показать отсутствие кубических APN-функций от 7 переменных, представимых в виде описанной выше суммы. Табл. 3, библиогр. 21.