Transformation of CNF via resolution.pdf Одним из методов криптоанализа является логический криптоанализ, когда криптографическийалгоритм рассматривается как программа для машины Тьюринга иподстановка открытого и шифрованного текстов в эту программу приводит к задачеВЫПОЛНИМОСТЬ (SAT) для КНФ. Проблема состоит в том, что получаемыеКНФ имеют большие размерности даже при небольшой размерности исходной задачи.Представленный в данной работе метод позволяет преобразовать исходную КНФв эквивалентную, с меньшим количеством дизъюнктов и переменных. Метод можетбыть использован как препроцессор КНФ для увеличения эффективности алгоритмоврешения задачи SAT [1].Метод резолюции основан на правилах исчисления высказываний и включает всебя ряд методик.1. Простая резолюция и разрешение уникальных переменных. Данная методикаоснована на следующих правилах вывода:1) (х V Y )&х ^ Y2) TRUE V х ^ TRUE3 ) FALSE V х ^ х4) х V х ^ TRUE5) х&х ^ o (пустой дизъюнкт)2. Резолюция по соседним дизъюнктам. Два дизъюнкта называются соседними,если они различаются знаком по единственному литералу. Резольвентой по соседнимдизъюнктам называется дизъюнкт, являющийся максимальным общим подмножествомсоседних дизъюнктов. Если в КНФ присутствует конъюнкция соседних дизъюнктов,то конъюнкция заменяется резольвентой по соседним дизъюнктам.3. Бинарная резолюция. Два дизъюнкта разрешимы относительно бинарной резолюции(бинарно разрешимы), если они совпадают хотя бы по одной переменной,которая входит в один дизъюнкт с отрицанием, а в другой - без.Справедлива следующая теорема, которая показывает, что бинарная резолюцияв применении к исходной КНФ может дать тот же результат, что и резолюция пососедним дизъюнктам, периодически применяемая во время поиска решения.Теорема 1. Любой дизъюнкт, полученный в результате резолюции по соседнимдизъюнктам в процессе переборного поиска решения, является производным от некоторогодизъюнкта, который может быть получен в результате применения бинарнойрезолюции к исходной КНФ.В результате применения методик 1-3 количество дизъюнктов в КНФ уменьшается,что приводит к уменьшению области поиска для различных алгоритмов решениязадачи SAT.Для проведения численных экспериментов были использованы следующие классыКНФ: FACTOR (КНФ, ассоциированные с задачей факторизации), DLOG (КНФ,ассоциированные с задачей дискретногологарифмирования), EDLOG (КНФ, ассоциированныес задачей дискретного логарифмирования на эллиптической кривой)[2]. Входные параметры алгоритмов сведения задач криптоанализа выбиралисьисходя из рекомендуемых соответствующими стандартами условий обеспечения криптостойкости[3]. Количество дизъюнктов и переменных в тестовых КНФ достигает 107и 106 соответственно.Результаты показывают, что для КНФ, ассоциированных с задачей факторизации,удается разрешать до 1,1% переменных и сокращать до 67% дизъюнктов исходнойКНФ, независимо от размерности исходной задачи. Для КНФ, ассоциированных состальными задачами криптоанализа, удается сократить число дизъюнктов на двапорядка. При этом трудоемкость метода резолюции не выше кубической от количествабит в ключе.Таким образом, метод резолюции является эффективным препроцессором КНФ,ассоциированных с задачами криптоанализа асимметричных шифров.

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