Относительно SAT Solvers и файлов cnf

Я пытался использовать Cryptominisat (подойдет что-то подобное), чтобы сформулировать атаку на Piccolo, легкий блочный шифр, похожий на AES.

Уравнения выглядят примерно так:

Z= z1|z2|...|z16, 1<= i<=16

Тогда ui = (1 + z (4i-3)) ^ (1+ z (4i-2)) ^ (1 + z (4i-1)) ^ (1+ z (4i)), 1 ‹= i ‹= 4

Тогда (1 + u1) V (1 + u2) V (1 + u3) V (1 + u4) = 1; ui + uj = 1, i ‹= i‹ = j ‹= 4

Мне нужна помощь относительно моего следующего шага. У меня есть готовые уравнения CNF для атаки и дешифрования, мне действительно нужна помощь в том, как использовать это с спутниковым решателем и поместить в формат файла CNF. Я искал в Интернете, но нигде нет четкого метода. Любая помощь будет оценена. Если вам нужна дополнительная информация, не стесняйтесь спрашивать. Мне нужно поместить приведенные выше уравнения в файл cnf.

Поскольку задействованные уравнения довольно сложны (их больше), некоторые ссылки или примеры для файлов cnf и их работы будут потрясающими.


c cryptography cnf cryptanalysis
person Rishav Mishra    schedule 30.04.2013    source источник

Ответы (1)


arrow_upward
1
arrow_downward

Эта спецификация формата CNF может помочь вам:

http://people.sc.fsu.edu/~jburkardt/pdf/dimacs_cnf.pdf

На этой странице есть ссылки на образцы файлов:

http://people.sc.fsu.edu/~jburkardt/data/cnf/cnf.html

person Tilo    schedule 30.04.2013
comment
Спасибо за ссылки. Поскольку я работаю над Piccolo, который действительно похож на AES, пример файла CNF, используемого для решения связанного блочного шифра, очень поможет. Мне нужно лучше понять, как составлять сложные и каскадные уравнения в этом формате. Спасибо! - person Rishav Mishra; 30.04.2013
comment
Проблема, вероятно, будет в том, что у вас есть операторы в ваших уравнениях, которые напрямую не поддерживаются решателями SAT - я бы предположил, например, XOR? Возможно, вам придется написать программу для преобразования уравнений за вас, но, возможно, кто-то знает решатель SAT, который был адаптирован к потребностям криптоанализа ... - person Tilo; 30.04.2013
comment
Нет, все уравнения в формате 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 и последнее уравнение, которое я описал в вопросе. Надеюсь, теперь я лучше объяснил. - person Rishav Mishra; 30.04.2013
comment
Это может быть тот же файл: elis.dvo.ru/~lab_11/glpk -doc / cnfsat.pdf (ссылка работает по состоянию на 09.12.2013) - person Tilo; 09.12.2013
comment
@RishavMishra, вы сможете помочь мне с этим вопросом, пожалуйста, crypto .stackexchange.com / questions / 18514 / - person Juan; 08.08.2014