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'

Скачать электронную версию публикации