基于強認證理論的三方網(wǎng)絡協(xié)議安全性證明*

肖美華，劉欣倩,2+，李婭楠，程道雷，梅映天

1.華東交通大學 軟件學院，南昌 330013

2.中國人民財產(chǎn)保險股份有限公司寧波市分公司 信息技術部，浙江 寧波 315000

基于強認證理論的三方網(wǎng)絡協(xié)議安全性證明*

肖美華1，劉欣倩1,2+，李婭楠1，程道雷1，梅映天1

1.華東交通大學 軟件學院，南昌 330013

2.中國人民財產(chǎn)保險股份有限公司寧波市分公司 信息技術部，浙江 寧波 315000

XIAO Meihua,LIU Xinqian,LI Yanan,et al.Security certification of three-party network protocols based on strong authentication theory.Journal of Frontiers of Computer Science and Technology,2016,10(12)：1701-1710.

形式化方法是分析網(wǎng)絡安全協(xié)議的一種重要方法，網(wǎng)絡協(xié)議安全性也是信息安全領域的研究熱點。事件邏輯是一種描述分布式系統(tǒng)中狀態(tài)遷移的形式化方法，用于證明網(wǎng)絡安全協(xié)議的安全性。以事件邏輯為基礎，定義強匹配及匹配會話，結合事件邏輯公理和推理規(guī)則，提出了強認證理論。利用該理論對有3個主體的Neuman-Stubblebine協(xié)議進行了研究，分析得出發(fā)送者是安全的而接收者是不安全的，從而證明了該協(xié)議是不安全的，說明了強認證理論適用于三方的網(wǎng)絡安全協(xié)議。該理論適用于類似多方網(wǎng)絡安全協(xié)議的安全性證明。

形式化方法；事件邏輯；強認證理論；Neuman-Stubblebine協(xié)議

1 引言

證明網(wǎng)絡協(xié)議的安全屬性是一個復雜的問題。形式化方法是一種強大的證明網(wǎng)絡協(xié)議的安全屬性的方法，其包括模態(tài)邏輯、定理證明和模型檢測[1]。模態(tài)邏輯和定理證明又可籠統(tǒng)地歸為一類。模型檢測自動化程度高，用來驗證系統(tǒng)的不安全性，但是只能對有限數(shù)量的并行通信進行研究，難以解決狀態(tài)爆炸問題。基于定理證明的形式化分析方法是對協(xié)議進行建?；驅f(xié)議需滿足的性質進行形式化描述，再用定理證明的技術來證明性質是否在協(xié)議模型中被滿足。定理證明最大的優(yōu)點是避免了模型檢測中狀態(tài)爆炸的問題，缺點是證明過程難以完全自動化，并需要有一定的專業(yè)知識。許多學者對定理證明方法進行了深入的研究，并取得了非凡的成就[2-5]。

事件邏輯[6-13]是由美國康奈爾大學的Bickford等人于2003年提出的一種定理證明方法，是一種描述分布式系統(tǒng)下協(xié)議和算法的邏輯，可以對安全協(xié)議一些基本原語進行形式化規(guī)約[6]。它采用標準邏輯概念，對安全協(xié)議的7種動作，即生成挑戰(zhàn)數(shù)、發(fā)送消息、接收消息、加密、解密、簽名和驗證，進行形式化描述，同時給出協(xié)議中密鑰、挑戰(zhàn)數(shù)和協(xié)議消息的形式化描述。本文以事件邏輯為基礎，定義強匹配及匹配會話，結合事件邏輯公理和推理規(guī)則，提出強認證理論。專注于將網(wǎng)絡安全協(xié)議用形式化描述后，在符合強認證理論條件下，利用強認證理論，可證明協(xié)議的安全性。

本文結構安排如下：第2章簡要介紹事件邏輯形式化理論，該部分貫穿全文；第3章形式化定義強認證理論；第4章對Neuman-Stubblebine協(xié)議進行詳細證明；第5章為結論。

2 事件邏輯

事件邏輯是一種描述并發(fā)與分布式系統(tǒng)下協(xié)議和算法的邏輯。

2.1 符號說明

