基于MiniSat的多项式方程组求解实现

邹湘景，彭伟

（国防科技大学计算机学院，长沙410073）

基于MiniSat的多项式方程组求解实现

邹湘景，彭伟

（国防科技大学计算机学院，长沙410073）

在许多分析验证研究中，经常要对问题中的多项式组进行求解。当多项式方程组规模较大时，求解比较困难，大大限制了分析研究的效率。针对该问题设计了一种算法，将具有一定格式的多项式转化为合取范式形式，使多项式求解问题转化为SAT求解问题。利用SAT求解器MiniSat对二元域上的多项式组进行求解，使得密码分析过程更加高效。实验结果表明：该算法能正确地将多项式进行转化，并能快速利用MiniSat求出结果。

可满足性问题；MiniSat；多项式；合取范式

1　背景

布尔函数的可满足性问题（即SAT问题）是当前计算机理论界与逻辑学界共同关注的一个重要问题。SAT问题是第一个被证明的NP完全问题［1］，许多重要而且比较难解决的分析验证与组合问题都可转化成SAT问题，因此对SAT问题的研究在理论和实践方面都非常有意义。许多优秀的SAT求解器的设计实现（例如MiniSat等）使得SAT问题能够较快求解。SAT求解器在近几年得到广泛的研究、应用和改进，特别是在自动规划、模型诊断和电路等价性等领域。每年一度的国际SAT竞赛促使SAT求解器的效率不断提高。将一个问题转化成SAT问题就可以利用已有的SAT求解器进行求解从而得出答案。

Gregory V.Bard等［2］于2007年首次将SAT问题求解算法应用于密码分析中。在密码分析过程中，特别是在针对流密码的代数攻击中，经常需要对多元非线性方程组进行求解。而流密码的多元非线性方程组求解是一个NP难题，复杂性高，且没有较好的自动化求解程序。流密码的多元非线性方程组求解是在二元域上进行的，可以将方程组求解问题转化为SAT问题求解。如果先将方程组转化为合取范式（即CNF）形式，再利用现有的SAT求解器（如MiniSat）进行求解则可以极大降低复杂性。

将逻辑函数转化为CNF形式的方法在很多文献中都有提到，例如：数字电路中将“与”门表示为CNF形式的方法；将全加器的逻辑表达式转化为CNF形式的方法［3］。文献［4-5］对多项式方程组转化为CNF形式进行了描述，但文献［4］只简要描述了如何将一个非线性项通过添加变元转化为合取范式的方法，文献［5］也仅对简单的异或式子转化进行了简要描述。考虑到流密码的多元非线性方程组需要分析的规模较大，如果能自动将方程组转化为CNF形式，而后调用SAT求解器求解，则将极大简化对流密码的分析。

本文针对这一问题，立足已有的研究成果，依据逻辑代数的基本定律和相关规则，对二元域上的多元非线性多项式进行转化。通过系统框架及相关模块的设计，使得二元域上的多元非线性多项式转化为CNF形式的过程自动化，然后调用MiniSat求解器进行求解。以欧洲eSTREAM项目中的Trivium算法［6］为例进行实验，通过对Trivium算法的输出多项式组进行转化求解，得到多项式组的一个解，从而证明了该设计的有效性。

2　相关研究

序列密码是密码学中一个重要的分支，具有加解密速度快、硬件实现简单、错误扩散率小等特点，因此被广泛应用于保密通信等领域。序列密码的设计是灵活多变的，不同的算法结构对应着不同的分析方法。随着密码分析学的不断发展、攻击方案的不断改进和计算机技术的日益更新，B-M算法、相关攻击、最佳仿射逼近攻击和差分密码分析技术等都可以对某些密码进行分析与破译。将SAT问题求解引入密码分析是近年来的一个研究方向［7］，促进了密码分析技术的发展。

2.1序列密码分析

为了促进序列密码的发展，欧洲于2004年实施了eSTREAM研究项目，借此征集到适合广泛采用的新的序列密码算法，由此引发了对序列密码分析研究的新一轮热潮，特别是对eSTREAM项目候选算法的分析研究。

