基于事件邏輯的WMN客戶端與LTCA認證協議安全性分析

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

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

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

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

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

1 WMN客戶端與LTCA認證協議

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

本文在研究通信雙方交互過程中進行5點假設：

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

2) 以多跳形式經過中間轉發的用戶節點忽略不計；

3) 不存在任何值得注意的網絡延遲現象；

4) 無線網絡環境包括非法Mesh客戶端在內所有用戶均可竊取傳輸信息；

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

WMN客戶端與LTCA間認證協議滿足5點:

1) 用戶或節點的私鑰由自己生成，節點主要指負責認證的服務器[17].

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

結合協議假設和滿足條件，當本地用戶MU與其他用戶通信時，WMN客戶端與LTCA間雙向認證協議詳細過程如圖1所示：

LTCA→MU:{RLTCA}

Fig. 1 Two-way authentication between user and LTCA
圖1 用戶與LTCA雙向認證

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

R

LTCA

，然后發送給用戶MU.

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

Fig. 2 Two-way authentication description圖2 雙向認證描述

2 事件邏輯理論

2.1 事件邏輯

事件邏輯對安全協議基本原語進行形式化規約，在協議研究中建立包含地址和事件的模型來證明協議安全屬性，信息以多種形態存儲在地址中，以消息形式在不同地址間進行傳遞.通過事件邏輯理論驗證加密協議安全性，定義事件邏輯方法的布爾值(B)、標示符(Id)、原子(Atom)，其中原子表示隨機數、簽名、密文以及加密密鑰等不可預測數據[9].定義事件、事件類以及事件結構構建認證理論，對協議強認證性質進行證明.

2.1.1 基本定義

1)Atom類型

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

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

2) 獨立性

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

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

3) 事件結構

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

計算系統語義通過事件結構語言描述，事件語言是任何語言的擴展.E,loc,<,info即事件序(event-ordering)，其中loc是事件E上的函數，<是事件E的一個因果關系，是一個本地有限集.事件包含有限個前驅.e∈E,loc(e)是事件存儲單元，info(e)表示事件發生時將消息交付給本地loc(e).e1

認證協議交互信息包括隨機數、簽名以及名字等元組信息，可以轉化為

Data≡defTree(Id+Atom).

事件結構中事件語言建模時需滿足：

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

②e1

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

④ 協議安全性證明中e′

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

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

2.1.2 加密系統建模

1) 隨機數n(nonce)

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

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

2) 事件類(event class)

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

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

若隨機數n∈E(Noncei),事件e∈E(X)沒有關聯，則(loc(e)≠si?X(e))‖Noncei(n).

類中事件轉換成原子X類中事件e信息包含原子a，則：

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

認證協議包含發送、接收、隨機數、簽名、認證、加密、解密7類事件[10]，事件類對應相關信息，信息類型取決于事件類，事件類中相關信息包含原子，基于7類事件類的形式化身份認證理論的類型列表具體定義如圖3所示：

Fig. 3 Event classes of the authentication theory
圖3 認證理論的事件類

在圖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進行簽名生成s.如果A是誠實主體，則loc(e)=A，誠實主體不會釋放私鑰.對于事件e′∈E(Verify)，該事件信息與簽名信息相對應即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生成時，對應解密公理AxiomD中存在一個匹配密鑰.

2.2 事件邏輯公理、推論及性質

2.2.1 事件邏輯公理

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

事件邏輯中PrivKey函數的主體包含原子，MatchingKeys函數構建密鑰間的關系，如圖4所示：

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

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)

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

3) 因果公理(causal axioms)

因果公理是對事件類中接收事件Rcv、驗證事件Verify、解密事件Decrypt所對應事件公理(接收公理AxiomR、驗證公理AxiomV、解密公理AxiomD)關系的整合.AxiomR,AxiomV相似，任何接收或驗證事件發生前存在一個與之相應且信息內容相同的發送或簽名事件[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相似，解密事件主體在事件發生前收到一個與之密鑰匹配、其他信息相同的加密事件,具體表示為

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

4) 不相交公理(disjointness axioms)

