基于MiniSat的多項(xiàng)式方程組求解實(shí)現(xiàn)

鄒湘景，彭偉

（國防科技大學(xué)計算機(jī)學(xué)院，長沙410073）

基于MiniSat的多項(xiàng)式方程組求解實(shí)現(xiàn)

鄒湘景，彭偉

（國防科技大學(xué)計算機(jī)學(xué)院，長沙410073）

在許多分析驗(yàn)證研究中，經(jīng)常要對問題中的多項(xiàng)式組進(jìn)行求解。當(dāng)多項(xiàng)式方程組規(guī)模較大時，求解比較困難，大大限制了分析研究的效率。針對該問題設(shè)計了一種算法，將具有一定格式的多項(xiàng)式轉(zhuǎn)化為合取范式形式，使多項(xiàng)式求解問題轉(zhuǎn)化為SAT求解問題。利用SAT求解器MiniSat對二元域上的多項(xiàng)式組進(jìn)行求解，使得密碼分析過程更加高效。實(shí)驗(yàn)結(jié)果表明：該算法能正確地將多項(xiàng)式進(jìn)行轉(zhuǎn)化，并能快速利用MiniSat求出結(jié)果。

可滿足性問題；MiniSat；多項(xiàng)式；合取范式

1　背景

布爾函數(shù)的可滿足性問題（即SAT問題）是當(dāng)前計算機(jī)理論界與邏輯學(xué)界共同關(guān)注的一個重要問題。SAT問題是第一個被證明的NP完全問題［1］，許多重要而且比較難解決的分析驗(yàn)證與組合問題都可轉(zhuǎn)化成SAT問題，因此對SAT問題的研究在理論和實(shí)踐方面都非常有意義。許多優(yōu)秀的SAT求解器的設(shè)計實(shí)現(xiàn)（例如MiniSat等）使得SAT問題能夠較快求解。SAT求解器在近幾年得到廣泛的研究、應(yīng)用和改進(jìn)，特別是在自動規(guī)劃、模型診斷和電路等價性等領(lǐng)域。每年一度的國際SAT競賽促使SAT求解器的效率不斷提高。將一個問題轉(zhuǎn)化成SAT問題就可以利用已有的SAT求解器進(jìn)行求解從而得出答案。

Gregory V.Bard等［2］于2007年首次將SAT問題求解算法應(yīng)用于密碼分析中。在密碼分析過程中，特別是在針對流密碼的代數(shù)攻擊中，經(jīng)常需要對多元非線性方程組進(jìn)行求解。而流密碼的多元非線性方程組求解是一個NP難題，復(fù)雜性高，且沒有較好的自動化求解程序。流密碼的多元非線性方程組求解是在二元域上進(jìn)行的，可以將方程組求解問題轉(zhuǎn)化為SAT問題求解。如果先將方程組轉(zhuǎn)化為合取范式（即CNF）形式，再利用現(xiàn)有的SAT求解器（如MiniSat）進(jìn)行求解則可以極大降低復(fù)雜性。

將邏輯函數(shù)轉(zhuǎn)化為CNF形式的方法在很多文獻(xiàn)中都有提到，例如：數(shù)字電路中將“與”門表示為CNF形式的方法；將全加器的邏輯表達(dá)式轉(zhuǎn)化為CNF形式的方法［3］。文獻(xiàn)［4-5］對多項(xiàng)式方程組轉(zhuǎn)化為CNF形式進(jìn)行了描述，但文獻(xiàn)［4］只簡要描述了如何將一個非線性項(xiàng)通過添加變元轉(zhuǎn)化為合取范式的方法，文獻(xiàn)［5］也僅對簡單的異或式子轉(zhuǎn)化進(jìn)行了簡要描述?？紤]到流密碼的多元非線性方程組需要分析的規(guī)模較大，如果能自動將方程組轉(zhuǎn)化為CNF形式，而后調(diào)用SAT求解器求解，則將極大簡化對流密碼的分析。

