密碼協議形式化分析中的邏輯規則精簡

潘　進， 王小明， 謝青松

(1.西安通信學院 信息安全系, 陜西 西安 710106;　2.西安通信學院 12隊, 陜西 西安 710106)

密碼協議形式化分析中的邏輯規則精簡

潘進1， 王小明2， 謝青松1

(1.西安通信學院 信息安全系, 陜西 西安 710106;2.西安通信學院 12隊, 陜西 西安 710106)

摘要:針對密碼協議形式化分析中初始規則集過大且不易收斂的問題，給出一種基于先驗知識集進行邏輯規則精簡的方法。在初始規則迭代過程中，使用等價邏輯樹理論進行規則集的蘊含和合一化處理，縮小初始規則集，并使形成的新的邏輯規則集具有與初始規則集等價的推導能力。

關鍵詞:形式化驗證；初始規則集；規則蘊含；規則合一化

分析密碼協議的安全性，有攻擊檢測和形式化分析兩種方法。攻擊檢測直觀且易于理解，但運用中帶有很大的偶然性和不確定性。形式化分析方法具有理論完備、廣泛適用、結論可靠的特點，是當前的研究熱點。

經歷基于知識和信念的模態邏輯理論[1]以及以通信序列進程為代表的模型檢測理論[2]之后，對形式化分析方法的關注被更多地集中在包括π演算和串空間理論在內的定理證明方法上[3]。

以π演算為代表的進程演算，理論上是一種進程代數，是交互和并發系統的理論模型，能夠以接近協議本身的語言來描述協議，精確刻畫協議運行過程和運行環境，特別適合于密碼協議的建模[4-5]，但進程演算的協議表述并不利于機器理解和推理，需要將其轉換成便于機器理解和推理的協議邏輯規則表述。

對協議進程演算模型進行機器自動轉換所得到的協議邏輯表述，往往是一個較為龐大并包括大量冗余信息的規則集，在其上直接進行安全屬性推導，不僅計算效率低，甚至會導致不收斂問題。

利用不動點迭代發散的充分條件對不停機進行預測[6-7]，采用預先設定最大搜索深度、最大加密層次可以強制停機，或者通過空間剪枝規則限制狀態搜索空間，也可緩解狀態空間爆炸問題[8-9]，但初始集龐大而冗余的問題在理論上并沒有得到解決。

本文基于攻擊者的能力和知識，擬采用等價邏輯推導樹方法對初始規則集進行蘊含與合一化精簡，以使推理過程中的狀態空間得到實質性壓縮。

1邏輯規則的蘊含與合一化

Horn邏輯既能等價表述進程演算的語法、語義，又易于被計算機理解。依據各種理論建模的密碼協議往往被轉換成Horn邏輯表述，然后再對邏輯規則集合進行自動化推導。關于規則集合的精簡問題只需針對Horn邏輯討論即可。

設邏輯規則

R=H→C=F1∧F2∧…∧Fn，

其中H是規則的假設，C是規則的結論,Fi(i=1,2,…,n)表示H中的事實，一般是關于Horn邏輯中變量、名稱或函數的謂語。

定義1對于兩個帶有變量的事實Fi和Fj，若存在一個變量替換σ使得

σFi=Fj，

則稱Fi和Fj是可合一化的，并稱σ為合一化因子。

定義2設有兩條邏輯規則

R1=H1→C1,R2=H2→C2,

其中H1和H2為多重假設。如果存在合一化因子σ，使得

σC1=C2,σH1?H2,

則稱R1蘊含R2，記為R1?R2。

定義3設有兩條邏輯規則

R=H→C,R′=H′→C′,

如果存在F0∈H′，使得C和F0能夠合一化，且σ為C和F0的最一般合一化因子，則存在新的合一化規則

R。F0R′=σ[H∪(H′{F0})]→σC′。

對合一化規則持續進行合一化，可不斷推導出新規則，形成邏輯推導樹。用η、η′和η″等表示邏輯推導樹的節點，則合一化過程可表示如圖1。

圖1　合一化規則

根據邏輯推導樹的相關理論，定義2中給出的蘊含概念和定義3中給出的合一化規則分別具有如下性質。

性質1如果邏輯規則R′?R，且一個邏輯推導樹的節點η被標記為R，那么節點η也可被標記為R′。

證明假設H為邏輯樹節點η的所有出邊集合，C為它的一個入邊，節點η被標記為R，則有

R?H→C。

又因為

R′?R，

所以

R′?H→C，