該部分描述分析密碼協(xié)議安全性質的符號和操作符語義。表1給出一些符號及其語義。

2.2 基本概念及定義

（1）Atom

一個atom類（Atom）來表示秘密信息，其中的成員用atoms來表示。

（2）獨立性原始命題

(x:T||a)表示類型T中的x不包含原子a。當類型T從上下文中很明顯看出時，可用x||a來表示x和a獨立。

（3）事件結構

事件語言是任何語言的擴展 E,loc,＜,in fo，這里loc是E上的函數(shù)，＜是E上的一個關系，對于e∈E，loc(e)是事件的存儲單元，e1＜e2表示事件e1在事件e2之前發(fā)生。事件結構中存儲單元表示主體、進程或線程。事件結構是滿足下邊公理的建模：

①≤表示局部有限偏序（每個事件e有有限個前驅）；

② e1＜loce2≡e1＜e2∧loc(e1)=loc(e2)表示局部序，是一個有相同存儲單元的事件集的全序；

③in fo(e)和事件e的原始信息相關，通常事件e發(fā)生時這個消息轉發(fā)給loc(e)認證理論中，loc(e)是事件e發(fā)生的主體，因此對一些標識符A來說loc(e)=A。

本文將(e′＜e∧loc(e′)=loc(e))縮寫為e′＜loce。

Table 1 Basic symbols and semantics of event logic表1 事件邏輯的基本符號和語義

（4）事件類

將身份認證協(xié)議中的事件進行分類，其中存在發(fā)送、接收、挑戰(zhàn)數(shù)、簽名、驗證、加密和解密事件。每類中的事件都有相關信息，且這些信息的類型由事件類決定。定義如下：

2.3 相關公理及規(guī)則

事件邏輯包括6種公理，這6種公理分別為密鑰公理、因果公理、不相交公理、誠實公理、流關系和隨機數(shù)公理。下面簡要介紹證明過程中需要用到的公理。

（1）因果公理

因果公理包含3個公理，將Rcv類、Verify類和Decrypt類的相關事件公理表示為 AxiomR公理、AxiomV公理和AxiomD公理，與之前相應的Send類、Sign類和Encrypt類中的事件因果對應。AxiomR公理和AxiomV公理相似，也就是說在任何接收或者驗證事件之前必須有一個具有相同相關信息的發(fā)送或者簽名事件。

AxiomD與AxiomR公理類似，解密事件與之前的加密事件擁有相同的相關信息，但是密鑰是一個匹配密鑰而不是相同密鑰。

（2）誠實公理

誠實主體不釋放它們的私鑰，因此簽名事件擁有誠實的簽名者；誠實主體私鑰的加密事件和解密事件必須發(fā)生在該主體，稱這個公理為AxiomS。

（3）隨機數(shù)公理

將隨機數(shù)公理記為AxiomF，包括三部分。第一部分為：

AxiomF的其他兩部分聲明了簽名、密文和包含它們的事件之間的相似關系。不同的是，沒有假設的簽名和加密總與特殊事件有關，因此如果一個行為包含簽名或者密文，只能推斷出具有相同信息的一些簽名或者加密動作，流關系如下：

引理3如果e1,e2∈E(New)且New(e1)=New(e2)，則e1=e2。

引理4（隨機數(shù)釋放引理）如果協(xié)議Protocol(bss)是合法的，A是誠實主體且遵守Pr，且thr是基本序列bss的一個實例，n=thr[j]，n∈E(New)，e=thr[i]和j＜i，那么如果j和i之間沒有一個k是E(Send)中的thr[k]，則隨機數(shù)New(n)不在e之前釋放。

2.4 基本序列

基本序列本質上是協(xié)議動作的一個參數(shù)列表，其中兩個參數(shù)是主體的標識符，記為A和B。遵守協(xié)議的主體A可以參與到任何多個線程中，其中任何一個線程都是協(xié)議基本序列的一個實例，且任何可能不同的主體都扮演著B的角色，并且允許基本序列中超過兩個主體。