本文針對這一問題，立足已有的研究成果，依據(jù)邏輯代數(shù)的基本定律和相關(guān)規(guī)則，對二元域上的多元非線性多項(xiàng)式進(jìn)行轉(zhuǎn)化。通過系統(tǒng)框架及相關(guān)模塊的設(shè)計，使得二元域上的多元非線性多項(xiàng)式轉(zhuǎn)化為CNF形式的過程自動化，然后調(diào)用MiniSat求解器進(jìn)行求解。以歐洲eSTREAM項(xiàng)目中的Trivium算法［6］為例進(jìn)行實(shí)驗(yàn)，通過對Trivium算法的輸出多項(xiàng)式組進(jìn)行轉(zhuǎn)化求解，得到多項(xiàng)式組的一個解，從而證明了該設(shè)計的有效性。

2　相關(guān)研究

序列密碼是密碼學(xué)中一個重要的分支，具有加解密速度快、硬件實(shí)現(xiàn)簡單、錯誤擴(kuò)散率小等特點(diǎn)，因此被廣泛應(yīng)用于保密通信等領(lǐng)域。序列密碼的設(shè)計是靈活多變的，不同的算法結(jié)構(gòu)對應(yīng)著不同的分析方法。隨著密碼分析學(xué)的不斷發(fā)展、攻擊方案的不斷改進(jìn)和計算機(jī)技術(shù)的日益更新，B-M算法、相關(guān)攻擊、最佳仿射逼近攻擊和差分密碼分析技術(shù)等都可以對某些密碼進(jìn)行分析與破譯。將SAT問題求解引入密碼分析是近年來的一個研究方向［7］，促進(jìn)了密碼分析技術(shù)的發(fā)展。

2.1序列密碼分析

為了促進(jìn)序列密碼的發(fā)展，歐洲于2004年實(shí)施了eSTREAM研究項(xiàng)目，借此征集到適合廣泛采用的新的序列密碼算法，由此引發(fā)了對序列密碼分析研究的新一輪熱潮，特別是對eSTREAM項(xiàng)目候選算法的分析研究。

Trivium是最終入選的7個算法之一。雖然至今還沒有針對Trivium的非常有效的攻擊方法，但對Trivium的分析研究一直不斷。2011年，賈艷艷等［8］針對2輪Trivium算法，通過找出更多線性逼近方程對其進(jìn)行多線性密碼分析，提出了一種更為有效的區(qū)分攻擊方法。2013年，歐智慧等［9］在2輪Trivium的線性逼近研究中，針對文獻(xiàn)［8］中線性逼近方程個數(shù)少和偏差小的問題，提出通過改變第1輪Trivium所占的時鐘數(shù)和線性逼近式的方法對第2輪進(jìn)行線性逼近，在攻擊成功概率相同的前提下，所需的數(shù)據(jù)量降為原來的1/16。2012年，孫文龍等［10］針對初始化為288輪的簡化版Trivium算法進(jìn)行了線性分析，更正了Turan等給出的關(guān)于密鑰、初始化向量和密鑰流比特的表達(dá)式，同時給出了當(dāng)允許選取特殊的密鑰和初始化向量時搜索最佳線性逼近式的算法。丁林［11］在其學(xué)位論文中提出了針對Trivium的自動搜索差分路徑技術(shù)，利用該技術(shù)可以得到任意輪Trivium算法的差分路徑，證明了初始化輪數(shù)低于359的Trivium算法不能有效抵抗差分分析。隨著SAT問題求解方法研究的發(fā)展，將SAT求解運(yùn)用到Trivium算法的安全性分析中的情形也越來越多。例如，轉(zhuǎn)化為SAT問題分析Trivium的可滑動對，利用MiniSat求解器分析Trivium的變種Bivium算法［12］等。到目前為止，對Trivium的分析還在不斷進(jìn)行。

2.2SAT問題相關(guān)研究

SAT問題是指：給定一組包含n個布爾變量X1，X2，X3，…，Xn（只能為真或假）的邏輯析取范式，查找是否存在它們的一組取值組合，使得該析取范式被滿足。SAT問題是典型的NP完全問題，對它的深入研究有利于NP完全問題的解決。

