基于事件邏輯的WMN客戶端與LTCA認(rèn)證協(xié)議安全性分析

肖美華 李婭楠,2 宋佳雯 王西忠 李 偉 鐘小妹

1(華東交通大學(xué)軟件學(xué)院 南昌 330013)2(中國鐵建重工集團(tuán)有限公司 長沙 410100)

網(wǎng)絡(luò)發(fā)展給世界帶來巨大變化，人們的日常生活離不開信息科技.信息在安全信道傳輸會遇到各種攻擊，如消息竊聽、消息攔截、消息篡改[1]等.網(wǎng)絡(luò)安全問題是全球性問題，2017年3月，維基解密(WiKiLeaks)公布數(shù)千份資料，其中揭秘一些黑客入侵事件[2]，不法組織不僅入侵iPhone手機(jī)、Android手機(jī)、智能電視，還攻擊操作系統(tǒng)獲取機(jī)密文件,甚至控制智能汽車發(fā)起暗殺活動[3].同年5月，在全球范圍內(nèi)爆發(fā)“WannaCry”比特幣勒索病毒，結(jié)合蠕蟲方式[4]進(jìn)行傳播，利用MS17-010漏洞向用戶的445端口發(fā)送數(shù)據(jù)包，遠(yuǎn)程執(zhí)行代碼后加密用戶文件，并釋放一個壓縮包，壓縮包中文件隱藏釋放到本地目錄，文件中毒后被加密鎖死.對150多個國家和地區(qū)、10多萬組織和機(jī)構(gòu)以及30多萬網(wǎng)民產(chǎn)生惡劣影響，損失高達(dá)500多億人民幣.

無線Mesh網(wǎng)(wireless mesh network，WMN)[5-6]擁有固定且電源充足的主干路由器，設(shè)計時不需要考慮太多能耗和移動性問題，適合投放于覆蓋大面積開放區(qū)域.認(rèn)證技術(shù)[7]在有線網(wǎng)絡(luò)中比較成熟，但是在無線網(wǎng)絡(luò)中由于存儲設(shè)備、帶寬等限制因素使其發(fā)展相對困難，無線網(wǎng)絡(luò)面臨比常規(guī)有線網(wǎng)絡(luò)更嚴(yán)重復(fù)雜的威脅，如何構(gòu)建合理的WMN認(rèn)證體系很是關(guān)鍵.認(rèn)證是安全通信的基礎(chǔ)，通過機(jī)密消息對移動節(jié)點身份進(jìn)行認(rèn)定，只有經(jīng)過認(rèn)證的節(jié)點才能訪問網(wǎng)絡(luò)資源[8].

形式化方法通過嚴(yán)格數(shù)學(xué)概念和邏輯方法對協(xié)議進(jìn)行描述，語義清晰、無歧義，可以發(fā)現(xiàn)其他方法不易被發(fā)現(xiàn)的網(wǎng)絡(luò)安全協(xié)議漏洞[9].定理證明描述并發(fā)與分布式系統(tǒng)，是一種協(xié)議和算法的邏輯，側(cè)重協(xié)議正確性，難以自動化[10].定理證明將協(xié)議描述為公理系統(tǒng)，協(xié)議安全目標(biāo)表示需要證明的定理，協(xié)議是否滿足安全目標(biāo)對應(yīng)于公理系統(tǒng)中目標(biāo)定理是否成立，可用于無限狀態(tài)空間協(xié)議正確性證明[11].事件邏輯(logic of events theory， LoET)[12]是定理證明的一種邏輯方法，用來刻畫加密協(xié)議在交互過程中的消息動作.肖美華等人[13-15]合作運(yùn)用事件邏輯理論對安全協(xié)議進(jìn)行形式化分析工作，克服協(xié)議組合邏輯PCL在協(xié)議分析過程中存在的不足.

1 WMN客戶端與LTCA認(rèn)證協(xié)議

輕量級動態(tài)容侵證書授權(quán)中心(lite and tolerate certificate authority, LTCA)認(rèn)證機(jī)制結(jié)合門限密碼思想與輕量級公鑰體制[8]，并支持WMN基礎(chǔ)設(shè)施，相較于MANET及WSN的節(jié)點資源豐富[16].

本文在研究通信雙方交互過程中進(jìn)行5點假設(shè)：

1) 隨機(jī)數(shù)是新鮮的，移動用戶不生成相同隨機(jī)數(shù)；

2) 以多跳形式經(jīng)過中間轉(zhuǎn)發(fā)的用戶節(jié)點忽略不計；

3) 不存在任何值得注意的網(wǎng)絡(luò)延遲現(xiàn)象；

4) 無線網(wǎng)絡(luò)環(huán)境包括非法Mesh客戶端在內(nèi)所有用戶均可竊取傳輸信息；

5) 本文所涉及的用戶特指本地用戶.

WMN客戶端與LTCA間認(rèn)證協(xié)議滿足5點:

1) 用戶或節(jié)點的私鑰由自己生成，節(jié)點主要指負(fù)責(zé)認(rèn)證的服務(wù)器[17].

3) LTCA.由1組Mesh網(wǎng)認(rèn)證服務(wù)器組成(MASs是WMN中負(fù)責(zé)認(rèn)證的Mesh路由器)，負(fù)責(zé)WMN中用戶MU的初始化，將MU主公鑰與身份IDMU由LTCA私鑰SKLTCA綁定簽名生成輔公鑰，對WMN異地用戶進(jìn)行身份認(rèn)證(此部分不做研究)[8].

結(jié)合協(xié)議假設(shè)和滿足條件，當(dāng)本地用戶MU與其他用戶通信時，WMN客戶端與LTCA間雙向認(rèn)證協(xié)議詳細(xì)過程如圖1所示：

LTCA→MU:{RLTCA}

Fig. 1 Two-way authentication between user and LTCA
圖1 用戶與LTCA雙向認(rèn)證

1) LTCA→MU.LTCA在收到用戶MU請求時，生成隨機(jī)數(shù)

R

LTCA

，然后發(fā)送給用戶MU.

WMN客戶端MU與LTCA之間確定雙向認(rèn)證可信性，具體交互過程如圖2所示：

