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

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

Описывается новая техника, применимая к задачам алгебраического криптоанализа. В рамках предлагаемой техники строятся линейные уравнения над полем из двух элементов, которыми дополняется система алгебраических уравнений, представляющая криптоанализ рассматриваемого шифра. Для генерации новых линейных уравнений используется SAT-решатель. Показано, что применение этой техники позволяет повысить эффективность атак из класса «угадывай и определяй», основанных на понятии линеаризующего множества. Эффективность предложенной техники подтверждается вычислительными экспериментами, проведёнными для ряда ослабленных по числу шагов инициализации версий известного поточного шифра Trivium.

Application of sat oracles for generation of additional linear constraints in cryptanalysis of some lightweight ciphers.pdf Настоящую работу можно рассматривать как прямое продолжение [1]. Приведём краткое описание используемых обозначений, понятий и вспомогательных результатов из [1]. Будем рассматривать задачу обращения (поиска прообразов) всюду определённой дискретной функции f : {0,1}n ^{0,1}m, (1) которая задана некоторой программой (алгоритмом) Mf. Иными словами, зная текст программы Mf и произвольный y Е Range f, требуется найти такой а Е {0,1}n, что f (а) _ y. Известно, что по Mf можно эффективно построить схему из функциональных элементов над базисом {Л, -} (конъюнкция, отрицание), которая задаёт функцию f. Такого рода схемы в символьной верификации называются И-НЕ-графами (And-Inverter Graph или AIG [2]). На практике для построения И-НЕ-графа по конкретному алгоритму Mf можно задействовать специализированные программные средства. Мы использовали для этих целей программный комплекс Transalg [3, 4]. Пусть Gf - И-НЕ-граф, который задаёт функцию (1). В Gf выделены n вершин, не имеющие предшественников (соответствуют аргументу функции f), эти вершины называются входными. Всем остальным вершинам Gf приписаны функциональные элементы из базиса {Л, -}, эти вершины называются внутренними вершинами или узлами. Среди внутренних вершин выделены m вершин, не имеющих потомков, эти вершины соответствуют значению функции f и называются выходными. С входными вершинами Gf связываются булевы переменные, образующие множество X = {x1,... , xn}. С каждой внутренней вершиной g графа Gf связывается булева переменная v, называемая вспомогательной, множество всех вспомогательных переменных обозначается через V. В множестве V выделяется подмножество Y = {y1,...,ym}, образованное переменными, которые приписаны выходным вершинам Gf. По графу Gf, используя преобразования Цейтина [5], можно построить КНФ Cf, которая называется шаблонной (template CNF [6]). Также по графу Gf можно построить систему алгебраических уравнений над GF(2), каждое уравнение которой имеет степень не выше 2. Опишем кратко соответствующую процедуру. Рассматриваем множества переменных X и V. Каждой вершине g с приписанной ей переменной v Е V сопоставим алгебраическое уравнение над полем GF(2). Если g - И-узел, то g имеет двух прямых предшественников в графе Gf. Предположим, что им приписаны переменные u и w. Если g - НЕ-узел, то он имеет в Gf единственного прямого предшественника, которому приписана переменная u. Произвольному g сопоставим уравнение над GF(2) по следующим правилам. Если g - И-узел, то имеем уравнение u Л w 0 v = 0, (2) если g - НЕ-узел, то имеем уравнение u 0 v = 1. (3) Определение 1. Пусть Ef - система, образованная уравнениями вида (2) или (3) по всем узлам графа Gf. Назовём Ef шаблонной системой уравнений над GF(2) для функции (1). Заметим, что Ef образована уравнениями над GF(2) степени не выше 2. Стандартным образом [7, 8] определим для произвольной переменной x Е U, U = X U V, подстановку её значения x = Л Е {0,1} в систему Ef. Иногда в результате подстановки x = Л вид некоторого уравнения может упроститься таким образом, что станет известным значение некоторой переменной x' Е X \\ {x}. В таких случаях будем говорить, что соответствующее значение переменной x' индуцировано подстановкой x = Л. Например, подстановка u =1 в (3) индуцирует значение 0 переменной v. Аналогичным образом определяется произвольная подстановка вида x = Л в шаблонную КНФ Cf. В [6] показано, что подстановка в Cf набора y значений переменных из Y, y Е Range f, даёт выполнимую КНФ Cf (y), из выполняющего набора которой эффективно извлекается такое а Е {0,1}n, что f(а) = y. Рассуждая по аналогии, можно показать, что подстановка y Е Range f в Ef даёт совместную систему уравнений Ef (y) над GF(2) и из произвольного решения Ef (y) можно эффективно извлечь такое а Е {0,1}n, что f (а) = y. Понятие линеаризующего множества сформулировано в [1]. Оно обобщает понятие линеаризационного множества, введённого в [8]. Неформально говоря, линеаризующее множество линеаризует систему вида Ef (y) с некоторой вероятностью, которая может быть существенно меньше 1 , но давать при этом атаку с относительно малой трудоёмкостью. Более точно, линеаризующее множество определяется на базе конструкции, с использованием которой в [9] предложены новые атаки из класса «угадывай и определяй». В соответствии с этой конструкцией с произвольным а, которое выбирается из {0,1}n согласно равномерному распределению, и произвольным B С X связывается набор значений переменных ва (получается в результате выбора соответствующих B компонент из а), а также Ya G Range f, такой что f(а) = Ya. Вероятность линеаризации рв - это доля таких a G {0,1}n, что подстановка пары ва, Ya в систему Ef превращает её в линейную. В [1] задача поиска линеаризующего множества с относительно малой трудоёмкостью соответствующей атаки ставится как проблема оптимизации специальной псевдобулевой функции [10], значения которой вычисляются в результате вероятностного эксперимента. В [1] для этой цели используется алгоритм, основанный на концепции tabu search [11], а в [12] -один вариант генетического алгоритма, описанный в [13]. Как итог, для задачи криптоанализа генератора A5/1 найдены линеаризующие множества, дающие атаки, трудоёмкость которых существенно меньше трудоёмкости известной атаки Р. Андерсона. В настоящей работе описана техника, которая позволяет дополнять системы вида Ef (y) новыми линейными уравнениями, что в ряде случаев позволяет построить существенно более эффективные (в смысле трудоёмкости соответствующих атак) линеаризующие множества. Итак, рассматривается задача обращения функции вида (1). Предположим, что функция f представлена в виде И-НЕ-графа Gf и по Gf построены шаблонная КНФ Cf и шаблонная система уравнений Ef над GF(2). Таким образом, ив Cf, и в Ef фигурируют переменные, образующие множество U = X U V. Рассмотрим произвольный И-узел g в графе Gf. Пусть узлу g приписана переменная v, а прямым предшественникам g - переменные u и w. С узлом g связана булева функция : {0,1}3 ^ {0,1}, заданная формулой u Л w = v. При построении Cf формула u Л w = v приводится к КНФ по таблице Tg (табл. 1). Та б л и ц а 1 Табличное задание функции ^>g u w v У.9 0 0 0 1 0 0 1 0 0 1 0 1 0 1 1 0 1 0 0 1 1 0 1 0 1 1 0 0 1 1 1 1 Обозначим через Sg множество решений связанного с g уравнения u Л w ф v = 0. Очевидно, что Sg образовано всеми теми наборами значений переменных u, w, v, которым в таблице Tg соответствует = 1. С другой стороны, в соответствии с преобразованиями Цейтина при построении Cf в эту КНФ войдут дизъюнкции вида u-01 V w-02 V v-03 по всем таким наборам (о1о2о3) из Tg, на которых = 0. В основе приведённого далее результата лежит следующее наблюдение: оказывается, для целого ряда криптографических функций вида (1) для существенной доли И-узлов g в Gf в множестве Sg существуют такие наборы (о1о2о3), что КНФ u01 Л w02 Л v03 Л Cf невыполнима. С использованием рассуждений из [6] можно показать, что данная ситуация соответствует тому факту, что никакой вход a G {0,1}n не может индуцировать для переменных из множества {u,w,v} значение (о1о2о3). Применительно к системе вида Ef (y) для произвольного y G Range f это означает, что вектор (aia2a3) может быть заведомо исключён из возможных решений данной системы. Может показаться удивительным, но, как правило, на доказательство невыполнимости КНФ вида u01 Л w°2 Л v°3 Л Gf у современного SAT-решателя уходят доли секунды. Таким образом, можно говорить, что такой SAT-решатель выполняет роль оракула, эффективно отсеивающего некоторые наборы из Sg. Основной результат настоящей работы состоит в следующем. Теорема 1. Пусть g - И-узел в И-НЕ-графе Gf, представляющем произвольную функцию f вида (1); Xg - {u,w,v} -множество переменных, связанных с g; Sg - множество решений уравнения u Л w Ф v = 0. Предположим, что для некоторого a = = (aia2a3), a £ Sg, SAT-оракул доказал невыполнимость КНФ u01 Л w°2 Л v°3 Л Gf. Тогда для любого такого a имеет место Sg \\ {a} = Sg n SL(X9), где Sl(x9) -множество решений некоторого линейного уравнения L(Xg) над F(2). Доказательство данной теоремы получается в результате разбора всех возможных случаев исключения a из Sg. Множество Sg приведено в табл. 2. Таблица 2 Множество Sg для И-узла g u w v У.9 0 0 0 1 0 1 0 1 1 0 0 1 1 1 1 1 Важное следствие теоремы 1 состоит в том, что если для И-узла g графа Gf SAT-оракул доказал невыполнимость КНФ u01 Л w02 Л v03 Л G/ для некоторого набора a = = (aia2a3), a £ Sg, то для любого 7 £ Range f можно добавить к системе Ef (7) некоторое линейное уравнение и получить эквивалентную систему. Тем самым использование шаблонной КНФ Gf и SAT-оракула позволяет эффективно добавлять в системы вида Ef (7) новые линейные уравнения. Алгоритм, проверяющий для каждого И-узла g в Gf выполнимость КНФ u01 Л Л w02 Л v03 Л Gf по всем a = (aia2a3), a £ Sg, реализован в виде программы на С+-Ъ В вычислительных экспериментах описанная техника тестировалась на задачах криптоанализа ослабленных по числу шагов инициализации вариантов известного шифра Trivium [14]. Отметим, что Trivium является одним из победителей конкурса eSTREAM, и для данного шифра не известно на сегодняшний день убедительных атак, позволяющих найти секретный ключ существенно быстрее, чем полным перебором. Особенность Trivium заключается в том, что перед генерацией ключевого потока в этом шифре выполняется стадия инициализации, в ходе которой секретный ключ длиной 80 бит смешивается с несекретной 80-битной инициализирующей последовательностью. Изначально в стандарте Trivium предусмотрено 1152 шага инициализации. Однако даже при существенно меньшем числе шагов инициализации получаемые варианты Trivium оказываются стойкими ко всем известным видам криптоанализа. По-видимому, лучшими известными атаками на ослабленные по числу шагов инициализации варианты Trivium являются т.н. «кубические атаки», описанные в [15]. Следует отметить, что атаки из [15] весьма специфичны по ряду моментов. В частности, предполагается, что противник ищет ключ, который использовался многократно совместно с различными инициализирующими векторами. В атаках, построенных нами, мы исходим из более реалистичного сценария - предполагается, что различные ключи могут использоваться совместно с некоторым фиксированным инициализирующим вектором. Более конкретно, рассмотрены варианты Trivium с числом шагов инициализации N = 160, 192, 288, 384. Для каждого случая решается задача обращения функции f(Tr,N) : {0,1}80 ^ {0,1}300, которая соответствует алгоритму Trivium с числом шагов инициализации N и известным инициализирующим вектором (во всех экспериментах использовался один и тот же инициализирующий вектор). Для каждого из полученных шифров мы рассматривали задачу поиска линеаризующего множества с минимальной трудоёмкостью в двух вариантах. В первом варианте использован подход [1, 12]: мы искали множество, линеаризующее систему квадратичных уравнений над GF(2), построенную по И-НЕ-графу G/(TrN). Во втором варианте к такой системе добавляются дополнительные линейные уравнения, сгенерированные при помощи SAT-оракула в соответствии с описанной выше техникой. Задача поиска эффективного линеаризующего множества ставится как задача минимизации псевдобулевой функции, описанной в [12]. Для её решения используется генетический алгоритм [13]. Вычислительные эксперименты проводились на кластере «Академик В. М. Матросов» Иркутского суперкомпьютерного центра СО РАН [16]. Результаты экспериментов в виде оценок трудоёмкости соответствующих атак приведены в табл. 3. Таблица 3 Результаты сравнения двух подходов N Метод |B| Рв Сложность атаки (число решённых систем уравнений) 160 Алгоритм из [12] Алгоритм с SAT-оракулом 44 39 0,774 0,350 6,82e+13 4,71e+12 192 Алгоритм из [12] Алгоритм с SAT-оракулом 58 48 0,431 0,219 2,01e+18 3,86e+15 288 Алгоритм из [12] Алгоритм с SAT-оракулом 73 66 0,506 0,457 5,60e+22 4,84e+20 384 Алгоритм из [12] Алгоритм с SAT-оракулом 78 74 0,954 0,093 9,50e+23 6,12e+23 Комментарии к табл. 3. В первом столбце приведено число шагов инициализации в рассматриваемой версии шифра Trivium. Во втором столбце указаны алгоритмы: мы сравниваем метод, описанный в [12], с методом, представленным в настоящей работе (с использованием SAT-оракула). В последующих столбцах приведены мощность линеаризующего множества, вероятность линеаризации и оценка числа систем линейных уравнений, которые необходимо решить для нахождения 80-битного секретного ключа.

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

