3
我一直在試圖使用Cryptominisat（類似的事情）來制定對Piccolo的攻擊，這是一種類似於AES的輕量級分組密碼。關於SAT求解器和CNF文件
方程是這樣的：
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;我需要一些關於下一步的幫助。我已經準備好了攻擊和解密的CNF方程，我真的需要如何使用座標解算器的幫助，並將它放在CNF文件格式中。我一直在尋找互聯網，但沒有任何地方給出明確的方法。任何幫助，將不勝感激。如果需要更多信息，請隨時詢問。我需要將上述方程式放入cnf文件中。
由於涉及的方程式相當複雜（還有更多），因此cnf文件及其工作的一些參考或示例將非常棒。
感謝您的參考。由於我正在研究與AES非常相似的Piccolo，因此用於解決相關分組密碼的示例CNF文件將有所幫助。我需要更好地瞭解如何放置這種格式的複雜和級聯方程。謝謝！ – 2013-04-30 18:42:36
問題可能是您的方程式中有運算符不是SAT求解程序直接支持的運算符 - 例如，我猜XORs？您可能需要編寫一個程序來爲您轉換方程式，但也許有人知道SAT解算器已根據密碼分析的需要進行了調整... – Tilo 2013-04-30 18:54:14
不，這些方程式均爲cnf格式。但是，我必須將錯誤和解密表示爲方程式。例如，故障的方程爲： z = z1 | z2 | ... | z16,1 <= i <= 16 然後， ui =（1 + z（4i-3））^（ （4i-2））^（1 + z（4i-1））^（！+ z（4i）），1≤i≤4 和我在問題中描述的最後一個方程。希望我現在更好地解釋自己。 – 2013-04-30 19:07:02