Trivium是最终入选的7个算法之一。虽然至今还没有针对Trivium的非常有效的攻击方法，但对Trivium的分析研究一直不断。2011年，贾艳艳等［8］针对2轮Trivium算法，通过找出更多线性逼近方程对其进行多线性密码分析，提出了一种更为有效的区分攻击方法。2013年，欧智慧等［9］在2轮Trivium的线性逼近研究中，针对文献［8］中线性逼近方程个数少和偏差小的问题，提出通过改变第1轮Trivium所占的时钟数和线性逼近式的方法对第2轮进行线性逼近，在攻击成功概率相同的前提下，所需的数据量降为原来的1/16。2012年，孙文龙等［10］针对初始化为288轮的简化版Trivium算法进行了线性分析，更正了Turan等给出的关于密钥、初始化向量和密钥流比特的表达式，同时给出了当允许选取特殊的密钥和初始化向量时搜索最佳线性逼近式的算法。丁林［11］在其学位论文中提出了针对Trivium的自动搜索差分路径技术，利用该技术可以得到任意轮Trivium算法的差分路径，证明了初始化轮数低于359的Trivium算法不能有效抵抗差分分析。随着SAT问题求解方法研究的发展，将SAT求解运用到Trivium算法的安全性分析中的情形也越来越多。例如，转化为SAT问题分析Trivium的可滑动对，利用MiniSat求解器分析Trivium的变种Bivium算法［12］等。到目前为止，对Trivium的分析还在不断进行。

2.2SAT问题相关研究

SAT问题是指：给定一组包含n个布尔变量X1，X2，X3，…，Xn（只能为真或假）的逻辑析取范式，查找是否存在它们的一组取值组合，使得该析取范式被满足。SAT问题是典型的NP完全问题，对它的深入研究有利于NP完全问题的解决。

关于SAT问题的算法主要有两种：完全算法和不完全算法。完全算法能求出命题逻辑公式的解或证明公式是不可满足的，但是效率无法满足实际需要；不完全算法求解速度相对较快，但是不一定能找到对应SAT问题的解。许多不完全算法都是基于局部搜索策略，其中代表性的有Selman和Kautz的GSAT算法、WALKSAT算法和NSAT算法，此外，梁东敏等对GSAT+walk的改进算法、黄文奇等提出的拟人拟物法、凌应标等［13］基于子句权重学习的求解SAT问题的遗传算法等也是重要的求解SAT问题的不完全算法。完全算法中最具代表性的是DPLL算法［14］，后续算法大多是在DPLL的基础上改进而来。当前许多最有效的求解器如Zchaff、BerkMinl和MiniSat都是基于DPLL算法。

迄今为止，SAT问题求解已经有很多研究成果。刘静等［15］基于组织的概念设计了一种新的进化算法求解SAT问题，将SAT问题分解成若干组织，然后用进化的方式来求解SAT问题。胡显伟等［16］提出了一种基于函数变换的求解SAT问题的新算法，利用SAT问题自身的特点将判定问题转化为连续函数的求极值问题，在求解速度、成功率和求解问题的规模等方面都有明显的提高。除此之外，还有一些优化SAT问题输入的预处理算法通过优化输入来减小SAT问题的规模，从而达到提高求解效率的目的。

2.3M iniSat求解器

MiniSat是一个性能优异且被广泛采用的SAT求解器，后续的许多SAT求解器都是在MiniSat的基础上进行改进。MiniSat输入为DIMACS格式［17］。DIMACS格式是一个简单的cnf文本格式，其注释行都是以“c”开始，非注释行的第1行为运行参数，格式为：

p cnf NUM_OF_VARIABLES NUM_OF_ CLAUSES。

其中：NUM_OF_VARIABLES表示布尔变量的个数；NUM_OF_CLAUSES表示子句的个数。

