Проблема булевой выполнимости и ее применение в криптоанализе
Habr ·
Алгоритмы решения проблемы булевой выполнимости (SAT – от Satisfiability) и реализующие их средства (SAT-решатели) позволяют определить выполнимость конкретной булевой формулы – существует ли такой набор определенных булевых значений («ложь»/«истина») переменных формулы, при которых результат формулы становится истинным. Проблема булевой выполнимости хорошо изучена; существуют различные методы сведения разного рода частных задач к формулировке на их основе конкретной булевой формулы и последующего решения определенного экземпляра задачи с помощью алгоритмов решения проблемы булевой выполнимости. Алгоритмический аппарат также активно развивается; в частности, предложены эффективные алгоритмы, позволяющие автоматизировать поиск значений переменных, приводящих к решению проблемы булевой выполнимости [1]. Алгоритмы, лежащие в основе SAT-решателей, хорошо распараллеливаются, что позволяет эффективно использовать вычислительные кластеры [2]. В анализе криптографических алгоритмов существует достаточно много задач, которые могут быть сведены к решению проблемы булевой выполнимости, что позволяет использовать хорошо изученный математический и эффективный алгоритмический аппарат решения SAT-задач для доказательства криптографических свойств (или для получения информации о криптографических свойствах) анализируемого алгоритма. В этой статье мы совместно с моей коллегой – ведущим аналитиком компании «Актив» Мариной Скоробогатовой – подготовили небольшой обзор применений подхода сведения задач криптоанализа к SAT-задачам, который и предлагаем вам под катом. Читать далее
Алгоритмы решения проблемы булевой выполнимости (SAT – от Satisfiability) и реализующие их средства (SAT-решатели) позволяют определить выполнимость конкретной булевой формулы – существует ли такой набор определенных булевых значений («ложь»/«истина») переменных формулы, при которых результат формулы становится истинным. Проблема булевой выполнимости хорошо изучена; существуют различные методы сведения разного рода частных задач к формулировке на их основе конкретной булевой формулы и последующего решения определенного экземпляра задачи с помощью алгоритмов решения проблемы булевой выполнимости. Алгоритмический аппарат также активно развивается; в частности, предложены эффективные алгоритмы, позволяющие автоматизировать поиск значений переменных, приводящих к решению проблемы булевой выполнимости [1]. Алгоритмы, лежащие в основе SAT-решателей, хорошо распараллеливаются, что позволяет эффективно использовать вычислительные кластеры [2]. В анализе криптографических алгоритмов существует достаточно много задач, которые могут быть сведены к решению проблемы булевой выполнимости, что позволяет использовать хорошо изученный математический и эффективный алгоритмический аппарат решения SAT-задач для доказательства криптографических свойств (или для получения информации о криптографических свойствах) анализируемого алгоритма. В этой статье мы совместно с моей коллегой – ведущим аналитиком компании «Актив» Мариной Скоробогатовой – подготовили небольшой обзор применений подхода сведения задач криптоанализа к SAT-задачам, который и предлагаем вам под катом. Читать далее