則節點η也可被標記為R′。

證明假設邏輯規則

R′=H′→C′，

因此，存在合一化因子σ使得

由于

因此η′存在一個出邊為σF0，假設這條邊的終點為節點η，且η被標記為

R=H→C。

重新定義R中的變量，與R′中的變量進行區分。假設H1為節點η所有出邊的集合，則可以得出

R?H1→σF0。

由此可擴展替換因子σ使得

σH?H1,σC′=σF0。

節點η′到節點η的邊被標記為σF0，它為F0的一個實例。根據σC′=σF0，事實C和F0可以進行合一化，故可定義新規則R。F0R′。假設σ′為C和F0的最一般合一化因子，并定義σ=σ″σ′,則有

R。F0R′=σ′[H∪(H′{F0})]→σ′C′。

又因為

因此，可以得出

2邏輯規則精簡算法

為了對安全屬性有針對性地精簡邏輯規則集，需要討論相對于邏輯事實集合的選擇函數。

定義4設有邏輯事實集合S，邏輯規則

R=H→C，

H中的事實F∈H。如果存在一個事實F′∈S和一個合一化因子σ，使得

σF=F′，

則稱F合一化屬于S，記為F∈rS。

定義5設有邏輯事實集合S，邏輯規則

R=H→C，

則稱

為關于事實S的選擇函數。

集合S通常是與攻擊者的能力和知識有關的一個邏輯事實集合，fS(R)表示規則R假設中被選擇出來進行S事實推導的假設。

設密碼協議及其攻擊者的進程演算模型已轉換成初始規則集B0，其中包含描述攻擊者攻擊能力與知識的事實集合S。規則精簡的目的就是要得到一個較小的邏輯集合B1，使得B1與B0具有等價的推導能力。所謂等價是指，在對所考慮的秘密性、認證性、匿名性等安全屬性進行驗證時，兩個集合推導出的結論是完全相同的。精簡結果與所考慮的安全屬性有關，與攻擊者的知識和能力有關。

邏輯規則精簡算法的流程如圖2所示,具體描述如下。

步驟1對于規則集B0中的每條規則R，判斷是否對于R1∈B，有R1?R。若是，去除規則R；否則，將R加入規則集B中。

步驟2按步驟1處理完規則集B0中的每條規則后，依據選擇函數是否為空將規則集B中的規則分成B′和B″兩類，其中規則集B′中的每條邏輯規則都使選擇函數為空，而規則集B″中的每條邏輯規則都使選擇函數非空。

步驟3將規則集B′中的邏輯規則R′與規則集B″中的邏輯規則R″進行合一化處理，并將得到的新規則R′。F0R″進行優化和蘊含處理后，再加入規則集B中，直至規則集B′和規則集B″中的規則不能進行合一化，出現不動點。

步驟4去除規則集B中選擇函數不為空的規則，剩下的規則集合就是精簡后的邏輯規則集B1。

圖2　邏輯規則精簡流程

3精簡集合的等價性證明

依照邏輯規則精簡算法得出精簡集合B1后，還需證明它與初始規則集B0的推理等價性。

定理1若B1是邏輯規則精簡算法得出的邏輯規則集，則B1與初始規則集B0具有等價的推導能力。

證明假設事實F可從規則集B0推導得到，則關于B0存在一個邏輯推導樹D0,由它可推導出F。若B1與B0具有等價的推導能力，則事實F也可從規則集B1中的規則推導得到，即關于B1也存在一個邏輯推導樹，能推導出F。

根據算法的步驟1可知，除去被規則集B蘊含的規則，B0中其他規則都被加入了規則集B中，所以模塊處理結束時，規則集B0中所有的規則都被規則集B的某一規則所蘊含。根據性質1，標記邏輯樹D0節點的所有規則都可以用B中的規則來代替，則關于B存在一個邏輯推導樹D可推導出F。

若邏輯樹D中存在標記節點的規則不在B1中，進行如下轉換。假設標記節點η′的規則R′不在B1中，且η′是D中最低的節點，則標記η′所有子節點的規則都在B1中。因R′?B1，故fS(R′)≠?。假設F0∈fS(R′)，根據性質2，如果節點η′存在一個子節點η，被標記為R，則可定義R。F0R′,從而可用標記為R。F0R′的節點η″代替節點η和η′。由于η′的所有子節點都被B1中的規則R標記，則fS(R)=?。由步驟3可知，由B中規則合一化所得的規則R。F0R′除了被規則集B蘊含的，都加入了規則集B中，所以規則合一化所得的規則都被規則集B的某一規則R″所蘊含。根據性質1，可將節點η″標記為R″。由于節點η″代替了節點η和η′，所以邏輯樹節點的總數將減少，即關于B存在一個邏輯樹D′可推導出F，其節點總數有所減少。