合取范式的每一个子句对应一行，一个子句的变量用标号表示，正值表示变量为原变量，负值表示变量为反变量，中间以空格分开，在每行结尾以0表示一个子句的结束。MiniSat求解器对输入的合取范式进行判定，如果输入有可满足解，则输出SAT，并输出一个解；如果不可满足，则输出UNSAT。

3　问题定义与分析

许多流密码的硬件设计实现主要由简单的逻辑电路组合而成，其输出逻辑式一般只包含“异或”（用⊕表示）、“与”（用·表示）和“或”（用+表示）3种，其他形式也可转化为这3种形式。因此，可以用A⊕B⊕C⊕D⊕E⊕F⊕…=0表示流密码的一轮输出多项式，其中A，B，C表示一个只包含“与”运算（用·表示）或者“或”运算（用+表示）的逻辑式，形如A=X1·X2·X3…。其他形式可以依据逻辑代数的交换律、分配律等基本定律变形为这种形式。对于该形式的逻辑代数，主要通过下面两步转化为CNF形式：

3.1将逻辑代数式转化为析取子句

对于逻辑代数式A⊕B⊕C⊕D⊕E⊕F⊕…=0，等式两边同时取反，即A⊕B⊕C⊕D⊕E⊕F⊕…若为1，依据异或逻辑运算规则中的反演率，可以推出A⊕B⊕C⊕D⊕E⊕F⊕…=1。要求出A⊕B⊕C⊕D⊕E⊕F⊕…=1的解，即要求等式左边A⊕B⊕C⊕D⊕E⊕F⊕…为真，因此可将其转化为CNF形式，通过MiniSat求可满足解使逻辑式A⊕B⊕C⊕D⊕E⊕F⊕…恒为真。

将形如A⊕B⊕C⊕D⊕E⊕F⊕…的式子转化为CNF形式，只需将其展开为逻辑代数的最大项表达式即可。由真值表得出逻辑代数的最大项表达式，只需将真值表中使函数值为0的各个最大项相与便可。因A⊕B⊕C⊕D⊕E⊕F⊕…为多项异或运算，即模二加运算，若使其值为0，则要求参与异或的各项中值取1的项为偶数项，而最大项中反变量表示1，原变量表示0，即要求参与异或的各项中取反的项为偶数项（A视为一个原变量整体）。

因此，从A、B、C、D…这些逻辑代数的异或项中选取偶数个项，并对选出的项取反，然后将所有项进行“或”运算，即可得到一个析取子句，如选取A、B这两项取反，可得一个析取子句为A+B+C+ D+E+F+…，即A+B+C+D+E+F+…。依次对所有项选取偶数个项，当所有偶数个项都选取到之后，将得到的析取子句用与运算连接起来，既可得到A⊕B⊕C⊕D⊕E⊕F⊕…的CNF形式。

3.2化简析取子句为合取范式析取项

以上得到的析取子句并不是合取范式的析取项，因为A，B，C等项中还包含有“与”运算或是“或”运算，需要进一步化简。对于“或”运算，如果该项（如A=X1+X2+X3）为原变量，即为（A+ B+C+D+…）形式，依据逻辑函数的结合律，在析取子句中不需化简，为（X1+X2+X3+B+C+ D+…）；对于“与”运算，如果该项（如A=X1· X2·X3）为反变量，即为（A+B+C+D+…）形式，则依据反演率和结合律，A=X1·X2·X3= X1+X2+X3，再按或运算代入其中得到（X1+ X2+X3+B+C+D+…）。

对于析取子句中原变量项中含有“与”运算，或是反变量项中含有“或”运算的，先将反变量项中的“或”运算通过反演率和结合律转变为“与”运算，如A=X1+X2+X3=X1·X2·X3。设计一个模块，对析取子句中含有的“与”运算进行转化。依据逻辑代数的分配率A+BC=（A+B）（A+C），将A=X1·X2·X3…Xn形式的与项代入，得到n个析取项。

通过以上两步，可将一个逻辑代数式转化为CNF形式，而后调用MiniSat求解器对CNF从句求解，得到的可满足解就是逻辑代数式的解。