如果主體A中的每一個動作都是它基本序列中的一個實例成員，則稱主體A遵守協(xié)議；如果簽名和密文動作不正確，那么驗證和解密動作在一個序列中不會出現(xiàn)。相似地，如果其他主體失效或者行為不當，那么下一個序列中的接收動作可能不會出現(xiàn)。

一般情況下，一個基本序列是兩個主體（也可以是多個主體）和一個線程的關系。當線程是已給主體基本序列中的一個實例，那么關系為真。因此，基本序列是Basic類型的一個成員。

一個基本序列用一個自由變量協(xié)議動作列表來定義，所有自由變量，除了A和B都解讀為原子。由于基本序列的每一個實例可能生成不同的隨機數(shù)、簽名等，在序列定義的關系中原子參數(shù)存在量化。如果loc(thr)=A∧?B:Id.?b∈bss.b(A,B,thr)，那么線程thr是主體A中已知bss列表基本序列關系中的一個，記作thr=oneof(bss,A)。

關系inoneof(e,thr,bss,A)用協(xié)議的形式化定義為：e∈thr∧thr=oneof(bss,A)。

3 強認證理論

以事件邏輯為基礎，定義強匹配及匹配會話，結合事件邏輯公理和推理規(guī)則，得出強認證理論。本文分線程、匹配會話和認證三部分說明。

3.1 線程

在單個主體中線程是動作的一個有序列表。

如果第一個發(fā)送和第二個接收具有相同的信息，那么s和r這兩個消息是一個弱匹配。如果s是r的前因，那么它們構成一個強匹配。

3.2 匹配會話

線程thr1和thr2構成一個長度為n的匹配會話，如果它們都包含至少n個消息，且當每個線程中的前n個消息是成對的，每對滿足m1?m2∨m2? m1。這種情況下，定義強匹配會話，記作。如果每一對只滿足m1～m2∨m2～m1，得到一個弱匹配會話，記作。

一個協(xié)議保證在不同主體上，兩個線程之間的一個強匹配會話，稱該協(xié)議滿足一個強身份認證性質，這種理論稱為強認證理論。強性質防止重放攻擊并且比省略因果序要求的對應的弱認證性質更難證明。

3.3 認證

如果主體A執(zhí)行一個具有參數(shù)B的全部發(fā)起者序列中的一個實例，那么倘若B是誠實主體，且也遵守相應的協(xié)議，需要主體B的一個應答序列實例與協(xié)議中前兩個消息構成一個匹配會話（不能保證主體A發(fā)送的第三個消息將會被主體B接收到）。類似的，如果主體B執(zhí)行全應答序列中的一個實例，那么應該有一個和主體A匹配的會話。

強認證理論的形式化定義指出協(xié)議中基本序列bs認證n個消息的Pr。

4 Neuman-Stubblebine協(xié)議證明

本章運用上文強認證理論分析證明Neuman-Stubblebine協(xié)議。

4.1 協(xié)議的形式化分析及描述

Neuman-Stubblebine協(xié)議[14-15]是一個基于隨機數(shù)的，以通過服務器來實現(xiàn)通信主體的雙向認證以及會話密鑰分配為目標的安全協(xié)議。認證過程主要分為兩個階段：第一階段為初始認證階段，由通過服務器實現(xiàn)發(fā)起者和響應者的雙向身份認證和會話密鑰分配的4條消息組成；第二階段為繼認證階段，由通過服務器實現(xiàn)發(fā)起者與響應者的再次身份認證的3條消息組成。密鑰服務器在后繼認證階段不再參與該協(xié)議。本文只針對初始認證階段的安全性進行研究。協(xié)議交換過程如圖1所示。

（1）A→B：A，RA

（2）B→S：A，B，RB，{A，RA，TB}KB

（3）S→A：{B，RA，K，TB}KA，{A，K，TB}KB，RB

（4）A→B：{A，K，TB}KB，{RB}K

利用事件邏輯對Neuman-Stubblebine協(xié)議進行基本序列排序，協(xié)議描述如圖2所示。

Fig.1 Neuman-Stubblebine protocol圖1 Neuman-Stubblebine協(xié)議

Neuman-Stubblebine協(xié)議的基本序列如下：