Fig. 2 Two-way authentication description圖2 雙向認(rèn)證描述

2 事件邏輯理論

2.1 事件邏輯

事件邏輯對安全協(xié)議基本原語進(jìn)行形式化規(guī)約，在協(xié)議研究中建立包含地址和事件的模型來證明協(xié)議安全屬性，信息以多種形態(tài)存儲在地址中，以消息形式在不同地址間進(jìn)行傳遞.通過事件邏輯理論驗證加密協(xié)議安全性，定義事件邏輯方法的布爾值(B)、標(biāo)示符(Id)、原子(Atom)，其中原子表示隨機(jī)數(shù)、簽名、密文以及加密密鑰等不可預(yù)測數(shù)據(jù)[9].定義事件、事件類以及事件結(jié)構(gòu)構(gòu)建認(rèn)證理論，對協(xié)議強(qiáng)認(rèn)證性質(zhì)進(jìn)行證明.

2.1.1 基本定義

1)Atom類型

Atom類型表示保密信息，其成員用atoms表示，atoms是不可預(yù)測的.Atom類型成員是基本元素，沒有結(jié)構(gòu)且不能被生成.Atom類型用來評價規(guī)范形式tok(a),tok(b),…,記為tokens，其中a,b,…為其中參數(shù).

置換規(guī)則.事件邏輯中對任意判斷J(a,b,…),其中a,b,…為有限集，則J(a′,b′,…)的真值過程a|→a′,b|→b′,…是一個置換.

2) 獨(dú)立性

事件邏輯理論中定義(state aftere)為事件e發(fā)生后主體出現(xiàn)的狀態(tài)，事件e本質(zhì)是一個空間或時間點.

(x:T‖a)表示T類型元素不包含原子a，當(dāng)x屬于T類型時，x‖a表示x和a獨(dú)立，即T類型的x獨(dú)立于a.

3) 事件結(jié)構(gòu)

分布式計算的形式化模型可定義分布式系統(tǒng)的運(yùn)算以及認(rèn)證[9]，在運(yùn)算中，e,events等消息是在遷移的，其中信息交互初始階段為info(e).事件集是信息在一些存儲位置(如主體在事件發(fā)生時進(jìn)程、線程)中事件出現(xiàn)的空間時間點.事件在單個位置時間點沒有重疊，是整體序.無論如何遷移(消息傳遞、消息共享)，事件各主體間均會產(chǎn)生因果序.

計算系統(tǒng)語義通過事件結(jié)構(gòu)語言描述，事件語言是任何語言的擴(kuò)展.E,loc,<,info即事件序(event-ordering)，其中l(wèi)oc是事件E上的函數(shù)，<是事件E的一個因果關(guān)系，是一個本地有限集.事件包含有限個前驅(qū).e∈E,loc(e)是事件存儲單元，info(e)表示事件發(fā)生時將消息交付給本地loc(e).e1

認(rèn)證協(xié)議交互信息包括隨機(jī)數(shù)、簽名以及名字等元組信息，可以轉(zhuǎn)化為

Data≡defTree(Id+Atom).

事件結(jié)構(gòu)中事件語言建模時需滿足：

① ≤表示局部有限偏序(每個事件e包含有限個前驅(qū))[10]；

②e1

③ 認(rèn)證理論中，loc(e)的位置是事件e發(fā)生的主體，對一些標(biāo)示符X來說loc(e)=X；

④ 協(xié)議安全性證明中e′

事件邏輯為消息自動機(jī)提供健全語義，消息可靠發(fā)送包含named,fifo,link，每一條信息都有關(guān)聯(lián)標(biāo)簽，是頭信息.事件包含類型、價值，收到的信息在linkl包含tagtg，是類型為rcv(l,tg)的事件e.消息類型依靠(link,tag)來判斷，例如sender(e)

事件e發(fā)送消息獨(dú)立于原子a，sends(e)‖a即?e′:E.(isrcv(e′)∧sender(e′)=e)?val(e′)‖a.

2.1.2 加密系統(tǒng)建模

1) 隨機(jī)數(shù)n(nonce)

主體i通過虛服務(wù)si對主體生成隨機(jī)數(shù)能力進(jìn)行模型構(gòu)建，該服務(wù)用來構(gòu)建si到i的連接li以及i到si的連接li，記錄在無重復(fù)包含指針的列表ats內(nèi).主體i需要隨機(jī)數(shù)時在連接li發(fā)送一個包含隨機(jī)數(shù)的請求消息，通過si收到的請求消息在E(Noncei)中生成事件n響應(yīng)，即Noncei(n)，其中主體atoms在ats中是獨(dú)立的.

域E(Noncei)中，若隨機(jī)數(shù)n∈E(Noncei)和事件e滿足n≤e?(val(e)‖Noncei(n))，則從events到atoms中偏序函數(shù)Noncei屬于隨機(jī)數(shù)交互，即除非事件在隨機(jī)數(shù)生成后與之產(chǎn)生因果，否則其值不包含該隨機(jī)數(shù).

2) 事件類(event class)

事件邏輯理論中，通過事件對協(xié)議進(jìn)行分類描述，使用事件序語言、事件類對協(xié)議進(jìn)行構(gòu)建.T類型事件類從事件到T類型值是簡單的偏函數(shù)，如果X是一個事件類，則規(guī)定E(X)是X范圍內(nèi)的事件集，E(X)中事件屬于類X.對于事件e∈E(X)，X(e)是類X分配給e的T類型值.

一個事件類可以是任何不同事件類中的成員，如果Y是類型T′的事件類，f是T→T′的函數(shù)，那么X(v)?Y(f(v))等價于?e.e∈X(v)?e∈Y(f(v)).

若隨機(jī)數(shù)n∈E(Noncei),事件e∈E(X)沒有關(guān)聯(lián)，則(loc(e)≠si?X(e))‖Noncei(n).

類中事件轉(zhuǎn)換成原子X類中事件e信息包含原子a，則：

X(e) hasa≡def(e∈?(X)∧(X(e):T‖a)).