關(guān)于SAT問題的算法主要有兩種：完全算法和不完全算法。完全算法能求出命題邏輯公式的解或證明公式是不可滿足的，但是效率無法滿足實(shí)際需要；不完全算法求解速度相對較快，但是不一定能找到對應(yīng)SAT問題的解。許多不完全算法都是基于局部搜索策略，其中代表性的有Selman和Kautz的GSAT算法、WALKSAT算法和NSAT算法，此外，梁東敏等對GSAT+walk的改進(jìn)算法、黃文奇等提出的擬人擬物法、凌應(yīng)標(biāo)等［13］基于子句權(quán)重學(xué)習(xí)的求解SAT問題的遺傳算法等也是重要的求解SAT問題的不完全算法。完全算法中最具代表性的是DPLL算法［14］，后續(xù)算法大多是在DPLL的基礎(chǔ)上改進(jìn)而來。當(dāng)前許多最有效的求解器如Zchaff、BerkMinl和MiniSat都是基于DPLL算法。

迄今為止，SAT問題求解已經(jīng)有很多研究成果。劉靜等［15］基于組織的概念設(shè)計了一種新的進(jìn)化算法求解SAT問題，將SAT問題分解成若干組織，然后用進(jìn)化的方式來求解SAT問題。胡顯偉等［16］提出了一種基于函數(shù)變換的求解SAT問題的新算法，利用SAT問題自身的特點(diǎn)將判定問題轉(zhuǎn)化為連續(xù)函數(shù)的求極值問題，在求解速度、成功率和求解問題的規(guī)模等方面都有明顯的提高。除此之外，還有一些優(yōu)化SAT問題輸入的預(yù)處理算法通過優(yōu)化輸入來減小SAT問題的規(guī)模，從而達(dá)到提高求解效率的目的。

2.3M iniSat求解器

MiniSat是一個性能優(yōu)異且被廣泛采用的SAT求解器，后續(xù)的許多SAT求解器都是在MiniSat的基礎(chǔ)上進(jìn)行改進(jìn)。MiniSat輸入為DIMACS格式［17］。DIMACS格式是一個簡單的cnf文本格式，其注釋行都是以“c”開始，非注釋行的第1行為運(yùn)行參數(shù)，格式為：

p cnf NUM_OF_VARIABLES NUM_OF_ CLAUSES。

其中：NUM_OF_VARIABLES表示布爾變量的個數(shù)；NUM_OF_CLAUSES表示子句的個數(shù)。

合取范式的每一個子句對應(yīng)一行，一個子句的變量用標(biāo)號表示，正值表示變量為原變量，負(fù)值表示變量為反變量，中間以空格分開，在每行結(jié)尾以0表示一個子句的結(jié)束。MiniSat求解器對輸入的合取范式進(jìn)行判定，如果輸入有可滿足解，則輸出SAT，并輸出一個解；如果不可滿足，則輸出UNSAT。

3　問題定義與分析

許多流密碼的硬件設(shè)計實(shí)現(xiàn)主要由簡單的邏輯電路組合而成，其輸出邏輯式一般只包含“異或”（用⊕表示）、“與”（用·表示）和“或”（用+表示）3種，其他形式也可轉(zhuǎn)化為這3種形式。因此，可以用A⊕B⊕C⊕D⊕E⊕F⊕…=0表示流密碼的一輪輸出多項(xiàng)式，其中A，B，C表示一個只包含“與”運(yùn)算（用·表示）或者“或”運(yùn)算（用+表示）的邏輯式，形如A=X1·X2·X3…。其他形式可以依據(jù)邏輯代數(shù)的交換律、分配律等基本定律變形為這種形式。對于該形式的邏輯代數(shù)，主要通過下面兩步轉(zhuǎn)化為CNF形式：

3.1將邏輯代數(shù)式轉(zhuǎn)化為析取子句

