Hybrid approach (SAT +ROBDD) to cryptanalysis of stream encryption systems.pdf В настоящем докладе представлен подход к решению логических (булевых) уравнений,в основе которого лежит гибридная стратегия, использующая как быстрые алгоритмырешения SAT-задач (нехронологический DPLL-вывод), так и двоичные диаграммырешений (BDD). Построенные алгоритмы тестировались на задачах обращенияряда криптографических функций.Главным объектом рассмотрения являются задачи обращения всюду определенныхдискретных функций, вычислимых за полиномиальное время. Более точно, речьидет о семействах функций вида f n : { 0 ,1}n ^ {0,1 }*, где { 0 ,1}n - множество всевозможныхдвоичных векторов длины n, а {0, 1}* - множество всевозможных двоичныхвекторов произвольной конечной длины. Предполагается, что для любого n Е Nфункция fn всюду определена и существует программа для детерминированной машиныТьюринга (ДМТ), которая вычисляет все функции семейства f = { f n} new. Еслитакая программа имеет полиномиальную от n сложность, то говорим, что семействофункций f находится в классе S. Задача обращения f n Е S заключается в том, чтобыпо известному у из области значений f n найти такое x Е { 0 ,1}n, что f n(x) = у.В работах [1 - 4] был развит пропозициональный подход к задачам обращения дискретныхфункций из класса S. В основе данного подхода лежит идея пропозициональногопредставления алгоритмов, восходящая к С. А. Куку. В соответствии с пропозициональнымподходом алгоритм вычисления дискретной функции f n Е S представляетсяв виде системы логических уравнений S (fn), которая, грубо говоря, описывает все возможныеварианты эволюции программы, вычисляющей f n, на входах из { 0 , 1}n. Послеподстановки в систему S (fn) вектора у из области значений f n имеем совместную системулогических уравнений S (fn)|y, решая которую, находим такой x Е { 0 ,1}n, чтоf n(x) = у. Для решения систем вида S (fn)|y могут использоваться различные подходы.В [1-4] для этих целей применялся SAT-подход, в основе которого лежит техникаприведения систем S (fn)|y к уравнениям вида «КНФ=1».В [3] была предложена технология крупноблочного параллелизма, предназначеннаядля решения SAT-задач. В работах [1, 3, 4] данная технология использовалась длярешения задач обращения некоторых криптографических функций на суперкомпьютерах.В качестве новых результатов в настоящем докладе фигурирует описание комбинированногоподхода к решению задач обращения дискретных функций из класса S,использующего как SAT-технологии, так и двоичные диаграммы решений (BDD). Основнаяидея такого подхода состоит в использовании BDD, а точнее, ROBDD длямодификации баз конфликтных дизъюнктов. Соответствующий механизм позволяетизбежать потери полноты базовым алгоритмом решения SAT-задачи (данный негативныйэффект, возникающий в современных SAT-решателях, был отмечен в [4]). Предполагаетсярассмотреть результаты вычислительных экспериментов по использованиюгибридного подхода (SAT+ROBDD) в распределенных вычислительных средах.

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