認(rèn)證協(xié)議包含發(fā)送、接收、隨機(jī)數(shù)、簽名、認(rèn)證、加密、解密7類事件[10]，事件類對應(yīng)相關(guān)信息，信息類型取決于事件類，事件類中相關(guān)信息包含原子，基于7類事件類的形式化身份認(rèn)證理論的類型列表具體定義如圖3所示：

Fig. 3 Event classes of the authentication theory
圖3 認(rèn)證理論的事件類

在圖3中，類Sign,Verify中事件類型相同，均為三元組Data×Id×Atom，其中類Sign,Verify為signed(e),signer(e),signature(e).事件類型在類Encrypt,Decrypt中為三元組Data×Key×Atom，即encrypted(e),key(e),ciphertext(e).

對于e∈E(Sign)，事件信息Sign(e)=x,A,s表示事件e是主體A對密文x進(jìn)行簽名生成s.如果A是誠實主體，則loc(e)=A，誠實主體不會釋放私鑰.對于事件e′∈E(Verify)，該事件信息與簽名信息相對應(yīng)即Verify(e′)=x,A,s表示事件e′是主體B=loc(e′)成功驗證主體A簽名生成的密文x.

事件e∈E(Encrypt),Encrypt(e)=x,k,c表示事件e是主體A通過密鑰k對明文x加密生成密文c，主體A擁有密鑰k和消息x.事件e′∈E(Decrypt)中,Decrypt(e′)=x,k′,c表示事件e′是主體B通過密鑰k′解密密文c生成明文x的過程.密文c生成時，對應(yīng)解密公理AxiomD中存在一個匹配密鑰.

2.2 事件邏輯公理、推論及性質(zhì)

2.2.1 事件邏輯公理

對稱密鑰和私鑰作為標(biāo)示符是不可測的，兩者并不相同，Key類型為Key≡defId+Atom+Atom.

事件邏輯中PrivKey函數(shù)的主體包含原子，MatchingKeys函數(shù)構(gòu)建密鑰間的關(guān)系，如圖4所示：

事件邏輯公理[9]包含密鑰公理、誠實公理、因果公理、不相交公理、流關(guān)系，具體為

1) 密鑰公理(key axiom,AxiomK)

密鑰公理(AxiomK)的匹配密鑰間是對稱的，密鑰信息是主體特有，不同主體不會擁有相同私鑰.主體A私鑰僅能夠與自身公鑰匹配，具體表示為

?A,B:Id.?k,k′；Key.?a:Atom
MatchingKeys(k;k′)?MatchingKeys(k′,k)∧
MatchingKeys(Symm(a);k)?k=Symm(a)∧
MatchingKeys(PrivKey(A);k)?k=A∧
MatchingKeys(A;k)?k=PrivKey(A)∧
PrivKey(A)=PrivKey(B)?A=B.

2) 誠實公理(honest axiom,AxiomS)

事件邏輯理論包含函數(shù)Honest：Id→B對誠實主體進(jìn)行斷言，誠實主體私鑰不會釋放，主體簽名、加密以及解密事件均發(fā)生在誠實主體上，通過AxiomS對誠實主體性質(zhì)刻化為

3) 因果公理(causal axioms)

因果公理是對事件類中接收事件Rcv、驗證事件Verify、解密事件Decrypt所對應(yīng)事件公理(接收公理AxiomR、驗證公理AxiomV、解密公理AxiomD)關(guān)系的整合.AxiomR,AxiomV相似，任何接收或驗證事件發(fā)生前存在一個與之相應(yīng)且信息內(nèi)容相同的發(fā)送或簽名事件[10]，具體為

AxiomR:?e:E(Rcv).?e′:E(Send).(e′Rcv(e)=Send(e′).
AxiomV:?e:E(Verify).?e′:E(Sign).(e′Verify(e)=Sign(e′).

AxiomD與AxiomR和AxiomV相似，解密事件主體在事件發(fā)生前收到一個與之密鑰匹配、其他信息相同的加密事件,具體表示為

?e:E(Decrypt).?e′:E(Encrypt).
e′plaintext(e)=plaintext(e′)∧
ciphertext(e)=ciphertext(e′)∧
MatchingKeys(key(e);key(e′)).

4) 不相交公理(disjointness axioms)

2個原子間不相交假設(shè)主要考慮2方面.一方面任意這7個事件類不在其他類中，即：

ActionDisjoint:?f:E→Z.?e:E.
(e∈E(New)?f(e)=1)∧
(e∈E(Send)?f(e)=2)∧…∧
(e∈E(Decrypt)?f(e)=7).

另一方面主體生成的隨機(jī)數(shù)n與主體所持有的私鑰、簽名或密文不相同，且三者間不相交[18].簽名可以是明文通過散列加密生成，而密文是明文加密生成，Data類型成員在散列加密后不等同于Data類型成員，那么簽名不等價于密文，具體表示為

?n:E(New).?s:E(Sign).?e:E(Encrypt).?A:
Id.New(n)≠signature(e)∧New(n)≠
ciphertext(e)∧New(n)≠Private(A)∧
ciphertext(e)≠Private(A)∧
signature(s)≠Private(A)∧
signature(s)≠ciphertext(e).

5) 流關(guān)系(flow relation)

流關(guān)系是隨機(jī)數(shù)因果序事件間的關(guān)聯(lián).Act類型包含7個事件類，記作actions.(ehasa)為真當(dāng)且僅當(dāng)action類型的e中包含a，具體表示為

ehasa≡def(e∈E(New)∧New(e) hasa)∨
(e∈E(Send)∧Send(e) hasa)∨
(e∈E(Rcv)∧Rcv(e) hasa)∨…

1)a從動作e1到動作e2發(fā)生在同一主體上；

2) 介于發(fā)送事件和接收事件間以明文發(fā)送a；

3)a在加密事件明文中，密文流向一個與之匹配的解密事件[18]，具體流關(guān)系遞歸為

6) 隨機(jī)數(shù)公理(nonce axiom,AxiomF)

隨機(jī)數(shù)公理記為AxiomF，包含3部分AxiomF1,AxiomF2,AxiomF3，其中AxiomF1關(guān)于流性質(zhì)，應(yīng)用在事件關(guān)聯(lián)的隨機(jī)數(shù)中，具體為