4　算法设计与实现

要将逻辑代数式转化为CNF形式，主要通过设计3个模块完成：mcnf模块、combination模块和split模块。由于需要转化的逻辑代数式为字符串形式，故先对其进行适当的处理。mcnf模块先将逻辑代数式进行适当变形化简，以适应combination模块的输入；combination模块主要是对所有异或项选取偶数项并取反，对于非标准合取范式中的析取项，调用split模块进行最后的处理。算法主要流程如图1所示。

图1　算法主要流程

4.1m cn f模块

mcnf模块的主要功能是将输入的字符串形式的逻辑代数式按照异或运算符分成一个个单独的项，并依据异或运算的重叠率和自等率将重复偶数次的项删除，得到的结果作为后面模块的输入，调用combination模块对异或项选取偶数项取反变量。算法伪码描述如下：

1）读入一个表示逻辑代数的字符串。

2）对字符串第1个字符至最后一个字符进行判断：①如果字符为“+”，存放字符的数组下标加1并判断下一个字符；②如果字符不为“+”，将字符放入数组中并判断下一个字符。

3）从数组第1个元素开始比较，将两个相同的元素重新赋值为“NULL”。

4）将数组中为“NULL”的元素移至数组最后。

5）对数组元素调用combination模块取偶数项。

6）结束。

4.2 com bination模块

combination模块的功能是从输入的异或项数组中选取偶数项并对其取反。定义一个vector结构变量vecOrder用以存储数组下标，然后通过对下标的取值来确定数组中的元素。例如，要从n个元素中取m个，则先取下标为0，1，2，3…（m-1）的元素，然后从下标数组的最右边一个开始加1，即下一组为取下标为0，1，2…（m-2），m的元素，直到取到下标为0，1，2…（m-2），（n-1）的一组元素。之后将下标数组的右边起第2个加1，并重复上面过程，直至所有情况都被选出为止。伪代码描述如下：

1）输入一个字符串数组X［］、数组元素个数n和需取反的项数m。

2）定义一个整型vector变量vecOrder并初始化为1，2，…，m，定义变量position并赋值为（m-1）以标识位置。

3）将数组中下标为vecOrder的元素的项取出并取反，然后和数组中剩下的项一起组成一个字符串，调用split模块。

4）如果vecOrder中的第1个元素为（n-m+ 1）（即取到了数组中的最后m个元素），跳至步骤7）。

5）如果vecOrder中的最后一个元素不为n且vecOrder中前面的元素都比后面的元素小，则将vecOrder中的最后一个元素加1并跳至步骤3）。

6）如果vecOrder中的最后一个元素为n，将position减1，即将标识位置向左移一位，将position位置及其右边的值都加1并跳至步骤5）。

7）结束。

4.3split模块

split模块的功能是将输出的析取子句中的与项利用分配率拆分成标准的析取项。对于输入的带*的字符串，以*和空格为判断符，将字符串拆分成两部分，并递归调用，直至字符串中不含*符号。输出的不含*的字符串即为DIMACS格式的输入。其伪代码为：

输入：带有与运算（*）的析取子句字符串

输出：标准的DIMACS格式文件

split（string X）

1.判断输入的字符串中是否含有“*”：

1.1不含“*”，直接输出字符串；

1.2否则将字符串分成两部分：

1.2.1字符串中第1个“*”之前的部

分加“*”后面第1个空格之后的部分，再调用split；

1.2.2字符串中第1个“*”前面第1个空格之前的部分加“*”之后的部分，再调用split；

2.结束。

5　实验及结果分析

为了验证设计的正确性和分析转化的效率，本文以Trivium算法为例进行实验。Trivium是进入欧洲eSTREAM计划最终方案的一个序列密码算法。算法分为两部分：第1部分为初始化阶段，利用80位密钥和80位初始化向量将288位内部状态进行初始化，在前4×288轮循环中，算法不输出密钥流；第2部分为密钥流生成阶段，在4× 288轮循环之后生成用于加密的密钥流Zi。其算法伪代码描述如下：

