潘　進(jìn)， 王小明， 謝青松

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

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

潘進(jìn)1， 王小明2， 謝青松1

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

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

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

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

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

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

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

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

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

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

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

設(shè)邏輯規(guī)則

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

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

定義1對(duì)于兩個(gè)帶有變量的事實(shí)Fi和Fj，若存在一個(gè)變量替換σ使得

σFi=Fj，

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

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

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

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

σC1=C2,σH1?H2,

則稱R1蘊(yùn)含R2，記為R1?R2。

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

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

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

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

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

圖1　合一化規(guī)則

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

性質(zhì)1如果邏輯規(guī)則R′?R，且一個(gè)邏輯推導(dǎo)樹(shù)的節(jié)點(diǎn)η被標(biāo)記為R，那么節(jié)點(diǎn)η也可被標(biāo)記為R′。

證明假設(shè)H為邏輯樹(shù)節(jié)點(diǎn)η的所有出邊集合，C為它的一個(gè)入邊，節(jié)點(diǎn)η被標(biāo)記為R，則有

R?H→C。

又因?yàn)?/p>

R′?R，

所以

R′?H→C，

則節(jié)點(diǎn)η也可被標(biāo)記為R′。

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

R′=H′→C′，

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

由于

因此η′存在一個(gè)出邊為σF0，假設(shè)這條邊的終點(diǎn)為節(jié)點(diǎn)η，且η被標(biāo)記為

R=H→C。

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

R?H1→σF0。

由此可擴(kuò)展替換因子σ使得

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

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

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

又因?yàn)?/p>

因此，可以得出

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

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

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

R=H→C，

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

σF=F′，

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

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

R=H→C，

則稱

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

集合S通常是與攻擊者的能力和知識(shí)有關(guān)的一個(gè)邏輯事實(shí)集合，fS(R)表示規(guī)則R假設(shè)中被選擇出來(lái)進(jìn)行S事實(shí)推導(dǎo)的假設(shè)。

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

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

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

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

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

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

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

3精簡(jiǎn)集合的等價(jià)性證明

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

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

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

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

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

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

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

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

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

4結(jié)語(yǔ)

引入基于攻擊者能力和先驗(yàn)知識(shí)的事實(shí)集合S,對(duì)表述協(xié)議及其安全屬性的初始規(guī)則集合B0進(jìn)行精簡(jiǎn)，可得具有等價(jià)推導(dǎo)能力的規(guī)則集合B1。由于B1中規(guī)則的假設(shè)都屬于S，而實(shí)際應(yīng)用中S很小，所以，精簡(jiǎn)算法可提高推導(dǎo)效率，改善推理算法的收斂性。

參考文獻(xiàn)

[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]潘進(jìn),顧香,王小明.基于應(yīng)用Pi演算的WTLS握手協(xié)議建模與分析[J/OL].西安郵電大學(xué)學(xué)報(bào), 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]徐軍.關(guān)于秘密共享方案在應(yīng)用Pi演算中的實(shí)現(xiàn)[J/OL].計(jì)算機(jī)應(yīng)用.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]李夢(mèng)君.安全協(xié)議形式化驗(yàn)證技術(shù)的研究與實(shí)現(xiàn)[D].長(zhǎng)沙:國(guó)防科技大學(xué),2005:93-105.

[7]周倜.復(fù)雜安全協(xié)議的建模與驗(yàn)證[D].長(zhǎng)沙:國(guó)防科技大學(xué),2008:95-113.

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

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

[責(zé)任編輯:瑞金]

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

基金項(xiàng)目：國(guó)家自然科學(xué)基金資助項(xiàng)目(61305083)

作者簡(jiǎn)介：潘 進(jìn)(1959-)，男，博士，教授，博導(dǎo)，從事網(wǎng)絡(luò)安全研究。E-mail:2373242787@qq.com 王小明(1982-)，男，碩士研究生，研究方向?yàn)榫W(wǎng)絡(luò)安全與防護(hù)。E-mail:279804359@qq.com

中圖分類(lèi)號(hào)：TP393

文獻(xiàn)標(biāo)識(shí)碼：A

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