由于在規則進行合一化處理時，需要滿足

fS(R)=?,fS(R′)≠?,

故在實際應用中，一般每次驗證時只關注協議的個別安全屬性，經過蘊含去除和優化后，S不僅是有限集，而且只有很少幾個邏輯事實。

經過有限次蘊含去除和優化迭代后，標記邏輯樹節點的所有規則都屬于規則集B1，從而得到關于B1的一個邏輯推導樹可推導出F。

4結語

引入基于攻擊者能力和先驗知識的事實集合S,對表述協議及其安全屬性的初始規則集合B0進行精簡，可得具有等價推導能力的規則集合B1。由于B1中規則的假設都屬于S，而實際應用中S很小，所以，精簡算法可提高推導效率，改善推理算法的收斂性。

參考文獻

[1]ABADIM,TUTTLEMR.ASemanticsforaLogicofAuthentication[C]//PODC’91ProceedingsoftheTenthAnnualACMSymposiumonPrinciplesofDistributedComputing.NewYork:ACM, 1991: 201-216.DOI:10.1145/112600.112618.

[2]MEADOWSC.TheNRLProtocolAnalyzer:AnOverview[J].JournalofLogicProgramming, 1996, 26(2): 113-131.DOI:10.1016/0743-1066(95)00095-X.

[3]SONGXD,BEREZINS,PERRIGA.Athena：anovelapproachtoefficientautomaticsecurityprotocolanalysis[J].JournalofComputerSecurity, 2001, 9(1/2): 47-74.

[4]潘進,顧香,王小明.基于應用Pi演算的WTLS握手協議建模與分析[J/OL].西安郵電大學學報, 2015, 20(2):26-31[2015-10-20].http://www.cnki.com.cn/Article/CJFDTotal-XAYD201502007.htm.DOI:10.13682/j-issn.2095-6533.2015.02.006.

[5]徐軍.關于秘密共享方案在應用Pi演算中的實現[J/OL].計算機應用.2013.33(11):3247-3251[2015-10-20].http://www.cnki.com.cn/Article/CJFDTotal-JSJY201311062.htm.DOI:10.11772/j.issn.1001-9081.2013.11.3247.

[6]李夢君.安全協議形式化驗證技術的研究與實現[D].長沙:國防科技大學,2005:93-105.

[7]周倜.復雜安全協議的建模與驗證[D].長沙:國防科技大學,2008:95-113.

[8]劉學鋒,石昊,蘇薛銳,等.安全協議自動驗證工具的狀態空間剪枝[J/OL].計算機應用,2004, 24(8):117-121[2015-10-20].http://d.wanfangdata.com.cn/Periodical/jsjyy200408037.

[9]石昊蘇,薛銳,馮登國.AVSP算法[J/OL].計算機工程與設計,2005,26(4):867-869[2015-10-20].http://www.cnki.com.cn/Article/CJFDTotal-SJSJ200504008.htm.

[責任編輯:瑞金]

Logicalrulessimplificationfortheformalanalysisofcryptographicprotocols

PANJin1,WANGXiaoming2,XIEQingsong1

(1.DepartmentofInformationSecurity,Xi’anCommunicationsInstitute,Xi’an710106China；2.Teamof12th,Xi’anCommunicationsInstitute,Xi’an710106China)

Abstract:Aiming to solve the problem that the initial rule set in the formal analysis of cryptographic protocols is too large to converge, a new method is put forward to streamline the logical rules based on prior knowledge. Using equivalent logic tree theory, the rule set can be implicated and unified in initial rule iteration process, which makes the new logical rule set have the same capacity as the initial one that has not been deflated.

Keywords:formal verification tools, initial rules sets, implication rule, rule of the unifying

doi:10.13682/j.issn.2095-6533.2016.02.003

收稿日期：2015-11-30

基金項目：國家自然科學基金資助項目(61305083)

作者簡介：潘 進(1959-)，男，博士，教授，博導，從事網絡安全研究。E-mail:2373242787@qq.com 王小明(1982-)，男，碩士研究生，研究方向為網絡安全與防護。E-mail:279804359@qq.com

中圖分類號：TP393

文獻標識碼：A

文章編號：2095-6533(2016)02-0016-04