关于SAT求解器和CNF文件

我一直在试图使用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文件及其工作的一些参考或示例将非常棒。

来源

2013-04-30 Rishav Mishra

的CNF格式的这个规范可以帮助你：

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

有此页面上的链接的样本文件：

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

来源

2013-04-30 18:37:36 Tilo

感谢您的参考。由于我正在研究与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

关于SAT求解器和CNF文件

回答

相关问题