本文主要对初始化阶段产生的多项式组进行实验。

5.1实验运行环境

实验中的mcnf模块、combination模块和split模块主要基于Windows下的VC++6.0环境编译运行，运行平台为32位Windows XP，硬件配置为AMD Athlon（tm）Dual Core Processor CPU 2.71 GHz，2G运行内存。CNF求解时，在同一台机器上的VMWare虚拟机中创建Ubuntu系统，在Ubuntu系统下运行MiniSat求解。

5.2实验过程

实验中，首先对Trivium密码初始化过程中的前93轮输出多项式进行转化，其输出多项式为：

0=Z1+s66+s93+s162+s177+s243+s288

0=Z2+s65+s92+s161+s176+s242+s287

…

0=Z92+s218+s263+s261*s262+s44+s2+ s44+s71+s69*s70+s149+s59+s86+s84*s85+ s164+s137+s152+s150*s151+s239+s197

0=Z93+s217+s262+s260*s261+s43+s1+ s43+s70+s68*s69+s148+s58+s85+s83*s84+ s163+s136+s151+s149*s150+s238+s196

在VC++6.0下编译运行，利用3个模块转化后得出的结果为：

-66-93 162 177 243 288 0

-66 93-162 177 243 288 0

…

217 262 261 1 70 69 148 58 85 84 163 136 151 149 238 196 0

217 262 261 1 70 69 148 58 85 84 163 136 151 150 238 196 0

此输出文件共有子句1 716 381个，程序运行时间为477 s，输出文件大小为120 M。在Ubuntu系统下通过./minisat〈cnf-file〉〈out-file〉调用MiniSat求解，经过3.5 s即求出了一个可满足解，见图2。

对Trivium初始化过程中的第94～111轮输出多项式进行转化，得到的输出文件共有子句8 957 970个，程序运行时间为3 033 s，输出文件大小为720 M。使用MiniSat在9.76 s后得到一个可满足解。

图2　一个可满足解

5.3结果分析

通过上面的结果可以看到：该算法在Trivium前93轮和第94～111轮都能很好地转化为CNF形式，并通过Ubuntu系统中的MiniSat求解，得出可满足解。但是从运行时间和转化的规模上来看，随着循环次数的增加，多项式中项数越来越多，转化后的子句数也越来越多，程序运行时间变长。通过分析，在Trivium算法的初始化阶段，去除重复项后到第122轮时，其多项式中有20项，可产生的子句数至少是220-1个；到第200轮时，多项式中有53项，可产生的子句数至少是253-1个，程序无法在短时间内成功转换。因此，减少多项式的项数是下一步算法改进的主要方向。

6　结束语

本文设计并实现了基于MiniSat的多元非线性多项式自动求解算法，可在二元域内将多元非线性多项式自动转化为CNF形式，进而调用Mini-Sat求出方程组的解。本文算法适用于对流密码代数攻击的分析，降低了分析过程中方程组的求解难度。

针对转换过程中CNF子句个数规模较大的问题，下一步的主要工作包括：①考虑通过引进一定数量的新变元替换方程组中出现频率较高的多项式，从而减少方程组中单项式个数，达到进一步减小CNF子句规模的目的；②参考文献［18］中的方法，引进新变元化简方程组中的非线性项，或是综合考虑方程组之间的关系，通过猜测一定数量的变量的值将方程组中的一些非线性项转变为线性项，简化方程；③调用不同的SAT求解器，分析多种求解器的求解效率，从而选择最佳求解程序。

［1］Cook SA.The complexity of theorem-proving procedures［C］//Proceedings of the 3rd Annual ACM Symposium on Theory of Computing.New York，USA：ACM，1971：151-158.

［2］Bard G V，Courtois N T，Jefferson C.Efficient Methods for Conversion and Solution of Sparse Systems of Low-Degree Multivariate Polynomials over GF（2）via SAT-Solvers［R］.Cryptology ePrint Archive，Report 2007/ 024，2007.