對于邏輯代數(shù)式A⊕B⊕C⊕D⊕E⊕F⊕…=0，等式兩邊同時取反，即A⊕B⊕C⊕D⊕E⊕F⊕…若為1，依據(jù)異或邏輯運(yùn)算規(guī)則中的反演率，可以推出A⊕B⊕C⊕D⊕E⊕F⊕…=1。要求出A⊕B⊕C⊕D⊕E⊕F⊕…=1的解，即要求等式左邊A⊕B⊕C⊕D⊕E⊕F⊕…為真，因此可將其轉(zhuǎn)化為CNF形式，通過MiniSat求可滿足解使邏輯式A⊕B⊕C⊕D⊕E⊕F⊕…恒為真。

將形如A⊕B⊕C⊕D⊕E⊕F⊕…的式子轉(zhuǎn)化為CNF形式，只需將其展開為邏輯代數(shù)的最大項(xiàng)表達(dá)式即可。由真值表得出邏輯代數(shù)的最大項(xiàng)表達(dá)式，只需將真值表中使函數(shù)值為0的各個最大項(xiàng)相與便可。因A⊕B⊕C⊕D⊕E⊕F⊕…為多項(xiàng)異或運(yùn)算，即模二加運(yùn)算，若使其值為0，則要求參與異或的各項(xiàng)中值取1的項(xiàng)為偶數(shù)項(xiàng)，而最大項(xiàng)中反變量表示1，原變量表示0，即要求參與異或的各項(xiàng)中取反的項(xiàng)為偶數(shù)項(xiàng)（A視為一個原變量整體）。

因此，從A、B、C、D…這些邏輯代數(shù)的異或項(xiàng)中選取偶數(shù)個項(xiàng)，并對選出的項(xiàng)取反，然后將所有項(xiàng)進(jìn)行“或”運(yùn)算，即可得到一個析取子句，如選取A、B這兩項(xiàng)取反，可得一個析取子句為A+B+C+ D+E+F+…，即A+B+C+D+E+F+…。依次對所有項(xiàng)選取偶數(shù)個項(xiàng)，當(dāng)所有偶數(shù)個項(xiàng)都選取到之后，將得到的析取子句用與運(yùn)算連接起來，既可得到A⊕B⊕C⊕D⊕E⊕F⊕…的CNF形式。

3.2化簡析取子句為合取范式析取項(xiàng)

以上得到的析取子句并不是合取范式的析取項(xiàng)，因?yàn)锳，B，C等項(xiàng)中還包含有“與”運(yùn)算或是“或”運(yùn)算，需要進(jìn)一步化簡。對于“或”運(yùn)算，如果該項(xiàng)（如A=X1+X2+X3）為原變量，即為（A+ B+C+D+…）形式，依據(jù)邏輯函數(shù)的結(jié)合律，在析取子句中不需化簡，為（X1+X2+X3+B+C+ D+…）；對于“與”運(yùn)算，如果該項(xiàng)（如A=X1· X2·X3）為反變量，即為（A+B+C+D+…）形式，則依據(jù)反演率和結(jié)合律，A=X1·X2·X3= X1+X2+X3，再按或運(yùn)算代入其中得到（X1+ X2+X3+B+C+D+…）。

對于析取子句中原變量項(xiàng)中含有“與”運(yùn)算，或是反變量項(xiàng)中含有“或”運(yùn)算的，先將反變量項(xiàng)中的“或”運(yùn)算通過反演率和結(jié)合律轉(zhuǎn)變?yōu)椤芭c”運(yùn)算，如A=X1+X2+X3=X1·X2·X3。設(shè)計一個模塊，對析取子句中含有的“與”運(yùn)算進(jìn)行轉(zhuǎn)化。依據(jù)邏輯代數(shù)的分配率A+BC=（A+B）（A+C），將A=X1·X2·X3…Xn形式的與項(xiàng)代入，得到n個析取項(xiàng)。

通過以上兩步，可將一個邏輯代數(shù)式轉(zhuǎn)化為CNF形式，而后調(diào)用MiniSat求解器對CNF從句求解，得到的可滿足解就是邏輯代數(shù)式的解。