2個原子間不相交假設主要考慮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).

另一方面主體生成的隨機數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) 流關系(flow relation)

流關系是隨機數因果序事件間的關聯.Act類型包含7個事件類，記作actions.(ehasa)為真當且僅當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發生在同一主體上；

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

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

6) 隨機數公理(nonce axiom,AxiomF)

隨機數公理記為AxiomF，包含3部分AxiomF1,AxiomF2,AxiomF3，其中AxiomF1關于流性質，應用在事件關聯的隨機數中，具體為

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

2.2.2 事件邏輯引理及性質

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

引理 3.隨機數引理.

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

在協議強認證證明過程中，規定被證明協議合法，線程thr1相鄰事件e0,e1不存在發送動作(或任何的動作發生)，由隨機數引理可得，事件e1發生前隨機數不會被釋放.

安全協議形式化分析過程中，誠實主體在執行相關動作時需要滿足5個性質[19]：

性質1.多組合信息交互.

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

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

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

性質2.不疊加.

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

?A:Id.?e1,e2:e1

性質3.事件匹配.

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

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

性質4.去重復性.

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

性質5.去未來性.

在考慮匹配動作的過程中，以當前已發生事件為基準，對于之后沒有發生的動作不予考慮來減少驗證過程中的不必要進程.

2.3 形式化方法描述協議

1) 線程

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

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

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

thr1?thr2∨thr2?thr1.

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

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

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

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

2) 基本序列(basic sequence)

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

基本序列是2個位置與一個線程的聯系，當線程是基本序列給定的位置參數，則這個關系為真，基本序列類型成員為

Basic≡defId→Id→Thread→P.

注：其中P代表命題(proposition),在命題邏輯結構中跟布爾運算是不同的.

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

3) 匹配會話及協議動作

① 匹配會話

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

② 協議動作

使用基本協議動作描述協議ProtocolAction類來定義協議動作.所有成員類包含標簽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}.

協議動作pa(protocol action)對應事件e，則：

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

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

① 定義協議

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

協議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動作是基本序列的實例成員，如果動作是一個或多個實例成員，則實例是兼容的.

② 認證

主體A,B為誠實主體且遵守協議，主體A發起一個會話序列，主體B的一個應答序列與之構成合法匹配會話.類似地，如果主體B執行全應答序列的一個實例，那么有一個和主體A的匹配會話，即接收消息和相匹配的發送消息內容一致[10].消息雙方完成身份認證保證不會有攻擊者借助之前攔截消息進行偽裝會話攻擊，匹配會話過程滿足強匹配，協議Pr中基本序列bs認證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 安全協議證明過程

事件邏輯理論描述協議強認證性質，具體如圖5所示：

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

1) 定義基本序列

利用事件邏輯理論方法對安全協議進行形式化描述，定義發起者、響應者序列的具體動作[9]，規范協議基本序列，確認滿足協議安全性需要證明的強認證性質.

2) 對強認證性質的單向進行證明

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

3) 確定匹配事件，進行排除分析

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

4) 確認強認證性質

確認匹配會話屬于弱匹配，分析協議交互過程的匹配會話長度，根據相關公理確認強匹配會話.

5) 單向證明成立后，進行雙向強認證性質證明

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

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

3 事件邏輯理論證明WMN客戶端與LTCA認證協議

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

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

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

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

協議需要驗證的強認證性質為

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

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

證明. 假設誠實主體MU≠LTCA且遵守WMN客戶端與LTCA雙向認證協議，線程thr1是

Fig. 7 Basic sequence of two-way authentication protocol
圖7 雙向認證協議的基本序列

基本序

I

3

的實例，

e

0

<

loc

e

1

<

loc

…<

loc

e

6