［3］曾维鹏，蔡莉莎，吴恒玉，等.MiniSAT求解器在电路故障诊断中的应用［J］.电气电子教学学报，2013，35（6）：60-62.

［4］戴江海，戚文峰.利用一种SAT问题全解算法求Trivium可滑动对［J］.信息工程大学学报，2012，13（1）：1 -7.

［5］Mate Soos，Karsten Nohl，Claude Castelluccia.Extending SAT Solvers to Cryptographic Problems［Z］.

［6］De Canniere C，Preneel B.TRIVIUM：A stream cipher construction inspired by block cipher design principles［C］//Proceedings of ISC2006.Heidelberg：Springer，2006：171-186.

［7］金海荣.混沌序列密码分析及应用研究［D］.哈尔滨：黑龙江大学，2009.

［8］贾艳艳，胡予濮，杨文峰，等.2轮Trivium的多线性密码分析［J］.电子与信息学报，2011，33（1）：223-227.

［9］欧智慧，赵亚群.2轮Trivium的线性逼近研究［J］.计算机工程，2013，39（11）：32-40.

［10］孙文龙，关杰，刘建东.针对简化版Trivium算法的线性分析［J］.计算机学报，2012，35（9）：1890-1896.

［11］丁林.序列密码初始化算法的安全性分析［D］.郑州：解放军信息工程大学，2012.

［12］Cameron McDonald，Chris Charnes，Josef Pieprzyk.Attacking Bivium with MiniSat［Z］.

［13］凌应标，吴向军，姜云飞.基于子句权重学习的求解SAT问题的遗传算法［J］.计算机学报，2005，28（9）：1476-1482.

［14］Hachtel G D，Somenzi F.Logic Synthesis and Verification Algorithms［M］.USA：Kluwer Academic Publishers，1996.

［15］刘静，钟伟才，刘芳，等.组织进化算法求解SAT问题［J］.计算机学报，2004，27（10）：1422-1428.

［16］胡显伟，任世军.基于函数变换的求解SAT问题的新算法［J］.智能计算机与应用，2012（3）：33-39.

［17］DIMACS［EB/OL］.［2012-06-28］.http：//www.cs. ubc.ca/hoos/SATLIB/Benchmarks/SAT/satformat.ps.

［18］孙文龙，关杰.针对Trivium型密码算法的代数攻击［J］.上海交通大学学报，2014，48（10）：1434-1439.

（责任编辑杨黎丽）

Realization of Solving Polynom ial System of Equations Based on M iniSat

ZOU Xiang-jing，PENGWei
（College of Computer，National University of Defense Technology，Changsha 410073，China）

In many research works of formal analysis and verification，it is often required to solve the polynomial equations associated with a problem.When the scale of the polynomial equations is large，it is difficult to get the solution，which greatly limits the efficiency of analysis.To solve the problem，an algorithm was designed in this paper which transforms polynomial equations with a certain format into conjunctive normal forms，thus the problem of solving polynomialequations can be turned to solve a boolean satisfiability problem（SAT）.The SAT solver MiniSatwas applied to solve the polynomial equations in GF（2）so thata solution can be found quickly andmake the analysismore efficient.Experiment results show that the proposed algorithm can convert polynomial equations correctly，and a solution can be found quickly with MiniSat.

boolean satisfiability problem；MiniSat；polynomial equations；conjunctive normal form

TP302

A

1674-8425（2015）06-0075-07

2015-03-22

国防科技大学预研项目；国家自然科学基金资助项目（61271252，61272010）

邹湘景（1986—），男，湖南岳阳人，硕士研究生，主要从事计算机网络信息安全研究；彭伟（1973—），男，研究员，主要从事计算机网络和网络安全研究。

邹湘景，彭伟.基于MiniSat的多项式方程组求解实现［J］.重庆理工大学学报：自然科学版，2015（6）：75 -81.

form at：ZOU Xiang-jing，PENGWei.Realization of Solving Polynomial System of Equations Based on MiniSat［J］. Journal of Chongqing University of Technology：Natural Science，2015（6）：75-81.