4.2 協(xié)議證明過程

利用之前定義的基本序列關系，定義Neuman-Stubblebine協(xié)議為Protocol([I1,I2,I3,R1,R2,R3,S1,S2])。要驗證的強身份認證性質為：

證明 假設誠實主體A≠B≠C且遵守Neuman-Stubblebine協(xié)議，并假設線程thr1是I3的一個實例。令e0＜loce1＜loc…＜loce5為thr1上的動作，那么e0,e1,…,e5的主體均為A。對一些atomsm,n,K,TB,s′,s″有：

根據(jù)AxiomD和AxiomS，存在一個事件e′使得e′＜e3∧DEMatch(e3,e′)∧loc(e′)=B∨loc(e′)=C成立。那么。

Fig.2 Description of Neuman-Stubblebine protocol圖2 Neuman-Stubblebine協(xié)議描述

因為B、C都遵守Neuman-Stubblebine協(xié)議，動作e′必須為協(xié)議的基本序列之中的一個實例成員。唯一一些包含Encrypt(_)動作的是I3、R1、R2、R3、S2，接下來逐個證明。

如果e′是I3中的一個實例，那么對于一些atoms m1,n1,K1,s1′′和主體D，有e0′＜loce′，如此：，但是明顯不符要求，因此I3排除。

如果e′是R1中的一個實例，那么對于一些atoms m2,n2,TB2,s2和主體E，在主體B上存在事件 e0′,e1′, e2′,e3′，如此得：

明顯不符合要求，排除R1。同理，排除R2和R3。

如果e′是S2中的一個實例，那么對于一些atoms m3,n3,K3,TB3,s3,s3′,s3′和主體F、G，在主體C上存在事件e0′,e1′,e2′,e3′,e4′,e5′，有：

即e3′=e′，因此有F=B,m3=m,k3=k,TB3=TB,s3′=s′，可得：

這樣，又必須存在一個事件e″使得e″＜e1′∧DEMatch(e1′,e″)∧loc(e′)=A∨loc(e′)=B成 立。 那 么。因此動作e″必須為協(xié)議基本序列中的一個實例成員。唯一一些包含Encrypt(_)動作的是I3、R1、R2、R3、S2，逐個證明。

如果e″是I3上的一個實例，那么對于一些atoms m4,n4,K4,TB4,s4′,s4′,s4′′和主體H，在主體A中有事件e0′,e1′,e2′,e3′,e4′，得：

由此可見明顯不符合要求，排除I3。

如果e″是S2上的一個實例，那么對于一些atoms m5,n5,K5,TB5,s5,s5′,s5′和主體J、L，在主體C中有事件e0′,e1′,e2′,e3′,e4′,e5′，得：

可以看到明顯不符要求，排除S2。

如果e″是R1上的一個實例，那么對于一些atoms m6,n6,TB6,s6和主體O，在主體B中有事件e0′,e1′,e2′, e3′，得：

即e2′=e″，因此有O=G,m6=m，TB6=TB,s6=s3，可得：

由引理4可知，在隨機數(shù)m釋放之前不會產(chǎn)生一個相同的隨機數(shù)m，因此在Rcv(e0′)=G,m=A,m中G=A，將之代入式（1）和式（2）中，得：

通過引理4可知，在Send(e5′)=n3,s′,s3′中n3= n,s3′=s″，再將之代入式（3）中，得：

因此可以得到Send(e1)=A,m=Rcv(e0′)和Rcv(e2)= n,s′,s″=Send(e5′)。這樣就有一個長度為2的（弱）匹配會話。

要想有一個強匹配會話，必須證明e1＜e0′和e5′＜e2。由上文可知通過AxiomF、引理2和假設A≠D，它遵循在e0和e0′之間存在一個發(fā)送事件S釋放隨機數(shù)m。如果e1≤j，那么得到的排序為e1＜e0′，再排除e0＜locj＜loce1。如果e0＜locj＜loce1，那么j必須為A的一些其他線程的成員，由引理4可知在線程thr1中e0和e1之間不存在發(fā)送動作，意味著隨機數(shù)m在e1之前不會釋放，這是AxiomF證明e1＜e0′所需要的部分。此外還必須證明e5′＜e2。這也可由AxiomF和引理4推斷出，因為e2擁有n且n=New(e2′)在e5′之前不釋放。