4　算法設(shè)計與實(shí)現(xiàn)

要將邏輯代數(shù)式轉(zhuǎn)化為CNF形式，主要通過設(shè)計3個模塊完成：mcnf模塊、combination模塊和split模塊。由于需要轉(zhuǎn)化的邏輯代數(shù)式為字符串形式，故先對其進(jìn)行適當(dāng)?shù)奶幚?。mcnf模塊先將邏輯代數(shù)式進(jìn)行適當(dāng)變形化簡，以適應(yīng)combination模塊的輸入；combination模塊主要是對所有異或項(xiàng)選取偶數(shù)項(xiàng)并取反，對于非標(biāo)準(zhǔn)合取范式中的析取項(xiàng)，調(diào)用split模塊進(jìn)行最后的處理。算法主要流程如圖1所示。

圖1　算法主要流程

4.1m cn f模塊

mcnf模塊的主要功能是將輸入的字符串形式的邏輯代數(shù)式按照異或運(yùn)算符分成一個個單獨(dú)的項(xiàng)，并依據(jù)異或運(yùn)算的重疊率和自等率將重復(fù)偶數(shù)次的項(xiàng)刪除，得到的結(jié)果作為后面模塊的輸入，調(diào)用combination模塊對異或項(xiàng)選取偶數(shù)項(xiàng)取反變量。算法偽碼描述如下：

1）讀入一個表示邏輯代數(shù)的字符串。

2）對字符串第1個字符至最后一個字符進(jìn)行判斷：①如果字符為“+”，存放字符的數(shù)組下標(biāo)加1并判斷下一個字符；②如果字符不為“+”，將字符放入數(shù)組中并判斷下一個字符。

3）從數(shù)組第1個元素開始比較，將兩個相同的元素重新賦值為“NULL”。

4）將數(shù)組中為“NULL”的元素移至數(shù)組最后。

5）對數(shù)組元素調(diào)用combination模塊取偶數(shù)項(xiàng)。

6）結(jié)束。

4.2 com bination模塊

combination模塊的功能是從輸入的異或項(xiàng)數(shù)組中選取偶數(shù)項(xiàng)并對其取反。定義一個vector結(jié)構(gòu)變量vecOrder用以存儲數(shù)組下標(biāo)，然后通過對下標(biāo)的取值來確定數(shù)組中的元素。例如，要從n個元素中取m個，則先取下標(biāo)為0，1，2，3…（m-1）的元素，然后從下標(biāo)數(shù)組的最右邊一個開始加1，即下一組為取下標(biāo)為0，1，2…（m-2），m的元素，直到取到下標(biāo)為0，1，2…（m-2），（n-1）的一組元素。之后將下標(biāo)數(shù)組的右邊起第2個加1，并重復(fù)上面過程，直至所有情況都被選出為止。偽代碼描述如下：

1）輸入一個字符串?dāng)?shù)組X［］、數(shù)組元素個數(shù)n和需取反的項(xiàng)數(shù)m。

2）定義一個整型vector變量vecOrder并初始化為1，2，…，m，定義變量position并賦值為（m-1）以標(biāo)識位置。

3）將數(shù)組中下標(biāo)為vecOrder的元素的項(xiàng)取出并取反，然后和數(shù)組中剩下的項(xiàng)一起組成一個字符串，調(diào)用split模塊。

4）如果vecOrder中的第1個元素為（n-m+ 1）（即取到了數(shù)組中的最后m個元素），跳至步驟7）。

5）如果vecOrder中的最后一個元素不為n且vecOrder中前面的元素都比后面的元素小，則將vecOrder中的最后一個元素加1并跳至步驟3）。

6）如果vecOrder中的最后一個元素為n，將position減1，即將標(biāo)識位置向左移一位，將position位置及其右邊的值都加1并跳至步驟5）。

7）結(jié)束。

4.3split模塊

