Я пытаюсь использовать Cryptominisat (что-то подобное сделает), чтобы сформулировать атаку на Piccolo, легкий блок-шифр, аналогичный AES.Что касается SAT Solvers и cnf файлов
Уравнения что-то вроде этого:
Z = z1 | z2 | ... | z16, 1 < = я < = 16
Тогда щ = (1 + г (4i-3))^(1+ г (4i-2))^(1 + Z (4i-1))^(1+ г (4i)), 1 = < я < = 4
Затем (1 + u1) V (1 + u2) V (1 + u3) V (1 + u4) = 1; ui + uj = 1, i < = i < = j < = 4
Мне нужна помощь относительно моего следующего шага. У меня есть уравнения CNF для атаки и готовое дешифрование, мне действительно нужна помощь в том, как использовать это с помощью сат-решателя и помещать его в формат файла CNF. Я смотрю по всему Интернету, но нет четкого метода, который дается где угодно. Любая помощь будет оценена по достоинству. Если вам нужна дополнительная информация, пожалуйста, не стесняйтесь спрашивать. Мне нужно поставить вышеуказанные уравнения в файл cnf.
Поскольку задействованные уравнения довольно сложны (их больше), некоторые ссылки или примеры для файлов cnf и их работы были бы удивительными.
Спасибо за ссылки. Поскольку я работаю над Piccolo, который действительно похож на AES, пример файла CNF, используемого для решения связанного блочного шифрования, поможет тонну. Мне нужно лучшее представление о том, как подавить сложные и каскадные уравнения в этом формате. Благодаря! –
Проблема, вероятно, в том, что у вас есть операторы в ваших уравнениях, которые напрямую не поддерживаются решателями SAT - я бы предположил, например, XOR? Возможно, вам придется написать программу для преобразования уравнений для вас, но, возможно, кто-то знает о решателе SAT, который был скорректирован с учетом криптоанализа ... – Tilo
Нет, уравнения все в формате cnf. Однако я должен представлять ошибки и дешифрование как уравнения. Например, уравнения для разлома: Z = z1 | z2 | ... | z16, 1 <= i <= 16 Затем ui = (1 + z (4i-3))^(! + z (4i-2))^(1 + z (4i-1))^(! + z (4i)), 1 <= i <= 4 и последнее уравнение, которое я описал в вопросе. Надеюсь, я сейчас объяснил себя лучше. –