NSe?auth(I3,2)得證。 □

接下來，證明NSe?auth(R3,3)。

證明 假設誠實主體A≠B≠C且遵守Neuman-Stubblebine協(xié)議，并假設線程thr1是R3的一個實例。令e0＜loce1＜loc…＜loce5＜loce6為thr1上的動作，那么 e0, e1,…,e6的主體均為B。對一些atomsm,n,TB,s,s″,s?有：

因為A、C都遵守Neuman-Stubblebine協(xié)議，動作e′、e″必須為協(xié)議基本序列中的一個實例成員。唯一一些包含Encrypt(_)動作的是I3、R1、R2、R3、S2，使用在證明時排除I3的方法，可以排除R1、R2、R3。接下來證明I3、S2。

如果e′或者e″是I3中的一個實例，那么對于一些atomsm1,n1,K1,TB1,s1′,s1′,s1′′和主體D、E，在主體A上存在事件e0′,e1′,e2′,e3′,e4′,e5′，有：

這樣，又必須存在一個事件 e?使得 e?＜e3′∧DEMatch(e3′,e?)∧loc(e?)=B∨loc(e?)=C成立。那么。

因為主體都遵守Neuman-Stubblebine協(xié)議，動作e?必須為協(xié)議基本序列中的一個實例成員。唯一一些包含Encrypt(_)動作的是I3、R1、R2、R3、S2，與上文排除法相同，排除I3。

如果e?是R1中的一個實例，那么對于一些atoms m2,n2,TB2,s2和主體F，在主體B上存在事件e0′′,e1′′, e2′′,e3′′，有：

明顯不符合要求，排除R1。同理R2和R3排除。

如果e?是S2中的一個實例，那么對于一些atoms m3,n3,K3,TB3,s3,s3′,s3′和主體G、H，在主體C上存在事件e0′′,e1′′,e2′′,e3′′,e4′′,e5′′，有：

即e3′′=e?，因此有G=E,m3=m1,K3=K,TB3=TB1,s3′= s1′，得：

現(xiàn)在回過頭來看e″，如果e″是也S2中的一個實例，那么對于一些atomsm4,n4,K4,TB4,s4,s4′,s4′和主體J、L，在主體C上存在事件e0′,e1′,…,e5′，有：

必須有Encrypt(e3′)=Encrypt(e″)或Encrypt(e4′)=Encrypt(e″)。

即e4′=e″，于是L=A,K4=K,TB4=TB,s4′=s″，因此有：

由引理4可知，m4=m，可得s4=s，有：

如果要證NSe?auth(R3,3)，就必須先證明有三對（強）匹配會話，而要證明（強）匹配會話，首先要有（強）匹配。即如果要證明NSe?auth(R3,3)，就必須有：

由式（6）、（7）、（9）不能證明A=D和m=m1，證明結束。 □

Neuman-Stubblebine協(xié)議只能證明第一個強認證性質，因此可以認為不符合強認證理論，存在消息重放的可能性，響應者是不安全的。說明Neuman-Stubblebine協(xié)議的初始認證階段不能夠達到雙向身份認證，可能存在由于消息重放引起的類型攻擊。

5 結束語

本文以事件邏輯為基礎，定義強匹配及匹配會話，結合事件邏輯公理和推理規(guī)則，提出強認證理論。利用該理論對有3個主體的Neuman-Stubblebine協(xié)議進行研究，首先對協(xié)議基本序列進行合法定義，其次分別證明發(fā)送者和接收者的安全性。證明得出發(fā)送者是安全的而接收者是不安全的，不能達到雙向身份認證，是不安全的協(xié)議，說明強認證理論適用于三方的網(wǎng)絡安全協(xié)議。認證協(xié)議可以通過只對協(xié)議誠實主體動作的推理來證明其認證性，強認證理論適用于多個主體的網(wǎng)絡安全協(xié)議認證性分析。