AxiomF2,AxiomF3介紹簽名、密文以及包含2類事件的相關(guān)關(guān)系，沒有規(guī)定簽名或密文與特殊事件有關(guān).如果一個動作包含簽名或密文，則可以推斷出具有相同信息的簽名或加密動作[10]，具體為

2.2.2 事件邏輯引理及性質(zhì)

基本序列是協(xié)議動作的參數(shù)列表，參數(shù)是主體標(biāo)識符，由2個及以上組成[9].遵守協(xié)議的主體參與到多個線程，線程是協(xié)議基本序列實例且遵守協(xié)議[10].

引理 3.隨機(jī)數(shù)引理.

協(xié)議Protocol(bss)是合法的，主體A是誠實主體且遵守Pr，線程thr是基本序列bss的一個實例，n=thr[j],n∈E(New),e=thr[i]和j

在協(xié)議強(qiáng)認(rèn)證證明過程中，規(guī)定被證明協(xié)議合法，線程thr1相鄰事件e0,e1不存在發(fā)送動作(或任何的動作發(fā)生)，由隨機(jī)數(shù)引理可得，事件e1發(fā)生前隨機(jī)數(shù)不會被釋放.

安全協(xié)議形式化分析過程中，誠實主體在執(zhí)行相關(guān)動作時需要滿足5個性質(zhì)[19]：

性質(zhì)1.多組合信息交互.

誠實主體A本身持有可信第三方(trusted third party,TTP)授權(quán)且遵守協(xié)議Protocol(bss)，在認(rèn)證過程中需要通過TTP授權(quán)進(jìn)行驗證，這屬于誠實主體自身行為,即:

?A:Id.?e,e′:E(e)∈TTP∧(e?e′:A|≡E[e].

在驗證協(xié)議交互過程安全性問題中可以省略該證明，從而降低證明過程中的復(fù)雜度.

性質(zhì)2.不疊加.

協(xié)議分析過程中，對于在匹配會話中已經(jīng)驗證過的動作，在新一輪的驗證過程中可以直接引用驗證結(jié)果來減少冗余.

?A:Id.?e1,e2:e1

性質(zhì)3.事件匹配.

在7種事件類中，在遵守協(xié)議Protocol(bss)的前提下發(fā)起者主體A、響應(yīng)者主體B(事件響應(yīng)者可以不是相同的主體)必須參與的事件類是雙方的或者多方的，從而保障事件發(fā)生的有效性.

?A,B:(A≠B).?e1,e2:((e1∈A,e2∈B)∧
(e1Verify(e2)∨Decrypt(e1)=Encrypt(e2).

性質(zhì)4.去重復(fù)性.

在驗證事件匹配的過程中，如果出現(xiàn)多個事件需要同時進(jìn)行驗證，則依據(jù)從上到下的原則進(jìn)行驗證來減少驗證過程中的重復(fù)操作.

性質(zhì)5.去未來性.

在考慮匹配動作的過程中，以當(dāng)前已發(fā)生事件為基準(zhǔn)，對于之后沒有發(fā)生的動作不予考慮來減少驗證過程中的不必要進(jìn)程.

2.3 形式化方法描述協(xié)議

1) 線程

線程是動作在單個位置的有序列表，滿足：

Thread≡def{thr:ActList|?i:thr[i]

thr1?thr2表示線程thr1是線程thr2前面發(fā)生的一個相鄰線程，定義thr1?thr2為

thr1?thr2∨thr2?thr1.

線程消息是線程中發(fā)送和接收動作的集合，即：

isMsg(e)≡defe∈E(Send)∨e∈E(Rcv)，
messages(thr)≡deffilter(isMsg,thr).

對于消息s和r，s是發(fā)送消息，r是接收消息，s和r間傳遞消息相同，則2條信息間是一個弱匹配關(guān)系，即s～r；如果s與r之間有直接因果關(guān)系，s發(fā)生在r之前，則s和r之間是一個強(qiáng)匹配關(guān)系，即為s|→r，具體為

s～r≡defs∈E(Send)∧r∈E(Rcv)∧
Send(s)=Rcv(r)，
s|→r≡defs～r∧s

2) 基本序列(basic sequence)

基本序列是協(xié)議動作的基本參數(shù)列表,在協(xié)議主體A,B參數(shù)是標(biāo)示符，主體A遵守協(xié)議，參與協(xié)議多個線程，線程是協(xié)議中的實例，與主體B在不同位置進(jìn)行交互[19].事件邏輯中所研究的協(xié)議允許多個主體參與.

基本序列是2個位置與一個線程的聯(lián)系，當(dāng)線程是基本序列給定的位置參數(shù)，則這個關(guān)系為真，基本序列類型成員為

Basic≡defId→Id→Thread→P.

注：其中P代表命題(proposition),在命題邏輯結(jié)構(gòu)中跟布爾運(yùn)算是不同的.

基本序列實例可以生成隨機(jī)數(shù)、簽名等，參數(shù)原子是在序列在關(guān)系中量化存在.線程thr是主體A中已知基本序列關(guān)系bss，記作thr=oneof(bss,A).關(guān)系inoneof(e,thr,bss,A)作為協(xié)議形式化定義，記作：e∈thr∧thr=oneof(bss,A).

3) 匹配會話及協(xié)議動作

① 匹配會話

線程thr1和thr2構(gòu)成長度為n的匹配會話，如果它們至少包含n個消息，當(dāng)每個線程中前n個消息成對，每對m1,m2滿足m1|→m2∨m2|→m1，則構(gòu)成強(qiáng)匹配會話，即為如果每對m1,m2只滿足m1～m2∨m2～m1，得到一個弱匹配會話，記作

② 協(xié)議動作

使用基本協(xié)議動作描述協(xié)議ProtocolAction類來定義協(xié)議動作.所有成員類包含標(biāo)簽tag和值value，ProtocolAction類成員包含7種動作，定義如下：

{New(a)|a∈Atom}；
{Send(x)|x∈Data}；
{Rcv(x)|x∈Data}；
{Sign(t)|t∈Data×Id×Atom}；
{Verify(t)|t∈Data×Id×Atom}；
{Encrypt(t)|t∈Data×Key×Atom}；
{Decrypt(t)|t∈Data×Key×Atom}.

協(xié)議動作pa(protocol action)對應(yīng)事件e，則：

e∈E(New)∧pa=new(New(e))∨
e∈E(Send)∧pa=send(Send(e))∨…

4) 事件邏輯方法描述協(xié)議

