CSEDays. Theory 2011

Екатеринбург, 14-17 апреля

News subscription
Share:

Reviews

Хорошее получилось мероприятие с потенциалом на будущее. Организаторы молодцы! :)
-- / CSEDays. Theory 2011
Home / CSEDays Theory 2011 / Семёнов Александр /

Решение задач криптоанализа с использованием SAT- и BDD-решателей

Author: Семёнов Александр Анатольевич

В докладе предполагается рассмотреть общую проблему обращения эффективно вычислимых дискретных функций (то есть функций, преобразующих двоичные слова в двоичные слова).

Проблема обращения заключается в том, чтобы по известному образу и известному описанию функции (в нашем случае таким описанием является алгоритм) найти неизвестный прообраз. Большое число практически важных задач, в том числе различные задачи криптоанализа, можно рассматривать как частные случаи проблемы обращения эффективно вычислимых дискретных функций. Построение «практически эффективных» вычислительных методов для решения задач обращения – крайне важная и актуальная проблема. «Практическая эффективность» того или иного метода/алгоритма должна быть убедительно аргументирована. В этом плане задачи криптоанализа могут выступать в роли таких аргументов – если метод успешно справляется с криптографическими тестами, он, как правило, эффективен и на задачах, вычислительная трудность в которые не закладывалась искусственно.

В докладе будут рассмотрены механизмы сведения задач обращения дискретных функций к системам булевых уравнений. Для решения последних используются SAT-решатели, базирующиеся на алгоритме DPLL, а также двоичные диаграммы решений (BDD). Будут представлены результаты по решению (с применением SAT- и BDD-решателей) задач криптоанализа некоторых систем шифрования в распределенных вычислительных средах. Будут приведены примеры использования SAT- и BDD-подходов в биоинформатике (в исследовании дискретных моделей генных сетей).

Посмотреть презентацию

Посмотреть видео лекции

Минимальные требования к знаниям слушателей:

  • стандартный университетский курс дискретной математики;
  • начальные главы математической логики (в объеме исчисления высказываний);
  • представления о вычислительной сложности алгоритмов.

Рекомендуется к прочтению по BDD:

  • Meinel Ch., Theobald T. Algorithms and Data Structures in VLSI-Design: OBDD-Foundations and Applications. Springer-Verlag, Berlin, Heidelberg, New York, 1998 (доступна в Интернете); 
  • Ю.Г. Карпов Model Checking. Верификация параллельных и распределенных программных систем. "БХВ-Петербург", 2010 (BDD не является основной темой данной книги).