[1]Li Yan,Huang Guangqiu,Zhang Bin.Markov evolutionary game model for dynamic network attacks safety analysis[J]. Journal of Frontiers of Computer Science and Technology, 2016,10(9):1272-1281.

[2]Datta A,Derek A,Mitchell J C,et al.Protocol composition logic[J].Electronic Notes in Theoretical Computer Science, 2007,172:311-358.

[3]Constable R L.On building constructive formal theories of computation noting the roles of turing,church,and brouwer [C]//Proceedings of the 27th Annual IEEE Symposium on Logic in Computer Science,Dubrovnik,Croatia,June 25-28,2012.Piscataway,USA:IEEE,2012:2-8.

[4]Berg M.Formal verification of cryptographic security proofs[R]. Faculty of Natural Sciences and Technology,Department of Computer Science,Saarland University,2013.

[5]Lu Laifeng,Duan Xindong,Ma Jianfeng.Improvement and formal proof on protocol Otway-Rees[J].Journal on Communications,2012,33(S1):250-254.

[6]Bickford M,Constable R L.A logic of events,TR2003-1893[R]. Cornell University,2003.

[7]Bickford M,Constable R L.Automated proof of authentication protocols in a logic of events[C]//Proceedings of the 6th International Verification Workshop,Edinburgh,Jul 20-21,2010:13-30.

[8]Bickford M.Unguessable atoms:a logical foundation for security[C]//LNCS 5295:Proceedings of the 2nd International Conference on Verified Software:Theories,Tools and Experiments,Toronto,Canada,Oct 6-9,2008,Berlin,Heidelberg:Springer,2008:30-53.

[9]Bickford M,Constable R L.Formal foundations of computer security[J].NATO Science for Peace and Security Series, D:Information&Communication Security,2008,14:29-52.

[10]Liu Xinqian,Xiao Meihua,Cheng Daolei,et al.Security authentication of the modified Needham-Schroeder protocol based on logic of event[J].Computer Engineering&Science,2015,37(10):1850-1855.

[11]Chien H Y,Wu T C,Yeh M K.Provably secure gatewayoriented password based authenticated key exchange protocol resistant to password guessing attacks[J].Journal of Information Science&Engineering,2013,29(2):249-265.

[12]Xiao Meihua,Bickford M.Logic of events for proving security properties of protocols[C]//Proceedings of the 2009 International Conference on Web Information Systems and Mining,Shanghai,Nov 7-8,2009.Washington:IEEE Computer Society,2009:519-523.

[13]Xiao Meihua,Ma Chenglin,Deng Chunyan.A novel approach to automatic security protocol analysis based on authentication event logic[J].Chinese Journal of Electronics,2015,24 (1):187-192.

[14]Li Xiehua,Gao Chunming.Efficient protocol-proving algorithm based on improved authentication tests[J].Computer Science,2009,36(4):73-76.

[15]Ding Mengwei,Zhou Qinglei,Zhao Dongming.The strand space model of Neuman-Stubblebine protocol and its analysis[J].Computer Applications and Software,2009,26(5): 37-39.

附中文參考文獻：

[1]李艷,黃光球,張斌.動態(tài)攻擊網(wǎng)絡Markov演化博弈安全分析模型[J].計算機科學與探索,2016,10(9):1272-1281.

[5]魯來鳳,段新東,馬建峰.Otway-Rees協(xié)議改進及形式化證明[J].通信學報,2012,33(S1):250-254.

[10]劉欣倩,肖美華,程道雷,等.基于事件邏輯的改進Needham-Schroeder協(xié)議安全性證明[J].計算機工程與科學,2015, 37(10):1850-1855.

[14]李謝華,高春鳴.基于改進認證測試理論的高效安全協(xié)議驗證算法[J].計算機科學,2009,36(4):73-76.

[15]丁萌偉,周清雷,趙東明.Neuman-Stubblebine協(xié)議的串空間模型及分析[J].計算機應用與軟件,2009,26(5):37-39.

XIAO Meihua was born in 1967.He received the Ph.D.degree in computer software and theory from Institute of Software,Chinese Academy of Sciences in 2007.From 2008 to 2009,he worked as a visiting scholar at Cornell University.Now he is a professor and Ph.D.supervisor at School of Software,East China Jiaotong University.His research interests include information security and software formal method,etc.