① 定義協(xié)議

事件邏輯理論使用Basic類型的基本序列關(guān)系表bss定義一個協(xié)議[10].協(xié)議是在存儲位置的斷言，類型為Id→P.

協(xié)議Protocol(bss)定義為

λA.?e:Act.loc(e)=A?
(?thr.inOneof(e,thr,bss,A))∧
?thr1,thr2.(inOneof(e,thr1,bss,A)∧
inOneof(e,thr1,bss,A))?thr1?thr2.

主體A動作是基本序列的實例成員，如果動作是一個或多個實例成員，則實例是兼容的.

② 認(rèn)證

主體A,B為誠實主體且遵守協(xié)議，主體A發(fā)起一個會話序列，主體B的一個應(yīng)答序列與之構(gòu)成合法匹配會話.類似地，如果主體B執(zhí)行全應(yīng)答序列的一個實例，那么有一個和主體A的匹配會話，即接收消息和相匹配的發(fā)送消息內(nèi)容一致[10].消息雙方完成身份認(rèn)證保證不會有攻擊者借助之前攔截消息進(jìn)行偽裝會話攻擊，匹配會話過程滿足強(qiáng)匹配，協(xié)議Pr中基本序列bs認(rèn)證n個消息，認(rèn)證過程滿足：

prauth(bs,n)≡def?A,B.?thr1.
(Honest(A)∧Honest(B)∧Pr(A)∧Pr(B)∧
A≠B∧loc(thr1)=A∧bs(A,B,thr1))?
?

2.4 安全協(xié)議證明過程

事件邏輯理論描述協(xié)議強(qiáng)認(rèn)證性質(zhì)，具體如圖5所示：

Fig. 5 The flowchart of event logic method which proves the protocol authentication 圖5 事件邏輯方法證明協(xié)議認(rèn)證性流程圖

1) 定義基本序列

利用事件邏輯理論方法對安全協(xié)議進(jìn)行形式化描述，定義發(fā)起者、響應(yīng)者序列的具體動作[9]，規(guī)范協(xié)議基本序列，確認(rèn)滿足協(xié)議安全性需要證明的強(qiáng)認(rèn)證性質(zhì).

2) 對強(qiáng)認(rèn)證性質(zhì)的單向進(jìn)行證明

規(guī)定主體不同是誠實的且遵守協(xié)議，假設(shè)某一線程為協(xié)議基本序列的實例，定義線程上的動作，確定協(xié)議匹配事件.分析匹配事件，確認(rèn)是否存在匹配會話以及匹配會話內(nèi)部是否含有需要進(jìn)一步證明的匹配事件.

3) 確定匹配事件，進(jìn)行排除分析

查詢相關(guān)匹配事件是否符合匹配會話，如果符合則進(jìn)行由內(nèi)而外對相關(guān)匹配會話的證明；如果不符合則進(jìn)行下一輪匹配事件的篩選證明，確認(rèn)整個匹配事件是否滿足弱匹配.

4) 確認(rèn)強(qiáng)認(rèn)證性質(zhì)

確認(rèn)匹配會話屬于弱匹配，分析協(xié)議交互過程的匹配會話長度，根據(jù)相關(guān)公理確認(rèn)強(qiáng)匹配會話.

5) 單向證明成立后，進(jìn)行雙向強(qiáng)認(rèn)證性質(zhì)證明

如果證明成立，則說明協(xié)議是安全的；在整個證明過程中，如果一邊的匹配事件不能滿足弱匹配，說明協(xié)議同樣不滿足強(qiáng)認(rèn)證性質(zhì)，在認(rèn)證階段不能達(dá)成雙向身份認(rèn)證，協(xié)議易被攻擊者偽裝身份進(jìn)行攻擊，存在消息重放的可能，協(xié)議主體不安全[10].

以流程圖的方法簡化事件邏輯理論證明協(xié)議安全性.

3 事件邏輯理論證明WMN客戶端與LTCA認(rèn)證協(xié)議

通過事件邏輯理論對WMN客戶端與LTCA雙向認(rèn)證協(xié)議進(jìn)行基本序列排序，定義I1,I2,I3為發(fā)起方在協(xié)議交互過程中產(chǎn)生的基本序，R1，R2，R3為協(xié)議響應(yīng)者在協(xié)議交互過程中產(chǎn)生的基本序.LTCA作為協(xié)議交互過程中動作發(fā)起方(initiator)，用戶MU作為協(xié)議交互過程中動作響應(yīng)方(res-ponder),協(xié)議具體描述如圖6所示.

Fig. 6 Basic sequence description of two-way authentication圖6 雙向認(rèn)證基本序列描述

基于事件邏輯理論定義協(xié)議滿足安全性需要滿足的身份認(rèn)證性質(zhì)，驗證WMN客戶端與LTCA協(xié)議認(rèn)證性[18]，協(xié)議基本序列如圖7所示.

根據(jù)協(xié)議中定義的基本序列，定義WMN客戶端與LTCA間雙向認(rèn)證協(xié)議Protocol([I1,I2,I3,R1,R2,R3]).

協(xié)議需要驗證的強(qiáng)認(rèn)證性質(zhì)為

Nseauth(I3,2)∧Nseauth(R3,3).

1) 對Nseauth(I3,2)進(jìn)行證明

證明. 假設(shè)誠實主體MU≠LTCA且遵守WMN客戶端與LTCA雙向認(rèn)證協(xié)議，線程thr1是

Fig. 7 Basic sequence of two-way authentication protocol
圖7 雙向認(rèn)證協(xié)議的基本序列

基本序

I

3

的實例，

e

0

<

loc

e

1

<

loc

…<

loc

e

6

為線程

thr

1