為線程

thr

1

上的動作，那么事件

e

0

,

e

1

,…,

e

6

發生的主體為LTCA.對原子

則有：

(1)

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

① 事件e′中e′

② 事件e″中e″

③ 事件e′″中e′″

④ 事件e″″中e″″

對于事件發生的主體滿足：

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

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

(2)

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

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

可得到：

(3)

可得到：

(4)

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

Nseauth(I3,2).

證畢.

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

(5)

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

則事件發生主體滿足：

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

(6)

可得到：

(7)

可以得到：

(8)

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

Nseauth(R3,3).

證畢.

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

4 形式化方法對比分析

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

4.1 事件邏輯與模態邏輯比較

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

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

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

2) BAN邏輯對協議理想化處理過分依賴分析者直覺，理想化過程會產生問題，使得理想化后協議與原來協議有一定差距.例如忽略或增加協議前提或內容，對協議目標描述不夠準確，易造成分析結果與原協議設計有一定出入[20].事件邏輯理論定義嚴謹的數學規則，規范一系列公理推論規則約束，從而保證強認證性質證明過程的嚴謹性.

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

4) BAN邏輯規則定義相較事件邏輯理論更加成熟，研究方面更廣泛.在定義規則上，BAN邏輯規則可讀性更強，使用者不需要過高的數學基礎以及邏輯推理能力.在使用BAN邏輯證明過程中，使用者可以通過調用定義規則對目標進行證明.

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

4.2 事件邏輯理論與PCL比較

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

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

2) PCL方法在協議交互動作建模中不夠嚴謹，對描述線程的前序動作序列機制缺乏定義.事件邏輯理論方法對協議形式化建模線程機制進行明確定義，通過原子獨立性規范事件發生先后線程狀態.

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

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

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

4.3 事件邏輯通用性

事件邏輯理論對分布式系統協議和算法進行描述，通過捕捉分布式系統模型實現.在事件邏輯理論基本定義中，對原子類型、獨立性、事件結構進行初步建模，保證加密系統建模過程中隨機數、事件類建模的完備性.事件邏輯理論通用性具體表現在3個方面：

1) 復雜協議對象簡化處理

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

2) 協議交互環境合理化假設

有線網絡與無線網絡環境對于協議應用要求有很大不同，相較而言，無線網絡環境下安全協議設計有挑戰性.安全協議不僅要保證用戶能夠承受有線網絡信息傳遞過程遇到的風險，還要面臨無線網絡環境獨有的危險，對協議安全性認證也是挑戰.

① 不同協議適用條件有所不同，協議形式化描述前要對協議執行條件進行了解，對協議交互條件進行合理化分析.

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

② 對不同協議提出合理化假設條件，在合理假設條件中要求研究者了解協議運行的基本環境和獨特環境.在提出假設的過程中，假設條件不宜過多，反之體現協議運行條件的苛刻，對協議獨特的運行環境進行合理化提取.

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

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

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

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

5 結 論

5.1 總 結

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

1) 對事件邏輯理論進行擴展，提出置換規則保證協議交互用戶在置換中性質的等價轉換.將基于事件邏輯理論證明協議安全性的過程通過流程圖表述，詳細介紹事件邏輯理論證明過程.

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

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

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

5.2 展望

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

1) 事件邏輯理論證明方法更多依靠手工證明，此次對該方法各個步驟進行定義，下一步研究可以著手實現分布自動化.將分步實施的概念加入正在構建的安全協議驗證系統中，從而實現網絡安全協議認證性的自動化證明.

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

3) 事件邏輯理論在安全協議證明過程中可能存在不足，可以對事件邏輯理論相關推論性質進行分析擴展及證明.

4) 單一的形式化方法證明存在缺陷，可以考慮在安全協議的研究證明中結合模型檢測或模態邏輯等方法對協議安全屬性進行分析，從而保障安全協議強認證性質刻畫的完備性.