линеаризующие множества, атаки из класса «угадывай и определяй», квадратичные системы над GF(2), псевдобулева оптимизация, Trivium, linearizing sets, guess-and-determine attack, quadratic systems over GF(2), pseudo-Boolean optimization, Trivium

Авторы

ФИООрганизацияДополнительноE-mail
Антонов Кирилл ВалентиновичИМИТ ИГУстудентaknitr@mail.ru
Семёнов Александр АнатольевичИнститут динамики систем и теории управления им. В.М. Матросова СО РАНкандидат технических наук, доцент, заведующий лабораториейbiclop.rambler@yandex.ru
Всего: 2

Ссылки

Семёнов А. А., Антонов К. В., Отпущенников И. В. Поиск линеаризующих множеств в алгебраическом криптоанализе как задача псевдобулевой оптимизации // Прикладная дискретная математика. Приложение. 2019. №12. С. 130-134.
Biere A. Bounded Model Checking // Handbook of Satisfiability. Amsterdam: IOS Press, 2009. P. 457-481.
Отпущенников И. В., Семёнов А. А. Технология трансляции комбинаторных проблем в булевы уравнения // Прикладная дискретная математика. 2011. №1 (11). С. 96-115.
Otpuschennikov I., Semenov A., Gribanova I., et al. Encoding cryptographic functions to SAT using TRANSALG system // Proc. 22nd European Conf. ECAI 2016. Frontiers in Artificial Intelligence and Applications. 2016. V.285. P. 1594-1595.
Цейтин Г. С. О сложности вывода в исчислении высказываний // Записки научных семинаров ЛОМИ АН СССР. 1968. Т. 8. С. 234-259.
Semenov A., Otpuschennikov I., Gribanova I., et al. Translation of algorithmic descriptions of discrete functions to SAT with application to cryptanalysis problems // Log. Methods Comput. Sci. 2020. V. 16. Iss. 1. P. 29:1-29:42.
Чень Ч., Ли Р. Математическая логика и автоматическое доказательство теорем. М.: Наука, 1983.
Агибалов Г. П. Логические уравнения в криптоанализе генераторов ключевого потока // Вестник Томского госуниверситета. Приложение. 2003. №6. С. 31-41.
Semenov A., Zaikin O., Otpuschennikov I., et al. On cryptographic attacks using backdoors for SAT // Proc. 32nd AAAI Conf. 2018. P. 6641-6648.
Boros E. and Hammer P. Pseudo-Boolean optimization // Discr. Appl. Math. 2002. V. 123. Iss. 1-3. P. 155-225.
Glover F. and Laguna M. Tabu Search. Norwell: Kluwer Academic Publishers, 1997.
Антонов К. В., Семёнов А. А. Применение метаэвристических алгоритмов псевдобулевой оптимизации к поиску линеаризующих множеств в криптоанализе криптографических генераторов // Материалы 6-й Междунар. школы-семинара «Синтаксис и семантика логических систем». Иркутск: ИГУ, 2019. С. 13-18.
Pavlenko A., Semenov A., and Ulyantsev V. Evolutionary computation techniques for constructing SAT-based attacks in algebraic cryptanalysis // LNCS. 2019. V. 11454. P. 237-253.
De Canniere C. Trivium: A stream cipher construction inspired by block cipher design principles // LNCS. 2006. V.4176. P. 171-186.
Dinur I. and Shamir A. Cube attacks on tweakable black box polynomials // LNCS. 2009. V. 5479. P. 278-299.
ЦКП Иркутский суперкомпьютерный центр СО РАН. http://hpc.icc.ru.
 Применение SAT-оракулов для генерации дополнительных линейных ограничений в задачах криптоанализа некоторых легковесных шифров | ПДМ. Приложение. 2020. № 13. DOI: 10.17223/2226308X/13/34

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