上的動作，那么事件

e

0

,

e

1

,…,

e

6

發(fā)生的主體為LTCA.對原子

則有：

(1)

由AxiomD以及AxiomS可知，存在事件e′,e″,e′″,e″″使得主體MU同時滿足4個條件：

① 事件e′中e′

② 事件e″中e″

③ 事件e′″中e′″

④ 事件e″″中e″″

對于事件發(fā)生的主體滿足：

Encrypt(e′)=RMU,PKLTCA,S3.
Encrypt(e″)=h1,PKLTCA,S2.
Encrypt(e′″)=,
.
Encrypt(e″″)=RLTCA,SKMU,S1.

根據(jù)性質(zhì)4，以事件e′為研究對象，因為主體MU遵守WMN客戶端和LTCA雙向認(rèn)證協(xié)議，事件e′必然為WMN客戶端與LTCA雙向認(rèn)證協(xié)議的基本序列之中的一個實例成員[10].在協(xié)議交互過程中包含加密Encrypt( )動作的是I3,R1,R2,R3，根據(jù)性質(zhì)5以及圖6可知，MU基本序R2,R3發(fā)生在基本序I3后，故基本序R2,R3可以排除.

(2)

在主體中，SKLTCA和PKLTCA分別為LTCA的私鑰和主公鑰，符合AxiomD定義構(gòu)成匹配，則主體滿足：

1RMU=RMU,PKA=PKLTCA,1S3=S3,A=L,
1h1=h1,1S2=S2,1S1=S1,RA=RLTCA.

可得到：

(3)

可得到：

(4)

由線程thr1的初始式(1)可知，基本序I3內(nèi)可以構(gòu)成完整(Send,Rcv)的是事件e1和e2.根據(jù)事件邏輯的認(rèn)證規(guī)則，結(jié)合式(1)以及式(4)可得，Send(e1)=L,RLTCA和Rcv(e2)=得到一個長度為2的(弱)匹配.

Nseauth(I3,2).

證畢.

2) 對Nseauth(R3,3)進(jìn)行證明

(5)

由AxiomD以及AxiomS可知，主體LTCA滿足存在事件e″?,e″?′,e″?″使得加密解密事件匹配成立，即：

則事件發(fā)生主體滿足：

根據(jù)性質(zhì)4，以事件e″?為研究對象，因為主體LTCA遵守WMN客戶端和LTCA雙向認(rèn)證協(xié)議，事件e″?必然為認(rèn)證協(xié)議的基本序列的實例成員.在協(xié)議交互過程中包含加密Encrypt( )動作的是I3,R1,R2,R3，根據(jù)性質(zhì)3以及圖6可知，對于基本序R1,R2可以進(jìn)行排除.

(6)

可得到：

(7)

可以得到：

(8)

線程thr2所涉及式(5)可知，在基本序R3中可以構(gòu)成完整的(Send,Rcv)是事件e0,e5,e6.根據(jù)協(xié)議形式化認(rèn)證規(guī)則，結(jié)合式(1)(4)(5)(8)可得，Rcv(e0)=L,RLTCACertLTCA,S6,S4,T2此時就可以得到一個長度為3的(弱)匹配.

Nseauth(R3,3).

證畢.

綜合證明1)和2)可知，強(qiáng)認(rèn)證性質(zhì)Nseauth(I3,2)∧Nseauth(R3,3)得到完整證明，即WMN客戶端和LTCA間雙向認(rèn)證協(xié)議同時滿足2個強(qiáng)認(rèn)證性質(zhì)，此過程不存在消息重放的可能性，協(xié)議安全性得證，即WMN客戶端和LTCA間雙向認(rèn)證協(xié)議是安全的且攻擊者無法通過偽裝合法用戶進(jìn)行重放攻擊.此時客戶端獲得LTCA的認(rèn)證證書，可以與其他的客戶端用戶進(jìn)行有效通信.

4 形式化方法對比分析

形式化方法用數(shù)學(xué)模型描述推理基于計算機(jī)的系統(tǒng)概念或方法，即規(guī)范語言+形式推理.規(guī)范語言包括：抽象模型規(guī)范法、代數(shù)規(guī)范法、狀態(tài)遷移規(guī)范法和公理規(guī)范法.形式化方法有形式化描述、形式化設(shè)計和形式化驗證，幾十年來國內(nèi)外專家學(xué)者在這3方面研究工作做出巨大貢獻(xiàn).事件邏輯理論是定理證明方法的一種，定理證明優(yōu)于其他形式化方法的地方在事件邏輯理論中均有體現(xiàn)，但事件邏輯理論相較于其他形式化方法也存在不足.本節(jié)綜合其他形式化方法對事件邏輯理論進(jìn)行概述.

4.1 事件邏輯與模態(tài)邏輯比較

模態(tài)邏輯是目前應(yīng)用最廣泛的形式化方法，包括BAN邏輯、類BAN邏輯，其中類BAN邏輯包含十多種邏輯方法.各類邏輯方法的語法定義各具特色，協(xié)議安全屬性驗證過程采用邏輯推理方式進(jìn)行證明，這與基于事件邏輯理論的定理證明方法一致.

以BAN邏輯為例，相較事件邏輯理論方法，BAN邏輯要進(jìn)行大量理想化處理，這其中包含協(xié)議前提、協(xié)議本身、協(xié)議目標(biāo)等，這些動作通過形式化描述實現(xiàn).

1) BAN邏輯形式化描述協(xié)議初始化假設(shè)、安全協(xié)議預(yù)期目標(biāo)，這些步驟與事件邏輯理論方法類似，但BAN邏輯對所處執(zhí)行環(huán)境、參與協(xié)議執(zhí)行主體和協(xié)議使用密鑰等作出的初始假設(shè)過分依賴.事件邏輯理論對協(xié)議初始化方面沒有過分處理，但對協(xié)議客觀環(huán)境進(jìn)行假設(shè)要求，在協(xié)議交互過程進(jìn)行合理抽象化處理.