split模塊的功能是將輸出的析取子句中的與項(xiàng)利用分配率拆分成標(biāo)準(zhǔn)的析取項(xiàng)。對于輸入的帶*的字符串，以*和空格為判斷符，將字符串拆分成兩部分，并遞歸調(diào)用，直至字符串中不含*符號。輸出的不含*的字符串即為DIMACS格式的輸入。其偽代碼為：

輸入：帶有與運(yùn)算（*）的析取子句字符串

輸出：標(biāo)準(zhǔn)的DIMACS格式文件

split（string X）

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

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

1.2否則將字符串分成兩部分：

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

分加“*”后面第1個空格之后的部分，再調(diào)用split；

1.2.2字符串中第1個“*”前面第1個空格之前的部分加“*”之后的部分，再調(diào)用split；

2.結(jié)束。

5　實(shí)驗(yàn)及結(jié)果分析

為了驗(yàn)證設(shè)計的正確性和分析轉(zhuǎn)化的效率，本文以Trivium算法為例進(jìn)行實(shí)驗(yàn)。Trivium是進(jìn)入歐洲eSTREAM計劃最終方案的一個序列密碼算法。算法分為兩部分：第1部分為初始化階段，利用80位密鑰和80位初始化向量將288位內(nèi)部狀態(tài)進(jìn)行初始化，在前4×288輪循環(huán)中，算法不輸出密鑰流；第2部分為密鑰流生成階段，在4× 288輪循環(huán)之后生成用于加密的密鑰流Zi。其算法偽代碼描述如下：

本文主要對初始化階段產(chǎn)生的多項(xiàng)式組進(jìn)行實(shí)驗(yàn)。

5.1實(shí)驗(yàn)運(yùn)行環(huán)境

實(shí)驗(yàn)中的mcnf模塊、combination模塊和split模塊主要基于Windows下的VC++6.0環(huán)境編譯運(yùn)行，運(yùn)行平臺為32位Windows XP，硬件配置為AMD Athlon（tm）Dual Core Processor CPU 2.71 GHz，2G運(yùn)行內(nèi)存。CNF求解時，在同一臺機(jī)器上的VMWare虛擬機(jī)中創(chuàng)建Ubuntu系統(tǒng)，在Ubuntu系統(tǒng)下運(yùn)行MiniSat求解。

5.2實(shí)驗(yàn)過程

實(shí)驗(yàn)中，首先對Trivium密碼初始化過程中的前93輪輸出多項(xiàng)式進(jìn)行轉(zhuǎn)化，其輸出多項(xiàng)式為：

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下編譯運(yùn)行，利用3個模塊轉(zhuǎn)化后得出的結(jié)果為：

-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個，程序運(yùn)行時間為477 s，輸出文件大小為120 M。在Ubuntu系統(tǒng)下通過./minisat〈cnf-file〉〈out-file〉調(diào)用MiniSat求解，經(jīng)過3.5 s即求出了一個可滿足解，見圖2。

對Trivium初始化過程中的第94～111輪輸出多項(xiàng)式進(jìn)行轉(zhuǎn)化，得到的輸出文件共有子句8 957 970個，程序運(yùn)行時間為3 033 s，輸出文件大小為720 M。使用MiniSat在9.76 s后得到一個可滿足解。

圖2　一個可滿足解

5.3結(jié)果分析

通過上面的結(jié)果可以看到：該算法在Trivium前93輪和第94～111輪都能很好地轉(zhuǎn)化為CNF形式，并通過Ubuntu系統(tǒng)中的MiniSat求解，得出可滿足解。但是從運(yùn)行時間和轉(zhuǎn)化的規(guī)模上來看，隨著循環(huán)次數(shù)的增加，多項(xiàng)式中項(xiàng)數(shù)越來越多，轉(zhuǎn)化后的子句數(shù)也越來越多，程序運(yùn)行時間變長。通過分析，在Trivium算法的初始化階段，去除重復(fù)項(xiàng)后到第122輪時，其多項(xiàng)式中有20項(xiàng)，可產(chǎn)生的子句數(shù)至少是220-1個；到第200輪時，多項(xiàng)式中有53項(xiàng)，可產(chǎn)生的子句數(shù)至少是253-1個，程序無法在短時間內(nèi)成功轉(zhuǎn)換。因此，減少多項(xiàng)式的項(xiàng)數(shù)是下一步算法改進(jìn)的主要方向。