肖美華（1967—），男，江西南昌人，2007年于中國科學院軟件研究所計算機軟件與理論專業(yè)獲得博士學位，2008年至2009年于美國康奈爾大學做訪問學者，現(xiàn)為華東交通大學教授、博士生導師，主要研究領域為信息安全，軟件形式化方法等。

LIU Xinqian was born in 1990.She is an M.S.candidate at School of Software,East China Jiaotong University. Her research interests include information security and software formal method,etc.

劉欣倩（1990—），女，遼寧營口人，華東交通大學軟件學院碩士研究生，主要研究領域為信息安全，軟件形式化方法等。

LI Yanan was born in 1992.She is an M.S.candidate at School of Software,East China Jiaotong University. Her research interests include information security and software formal method,etc.

李婭楠（1992—），女，河南洛陽人，華東交通大學軟件學院碩士研究生，主要研究領域為信息安全，軟件形式化方法等。

CHENG Daolei was born in 1991.He is an M.S.candidate at School of Software,East China Jiaotong University. His research interests include information security and software formal method,etc.

程道雷（1991—），男，江西上饒人，華東交通大學軟件學院碩士研究生，主要研究領域為信息安全，軟件形式化方法等。

MEI Yingtian was born in 1992.She is an M.S.candidate at School of Software,East China Jiaotong University. Her research interests include information security and software formal method,etc.

梅映天（1992—），安徽池州人，華東交通大學軟件學院碩士研究生，主要研究領域為信息安全，軟件形式化方法等。

Security Certification of Three-Party Network Protocols Based on Strong Authentication Theory*

XIAO Meihua1,LIU Xinqian1,2+,LI Yanan1,CHENG Daolei1,MEI Yingtian1
1.School of Software,East China Jiaotong University,Nanchang 330013,China
2.Department of Information and Technology,PICC Property and Casualty Company Limited(Ningbo Branch), Ningbo,Zhejiang 315000,China
+Corresponding author:E-mail:liuxinqianlxq@sina.com

Formal method is an important approach for analyzing network security protocols.Network protocol security is a research hotspot in information security field.Event logic is a formalism for describing transition between states in a distributed system.It’s common to use event logic to certify the security of network security protocols. Based on event logic,this paper defines strong match and match sessions,and proposes the strong authenticationtheory by combining event logic axioms and inference rules.Using the strong authentication theory,this paper proves that three-principal Neuman-Stubblebine protocol is not secure because the sender is secure and the receiver isn’t secure.The research results show that the strong authentication theory is applicable to the security certification of similar multi-party security protocols.

formal method;event logic;strong authentication theory;Neuman-Stubblebine protocol

10.3778/j.issn.1673-9418.1607032

A

TP309

*The National Natural Science Foundation of China under Grant Nos.61163005,61562026(國家自然科學基金);the Natural Science Foundation of Jiangxi Province under Grant Nos.20132BAB201033,20161BAB202063(江西省自然科學基金);the Science and Technology International Cooperation Project of Jiangxi Province under Grant No.20151BDH80005(江西省對外科技合作技術項目);the Soft Science Research Project of Jiangxi Province under Grant No.20151BBA10042(江西省軟科學研究計劃項目);the Science and Technology Ground Project of College in Jiangxi Province under Grant No.KJLD13038(江西省高?？萍悸涞赜媱濏椖?;the Program of Co-Innovation Center of the Intelligent Management and Equipment for Orchard on the Hilly Land in South China (南方山地果園智能化管理與裝備協(xié)同創(chuàng)新中心資助項目);the Special Funds for Visiting Scholars Development Plan of the Young Teachers in the Ordinary Universities of Jiangxi Province(江西省普通本科高校中青年教師發(fā)展計劃訪問學者專項資金).

Received 2016-07,Accepted 2016-09.

CNKI網(wǎng)絡優(yōu)先出版:2016-09-08,http://www.cnki.net/kcms/detail/11.5602.TP.20160908.1045.020.html