2) BAN邏輯對協(xié)議理想化處理過分依賴分析者直覺，理想化過程會產(chǎn)生問題，使得理想化后協(xié)議與原來協(xié)議有一定差距.例如忽略或增加協(xié)議前提或內(nèi)容，對協(xié)議目標(biāo)描述不夠準(zhǔn)確，易造成分析結(jié)果與原協(xié)議設(shè)計有一定出入[20].事件邏輯理論定義嚴(yán)謹(jǐn)?shù)臄?shù)學(xué)規(guī)則，規(guī)范一系列公理推論規(guī)則約束，從而保證強(qiáng)認(rèn)證性質(zhì)證明過程的嚴(yán)謹(jǐn)性.

3) BAN邏輯利用規(guī)則進(jìn)行按步推理，運(yùn)用嚴(yán)謹(jǐn)推理邏輯證明協(xié)議.但是BAN邏輯語義刻畫不夠清晰，證明協(xié)議安全性并不能讓人很好信服，同樣BAN邏輯不能很好保證協(xié)議證明的實用性.事件邏輯理論定義的定理規(guī)則，結(jié)構(gòu)清晰、無歧義，保證協(xié)議在證明過程中的真實可靠性，使得協(xié)議安全屬性更具有可信性.

4) BAN邏輯規(guī)則定義相較事件邏輯理論更加成熟，研究方面更廣泛.在定義規(guī)則上，BAN邏輯規(guī)則可讀性更強(qiáng)，使用者不需要過高的數(shù)學(xué)基礎(chǔ)以及邏輯推理能力.在使用BAN邏輯證明過程中，使用者可以通過調(diào)用定義規(guī)則對目標(biāo)進(jìn)行證明.

5) 模態(tài)邏輯與事件邏輯理論一樣，需要大量的手工作業(yè)，在形式化自動化驗證方面有待提高.

4.2 事件邏輯理論與PCL比較

協(xié)議組合邏輯(protocol composition logic, PCL)是一種證明加密協(xié)議安全系統(tǒng)的邏輯方法.PCL與事件邏輯理論方法一樣，協(xié)議形式化建模生成隨機(jī)數(shù)、接收發(fā)送消息、對消息執(zhí)行加密操作以及簽名驗證.

1) 協(xié)議安全屬性驗證中，PCL方法只能對部分協(xié)議性質(zhì)進(jìn)行刻畫，對數(shù)據(jù)簽名協(xié)議的認(rèn)證性質(zhì)不能進(jìn)行刻畫，而基于事件邏輯理論的定理證明方法可以對其他安全屬性進(jìn)行刻畫認(rèn)證.

2) PCL方法在協(xié)議交互動作建模中不夠嚴(yán)謹(jǐn)，對描述線程的前序動作序列機(jī)制缺乏定義.事件邏輯理論方法對協(xié)議形式化建模線程機(jī)制進(jìn)行明確定義，通過原子獨(dú)立性規(guī)范事件發(fā)生先后線程狀態(tài).

3) PCL方法對協(xié)議信息數(shù)據(jù)類型缺乏必要約束、限制，事件邏輯理論定義特有Atom類型對沒有結(jié)構(gòu)且不能被生成的基本元素進(jìn)行規(guī)范化定義，保證協(xié)議信息數(shù)據(jù)類型的規(guī)范充分.

4) PCL方法描述Diffie-Hellman代數(shù)行為及散列函數(shù)的能力不足，以散列函數(shù)加密為例，事件邏輯理論在處理加密動作時選擇對其進(jìn)行刻畫.以散列函數(shù)加密為例，在消息解密驗證過程中，事件邏輯理論方法通過有效信息生成新的散列加密，然后與刻畫的加密動作進(jìn)行比較證明.

5) PCL在應(yīng)用中經(jīng)歷時間長久，特別是在協(xié)議動作分布自動化方面做了大量工作，此方面是事件邏輯理論方法亟待改進(jìn)的.

4.3 事件邏輯通用性

事件邏輯理論對分布式系統(tǒng)協(xié)議和算法進(jìn)行描述，通過捕捉分布式系統(tǒng)模型實現(xiàn).在事件邏輯理論基本定義中，對原子類型、獨(dú)立性、事件結(jié)構(gòu)進(jìn)行初步建模，保證加密系統(tǒng)建模過程中隨機(jī)數(shù)、事件類建模的完備性.事件邏輯理論通用性具體表現(xiàn)在3個方面：

1) 復(fù)雜協(xié)議對象簡化處理

協(xié)議對象的簡化處理要求對協(xié)議抽象過程、協(xié)議通用屬性進(jìn)行標(biāo)識，保證協(xié)議對象的平凡性；對特有屬性進(jìn)行特別標(biāo)識，保證協(xié)議對象獨(dú)特性.例如，在WMN客戶端與LTCA交互認(rèn)證協(xié)議中，客戶端與LTCA具有共有屬性公私鑰(PK,SK),但2個主體有各自獨(dú)特性，客戶端擁有特有輔公鑰LTCA通過合法程序生成客戶端用戶輔公鑰的權(quán)限，在認(rèn)證過程中生成唯一的證書CertL，需要在協(xié)議形式化描述中對這些性質(zhì)進(jìn)行特別刻畫.

2) 協(xié)議交互環(huán)境合理化假設(shè)

有線網(wǎng)絡(luò)與無線網(wǎng)絡(luò)環(huán)境對于協(xié)議應(yīng)用要求有很大不同，相較而言，無線網(wǎng)絡(luò)環(huán)境下安全協(xié)議設(shè)計有挑戰(zhàn)性.安全協(xié)議不僅要保證用戶能夠承受有線網(wǎng)絡(luò)信息傳遞過程遇到的風(fēng)險，還要面臨無線網(wǎng)絡(luò)環(huán)境獨(dú)有的危險，對協(xié)議安全性認(rèn)證也是挑戰(zhàn).

① 不同協(xié)議適用條件有所不同，協(xié)議形式化描述前要對協(xié)議執(zhí)行條件進(jìn)行了解，對協(xié)議交互條件進(jìn)行合理化分析.