6　結(jié)束語

本文設(shè)計并實(shí)現(xiàn)了基于MiniSat的多元非線性多項(xiàng)式自動求解算法，可在二元域內(nèi)將多元非線性多項(xiàng)式自動轉(zhuǎn)化為CNF形式，進(jìn)而調(diào)用Mini-Sat求出方程組的解。本文算法適用于對流密碼代數(shù)攻擊的分析，降低了分析過程中方程組的求解難度。

針對轉(zhuǎn)換過程中CNF子句個數(shù)規(guī)模較大的問題，下一步的主要工作包括：①考慮通過引進(jìn)一定數(shù)量的新變元替換方程組中出現(xiàn)頻率較高的多項(xiàng)式，從而減少方程組中單項(xiàng)式個數(shù)，達(dá)到進(jìn)一步減小CNF子句規(guī)模的目的；②參考文獻(xiàn)［18］中的方法，引進(jìn)新變元化簡方程組中的非線性項(xiàng)，或是綜合考慮方程組之間的關(guān)系，通過猜測一定數(shù)量的變量的值將方程組中的一些非線性項(xiàng)轉(zhuǎn)變?yōu)榫€性項(xiàng)，簡化方程；③調(diào)用不同的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求解器在電路故障診斷中的應(yīng)用［J］.電氣電子教學(xué)學(xué)報，2013，35（6）：60-62.

［4］戴江海，戚文峰.利用一種SAT問題全解算法求Trivium可滑動對［J］.信息工程大學(xué)學(xué)報，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］金海榮.混沌序列密碼分析及應(yīng)用研究［D］.哈爾濱：黑龍江大學(xué)，2009.

［8］賈艷艷，胡予濮，楊文峰，等.2輪Trivium的多線性密碼分析［J］.電子與信息學(xué)報，2011，33（1）：223-227.

［9］歐智慧，趙亞群.2輪Trivium的線性逼近研究［J］.計算機(jī)工程，2013，39（11）：32-40.

［10］孫文龍，關(guān)杰，劉建東.針對簡化版Trivium算法的線性分析［J］.計算機(jī)學(xué)報，2012，35（9）：1890-1896.

［11］丁林.序列密碼初始化算法的安全性分析［D］.鄭州：解放軍信息工程大學(xué)，2012.

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

［13］凌應(yīng)標(biāo)，吳向軍，姜云飛.基于子句權(quán)重學(xué)習(xí)的求解SAT問題的遺傳算法［J］.計算機(jī)學(xué)報，2005，28（9）：1476-1482.

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

［15］劉靜，鐘偉才，劉芳，等.組織進(jìn)化算法求解SAT問題［J］.計算機(jī)學(xué)報，2004，27（10）：1422-1428.

［16］胡顯偉，任世軍.基于函數(shù)變換的求解SAT問題的新算法［J］.智能計算機(jī)與應(yīng)用，2012（3）：33-39.

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

［18］孫文龍，關(guān)杰.針對Trivium型密碼算法的代數(shù)攻擊［J］.上海交通大學(xué)學(xué)報，2014，48（10）：1434-1439.

（責(zé)任編輯楊黎麗）

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

國防科技大學(xué)預(yù)研項(xiàng)目；國家自然科學(xué)基金資助項(xiàng)目（61271252，61272010）

鄒湘景（1986—），男，湖南岳陽人，碩士研究生，主要從事計算機(jī)網(wǎng)絡(luò)信息安全研究；彭偉（1973—），男，研究員，主要從事計算機(jī)網(wǎng)絡(luò)和網(wǎng)絡(luò)安全研究。

鄒湘景，彭偉.基于MiniSat的多項(xiàng)式方程組求解實(shí)現(xiàn)［J］.重慶理工大學(xué)學(xué)報：自然科學(xué)版，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.