潘　進， 王小明， 謝青松

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

密碼協(xié)議形式化分析中的邏輯規(guī)則精簡

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

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

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

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

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

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

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

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

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

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

1邏輯規(guī)則的蘊含與合一化

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

設邏輯規(guī)則

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

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

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

σFi=Fj，

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

定義2設有兩條邏輯規(guī)則

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

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

σC1=C2,σH1?H2,

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

定義3設有兩條邏輯規(guī)則

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

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

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

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

圖1　合一化規(guī)則

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

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

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

R?H→C。

又因為

R′?R，

所以

R′?H→C，

則節(jié)點η也可被標記為R′。

證明假設邏輯規(guī)則

R′=H′→C′，

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

由于

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

R=H→C。

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

R?H1→σF0。

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

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

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

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

又因為

因此，可以得出

2邏輯規(guī)則精簡算法

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

定義4設有邏輯事實集合S，邏輯規(guī)則

R=H→C，

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

σF=F′，

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

定義5設有邏輯事實集合S，邏輯規(guī)則

R=H→C，

則稱

為關于事實S的選擇函數(shù)。

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

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

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

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

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

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

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

圖2　邏輯規(guī)則精簡流程

3精簡集合的等價性證明

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

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

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

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

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

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

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

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

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

4結語

引入基于攻擊者能力和先驗知識的事實集合S,對表述協(xié)議及其安全屬性的初始規(guī)則集合B0進行精簡，可得具有等價推導能力的規(guī)則集合B1。由于B1中規(guī)則的假設都屬于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握手協(xié)議建模與分析[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演算中的實現(xiàn)[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]李夢君.安全協(xié)議形式化驗證技術的研究與實現(xiàn)[D].長沙:國防科技大學,2005:93-105.

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

[8]劉學鋒,石昊,蘇薛銳,等.安全協(xié)議自動驗證工具的狀態(tài)空間剪枝[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-)，男，博士，教授，博導，從事網(wǎng)絡安全研究。E-mail:2373242787@qq.com 王小明(1982-)，男，碩士研究生，研究方向為網(wǎng)絡安全與防護。E-mail:279804359@qq.com

中圖分類號：TP393

文獻標識碼：A

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