例如WMN客戶端協(xié)議對比有線網(wǎng)絡(luò)安全協(xié)議沒有可靠的認(rèn)證中心，對LTCALCA形式化描述要求具體化，輕量級CA與客戶端認(rèn)證中加入輔公鑰以及證書機(jī)制，加入門限機(jī)制容侵的輕量級CA則在LTCA基礎(chǔ)上加入時間戳T保證LTCA在加密解密信息迭代的時間有效性.

② 對不同協(xié)議提出合理化假設(shè)條件，在合理假設(shè)條件中要求研究者了解協(xié)議運(yùn)行的基本環(huán)境和獨(dú)特環(huán)境.在提出假設(shè)的過程中，假設(shè)條件不宜過多，反之體現(xiàn)協(xié)議運(yùn)行條件的苛刻，對協(xié)議獨(dú)特的運(yùn)行環(huán)境進(jìn)行合理化提取.

例如WMN客戶端間認(rèn)證協(xié)議要求移動主體A與移動主體B在有安全保障條件下進(jìn)行通信，在A,B節(jié)點間進(jìn)行雙向認(rèn)證并產(chǎn)生安全的會話密鑰.安全保障不是說協(xié)議交互環(huán)境絕對安全，協(xié)議交互過程有受到攻擊者攻擊的可能，安全保障是指在協(xié)議交互過程中不會受到惡劣自然環(huán)境或大型設(shè)備故障等非人為蓄意情況的影響.客戶端間交互時，雙方都收到認(rèn)證中心的認(rèn)證，擁有認(rèn)證中心頒發(fā)的證書.

3) 協(xié)議交互過程刪繁就簡

協(xié)議信息在無線網(wǎng)絡(luò)通道傳遞的過程中包含各種基本信息，例如數(shù)據(jù)在物理層、網(wǎng)絡(luò)層等的傳輸交互，這些信息在事件邏輯理論形式化描述過程中均不做具象處理，以信息Msg來定義.但是協(xié)議動作對消息處理要進(jìn)行明確標(biāo)注，保證事件邏輯理論方法在協(xié)議建模時信息傳遞過程的有效性.

例如Needham-Schroeder協(xié)議交互雙方在進(jìn)行信息傳遞過程中，主體A通過主體B的公鑰PKB對自己產(chǎn)生的隨機(jī)數(shù)Na以及時間戳T1進(jìn)行加密，將消息傳遞給用戶主體B.在形式化描述過程中，對信息的各層封裝交互并不做研究描述，直接總括這一過程，即A→B:SignPKB{A,Na,T1}.

5 結(jié) 論

5.1 總 結(jié)

信息安全涉及信息資源交互中的機(jī)密性、完整性以及可用性，安全協(xié)議形式化方法在長期積累中形成比較完善的理論體系以及模型，定理證明是形式化方法的一種，基于嚴(yán)格數(shù)學(xué)理論知識和邏輯推導(dǎo)，從而確定協(xié)議在合理假設(shè)條件下是否滿足要驗證的安全屬性[21].本文基于事件邏輯理論，使用定理證明的方法對WMN客戶端協(xié)議認(rèn)證性進(jìn)行分析，所取得的成果具體有4個方面：

1) 對事件邏輯理論進(jìn)行擴(kuò)展，提出置換規(guī)則保證協(xié)議交互用戶在置換中性質(zhì)的等價轉(zhuǎn)換.將基于事件邏輯理論證明協(xié)議安全性的過程通過流程圖表述，詳細(xì)介紹事件邏輯理論證明過程.

2) 通過事件邏輯描述客戶端與LTCA間交互協(xié)議的基本序列，對協(xié)議交互動作形式化描述.證明協(xié)議強(qiáng)認(rèn)證性質(zhì)，得出WMN客戶端與LTCA間認(rèn)證協(xié)議在合理假設(shè)下是安全的.表明事件邏輯理論可以對安全協(xié)議不同身份主體間的認(rèn)證性進(jìn)行證明.

3) 結(jié)合文獻(xiàn)[10,19]可知，事件邏輯不僅可以對有線網(wǎng)絡(luò)安全協(xié)議的安全屬性進(jìn)行證明，對無線網(wǎng)絡(luò)安全協(xié)議的安全屬性也可以給予合理論證，進(jìn)而保證安全協(xié)議在用戶交互過程中的可靠性.

4) 分析事件邏輯理論方法與其他邏輯證明方法的優(yōu)缺點，說明事件邏輯理論具有通用性.

5.2 展望

國內(nèi)外專家學(xué)者對無線網(wǎng)絡(luò)協(xié)議研究領(lǐng)域做了大量的研究，取得了豐碩成果.絕對安全協(xié)議是不存在的，不論多么完美的協(xié)議總會存在未被發(fā)現(xiàn)的漏洞，還需要進(jìn)一步的研究證明甚至是改進(jìn)論證.本文運(yùn)用的事件邏輯理論方法也存在不足和需要進(jìn)一步改善的方面，根據(jù)目前研究成果，今后進(jìn)一步研究方向可以從4點進(jìn)行考慮：

1) 事件邏輯理論證明方法更多依靠手工證明，此次對該方法各個步驟進(jìn)行定義，下一步研究可以著手實現(xiàn)分布自動化.將分步實施的概念加入正在構(gòu)建的安全協(xié)議驗證系統(tǒng)中，從而實現(xiàn)網(wǎng)絡(luò)安全協(xié)議認(rèn)證性的自動化證明.

2) 在對協(xié)議安全屬性進(jìn)行分析研究時，目前更多的是通過事件邏輯理論方法對安全協(xié)議認(rèn)證性證明，下一步可以考慮通過基于事件邏輯理論的定理證明方法對安全協(xié)議保密性、完整性等安全屬性進(jìn)行形式化證明.

3) 事件邏輯理論在安全協(xié)議證明過程中可能存在不足，可以對事件邏輯理論相關(guān)推論性質(zhì)進(jìn)行分析擴(kuò)展及證明.

4) 單一的形式化方法證明存在缺陷，可以考慮在安全協(xié)議的研究證明中結(jié)合模型檢測或模態(tài)邏輯等方法對協(xié)議安全屬性進(jìn)行分析，從而保障安全協(xié)議強(qiáng)認(rèn)證性質(zhì)刻畫的完備性.