Применение SAT-решателей для построения булевых функций с заданными криптографическими свойствами | ПДМ. Приложение. 2020. № 13. DOI: 10.17223/2226308X/13/38

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

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

Construction of cryptographic boolean functions using SAT-solvers.pdf В настоящее время SAT-решатели используются для решения криптографических задач разного типа. Например, проведён криптоанализ асимметричной криптосистемы RSA [1], в результате которого удалось факторизовать числа до 417 бит; выполнен криптоанализ шифра Trivium и его модификаций [2]. В [3] представлена гомоморфная криптосистема с открытым ключом, основанная на SAT-задаче. С помощью SAT-решателей успешно проверяется обратимость векторных булевых функций [4]. В данной работе предлагается использование SAT-решателей в задачах построения криптографических булевых функций и проверки эквивалентности двух булевых функций. Для получения набора булевых формул использованы следующие понятия и свойства. Определение 1. Векторная булева функция F : Zn ^ Zn называется взаимно однозначной, если она инъективна и сюръективна, то есть одновременно выполняются следующие условия: 1) Vx' Е Zn Vx" Е Zn (x' _ x" ^ F(x') _ F(x")); 2) Vy Е Zn 3x Е Zn 2F(x) _ y). Определение 2. Векторная булева функция F : Zn ^ Zn является дифференциально 5-равномерной, если для любого ненулевого a Е Zn и произвольного b Е Zn уравнение F(x) ф F(x ф а) _ b имеет не более 5 решений. Условия, фигурирующие в определениях, представляются в виде КНФ и подаются на вход SAT-решателя. В результате его работы происходит означивание переменных таким образом, чтобы формулы были истинными, а следовательно, условия выполнялись. Векторные булевы функции были закодированы в двух представлениях: 1) В разреженном представлении используется 22n переменных fx y, из которых 2n равны 1, остальные равны 0: fx,y _ 1 ^^ F(x) _ y, где x,y Е Zn. 2) В плотном представлении используется n2n переменных fbx,k: fbx,k _ 1 ^^ Fk (x) _ 1, где F (x) _ (Fo(x),F2(x),...,Fn-i(x)), Fk : Zn ^ Z2', k _0,...,n - 1; x Е Z™ Для записи условий на переменные fx,y и f bx,k понадобятся следующие вспомогательные переменные: - f bqx,y,k _ 1 ^^ f bx,k _ f by,k, где k _ 0,..., n - 1; x, y Е Zn; - dx,a,b _ 1 ^^ F(x) ф F(x ф a) _ b, где x, a, b Е Zn; - dex,y,a _ 1 ^^ F(x) ф F(x ф a) _ F(y) ф F(y ф a), где x, y, a Е Zn; - dbqx,y,a,k _ 1 ^^ f bqx,x®a,k _ fbqy,y®a,k, где k _ 0,..., n - 1, x, y, a Е Zn. В КНФ эти зависимости записываются следующим образом: SoPD(fb, fbq) _ Л (fbqx,y,k V fbx,k V fby,k) Л (fbqx,y,k V fbx,k V fby,k)Л x,y,k Л(fbqx,y,k V fbx,k V fby,k) Л (fbqx,y,k V fbx,k V fby,k), SpDen(f, fb) ^ (fx,y V fbx,k) Л (fx,y V fbxOo V... V fbx^ 1); x,y,k DerS(f, d) ^ Д (fx,z V fx®a,z®b V dx,a,b ) Л (fx,z V fx®a,z®b V dx;a,b)Л b,a,z,x Л(fx,z V fx®a,z®b V dx,a,b ) Л (fx,z V fx®a,z®b V dx,a,b); SoPEqD(/bq,dbq) = Д (dbq k V /bq x,x®a,k v /bqy,y®a, k )л a,x,y,k л(dЪqx,y,a,k V /b5x,x®a,k V /b5y,y®a,k) Л (db5x,y,a,k V /b5x,x®a,k V /b5y,y®a,k)Л ^dbqx,y,a,k V /b?x,x®a,k V /b?y,y®a,k); k = 0,..., n - 1; x, y, z, a, b E Z: n. Свойства из определений 1 и 2 можно записать следующими формулами. Теорема 1. Переменные /x,y задают функцию F : Zn ^ Zn тогда и только тогда, когда следующая формула является истинной: FS(/)= Л (Л /x,y V /x,y) Л Д ( V /x,y). xezj y',y"ezn xezj yezj y'

Ключевые слова

SAT-решатели, криптография, булевы функции, SAT-solvers, cryptography, Boolean functions

Авторы

ФИООрганизацияДополнительноE-mail
Доронин Артемий ЕвгеньевичНовосибирский государственный университетстудентartem96dor@gmail.com
Калгин Константин ВикторовичИнститут вычислительной математики и математической геофизики СО РАН; Институт математики им. С. Л. Соболева СО РАН; Новосибирский государственный университеткандидат физико-математических наук, научный сотрудник; младший научный сотрудник; старший преподаватель кафедры параллельных вычислений ФИТkalginkv@gmail.com
Всего: 2

Ссылки

Огородников Ю. Ю. Комбинированная атака на алгоритм RSA с использованием SAT-подхода // Динамика систем, механизмов и машин. Омск: ОмГТУ, 2016. С. 276-284.
Заикин О. С., Отпущенников И. В., Семёнов А. А. Оценки стойкости шифров семейства Trivium к криптоанализу на основе алгоритмов решения проблемы булевой выполнимости // Прикладная дискретная математика. Приложение. 2016. №9. С. 46-48.
Schmittner S. E. A SAT-based Public Key Cryptography Scheme. IACR Cryptol. ePrint Arch. 2015. https://eprint.iacr.org/2015/771.pdf.
Wille R., Lye A., and Niemann P. Checking reversibility of Boolean functions // LNCS. 2016. V. 9720. P. 322-337.
 Применение SAT-решателей для построения булевых функций с заданными криптографическими свойствами | ПДМ. Приложение. 2020. № 13. DOI: 10.17223/2226308X/13/38

Применение SAT-решателей для построения булевых функций с заданными криптографическими свойствами | ПДМ. Приложение. 2020. № 13. DOI: 10.17223/2226308X/13/38