1 引言
SVO邏輯[1]是P.Syverson和P.C.Van Oorschot于1994年對BAN邏輯進行改進后提出來的一種邏輯化推導方法，它吸取了BAN[2]邏輯、GNY邏輯[3]、AT邏輯[4]和VO邏輯[5]的優點，同時又具有十分簡潔的推理規則和公理。但是SVO邏輯因為其自身局限，在分析認證協議方面仍然存在不足。本文通過增加SVO邏輯的推理規則以及公理，對SVO邏輯進行了擴展，使其可以更好的分析認證協議。并利用擴展的SVO邏輯對Needham-Schroeder認證協議[6]進行了分析，說明本文對SVO邏輯的改進是有效的。
2 SVO邏輯符號說明及其推理規則
2.1 邏輯符號
設實際協議的主體用A和B表示，可信的第三方用S表示。Na和Nb為隨機數。A和
B之間的共享密鑰用Kab表示，類似的還有Kas和Kbs。用密鑰K加密消息M表示為
{M}K。
P|≡X:表示協議從開始到結束整個過程中P一直相信X。
P  X:表示P可見X，也就是P接收到了X。
P| X:表示P在某時發送了一個包含X的消息，但不能確定它是何時發送的。
P| X:表示P對X有仲裁權。
#(X):表示X是新鮮的。
P Q：表示密鑰K只為P和Q所知。
| P：表示K是P的公鑰， 是P的私鑰，只能是P擁有或者P相信的實體擁有。
P Q：表示秘密X只為P和Q所知。
{X}K:表示用K加密X。
<X>Y:表示X和秘密Y的組合，Y的出現證明了誰發送了<X>Y。
(X,Y):表示消息X和消息Y的組合消息。
如果 是一個公式，那么下列表示也是一個公式，P|≡：P相信為真，并不意味著為真。如果1和2是公式，那么1 2、1 2和1→2都是公式。
2.2 推理規則
SVO邏輯的兩條基本推理規則是：
MP規則:由 和  可以推導出；Nec規則:由|-可以推導出|-P|≡。
(1)消息含義規則(Message-meaning rules)：
M1: ； M2: ；
M3: ； M4:
(2)隨機數驗證規則(Nonce-verification rule)： N1:
(3)管轄權規則(Jurisdiction rule)： J1:
(4)信任規則(Believing rules)：
B1: ； B2: ；
B3: ； B4:
5)消息接受規則(Receiving rules)：
R1: ； R2: ；
R3: ；R4: ；
R5:
6)新鮮性規則(Fresh rules)： F1: ； F2:
3 對SVO邏輯的改進
SVO邏輯對NS認證協議進行形式化分析的主要目的是要探索使用消息新鮮性規則對認證協議中重放攻擊的相關問題和解決辦法。分析SVO邏輯的隨機數驗證規則發現，在消息中合適位置加入新鮮元素可以擴展協議主體的信仰從而避免重放攻擊。對于NS協議只要消息M3中有新鮮元素的時候就能推導出B相信會話密鑰Kab是用
于A和B之間進行通信的密鑰。為了更好的分析和證明NS協議，本文在文獻[7]
的基礎上對SVO邏輯的隨機數驗證規則進行了改進，提出一條消息只有在新鮮性、完整性和時限性都滿足的同時，才能得到發送方剛剛說過此消息的結論。
隨機數驗證規則： :
時限性的符號說明:T(X)表示消息X的時戳,只有當消息上的時戳與當前本地時
間的差值在一定范圍內，接收方才接收這個消息。為了能更好的形式化分析NS
認證協議，本文還添加了以下消息時限性規則：
消息時限性規則：T1: ；T2:
公式T1表示用只有通信雙方知道的密鑰K加密的消息X具有時限性。T2說明如果一個消息串具有時限性，則它的各個子消息也具有時限性，但是這個公式不可以倒過來推導。T3中F(X)是某個密鑰協商函數，它表示如果這個函數如果有時限性，則它所對應的消息也具有時限性。
4 Needham-Schroeder協議形式化分析
4.1 Needham-Schroeder認證協議描述
這個協議由Roger Needham和Michael Schroeder于1978年發明，該協議可描述如下：
M1 A→S： A，B，Na；
M2 S→A： {Na，B，Kab，{Kab，A}Kbs}Kas；
M3 A→B： {Kab，A}Kbs；
M4 B→A： {Nb}Kab；
M5 A→B： { Nb-1}Kab。
具體分析過程可參考文獻[2]。從文獻[2]可知，協議無法確保會話密鑰Kab的新
鮮性，因此一個入侵者有足夠的時間得到一個舊的會話密鑰并重用。更糟糕的
是，如果主體A的私鑰被竊取，入侵者能使用A的私鑰來得到會話密鑰與任何其
他的協議主體進行通信，即使A的私鑰改變了仍然可以使用這些會話密鑰，因
為協議無法驗證會話密鑰Kab的新鮮性。
4.2 改進的NS認證協議分析
4.2.1 NS協議的改進
針對上述NS認證協議的缺陷及易受到的攻擊，參照文獻[8]的改進協議如下：
M1：A→S: A，B，Na； M2：S→B: A； M3：B→S: ；
M4：S→A: {Na，B，Kab }Kas； M5：S→B: {Kab，A,  }Kbs；
M6：B→A： {Nb, Kab}Kab； M7：A→B： {Kab,Nb-1}Kab
4.2.2 改進的NS協議的形式化證明
下面應用改進的SVO邏輯形式化分析改進的NS協議。
NS協議的安全目標可以形式化的歸納為：
G1 A|≡A B G2 B|≡A B
G3 A|≡B|≡AB G4 B|≡A|≡AB
首先給出該協議中關于主體A的初始條件如下：
A1：A|≡#(Na)； A2：A|≡A S； A3：A|≡S| AB
A4：A|≡S|A B； A5：A{Na,B,AB}kas
A6：A|≡A{Na,B,AB}kas； A7: A|≡S|{Na,B,AB}kas
上述初始條件反應了主體A的初始信念(A1,A2,A3,A4)，接受消息(A5)，理解消息(A6)，解釋消息(A7)。下面開始分析：
由A2應用T1和Nec規則可得 A|≡T(Na,B,AB) (1)
由A5和A7應用R3，M4和MP規則可得A|≡S|{Na,B,AB} (2)
由A1應用F1和Nec規則可得 A|≡#(Na,B,AB) (3)
由(1)，(2)和(3)應用 規則可得 A|≡S|≡{Na,B,AB} (4)
由(4)應用B3規則可得 A|≡S|≡AB (5)
由(5)和A3、A4可得 A|≡AB (6)；A|≡#(AB) (7)
證明了安全目標G1。
關于主體B的初始條件如下：
B1：B|≡#(Nb)； B2：B|≡B  S； B3：B|≡S| AB
B4：B|≡S|AB； B5：B{AB,B,}kbs
B6：B|≡B{AB,B,}kbs； B7: B|≡S|{AB,B,}kbs
上述初始條件反應了主體B的初始信念(B1,B2,B3,B4)，接受消息(B5)，理解消息(B6)，解釋消息(B7)。下面開始分析：
由B2應用T1和Nec規則可得 B|≡T(AB,A,) (8)
由B5和B7應用R3，M4和MP規則可得 B|≡S|{AB,A,} (9)
由B1應用F1和Nec規則可得 B|≡#(AB,A,) (10)
由(6)，(7)和(8)應用規則可得 B|≡S|≡{AB,A,} (11)
由(9)應用B3規則可得 B|≡S|≡AB (12)
由(10)和B3、B4可得 B|≡AB (13)；B|≡#(AB) (14)
證明了安全目標G2。
由(1)應用T2規則可得 A|≡T(AB) (15)
由消息M6可得 A{Nb,AB}kab (16)
由(16)、(6)、(7)和M3規則可得 A|≡B|{Nb,AB} (17)
由(17)和M4規則可得 A|≡B|(AB) (18)
由(18)和(7)、(15)應用規則可得 A|≡B|≡AB (19)
證明了安全目標G3。
由(8)應用T2規則可得 B|≡T(AB) (20)
由消息M7可得 B{AB,Nb-1}kab (21)
由(21)、(13)、(14)和M3規則可得 B|≡A|{AB,Nb-1} (22)
由(22)和M4規則可得 B|≡A|(AB) (23)
由(23)和(14)、(20)應用規則可得 B|≡A|≡AB (24)
證明了安全目標G4。
這一分析結果表明，運用改進的SVO邏輯形式化分析NS協議后，主體A和B都
相信Kab是適合與他們雙方通信的非確信共享會話密鑰，而不用再借助假設B|
≡#(Kab),從而滿足了消息新鮮性規則，從而所以有效抵御了重放攻擊。
5 結論
SVO邏輯方法是安全協議形式化分析的一種簡單有效的形式化方法，它的提出標志著BAN類邏輯方法已經走向成熟。它被廣泛應用于多種安全協議的形式化分析，并且取得了巨大成功。文中通過增加和改進SVO邏輯的推理規則以及公理，提出了一種改進的SVO邏輯，并用改進的邏輯來分析了NS協議。通過對以前各個學者運用原始的SVO邏輯分析協議進行比較，發現改進的SVO邏輯在形式化分析NS認證協議方面能有效保持消息新鮮性規則并抵御消息重放，從而說明對SVO邏輯的擴展改進是切實有效的，同時這些工作對于安全協議形式化分析的一些其他方法同樣具有借鑒意義。
參考文獻 (References)
[1] Syverson, Oorschot. On unifying some authentication protocol logic. In: IEEE Computer Society Symp on Research in Security and Privacy. Washington: IEEE Computer Society Press, 1994.14-28.
[2] Burrows, Abadi and Needham. A Logic of Authentication[R]. Technical Report 39, CANADA: DEC Systems Research Center, 1989.Parts and Versions of This material Have Been Presented in Many Places Including ACM Transactions Computer Systems, 1990, 8(1):18-36.
[3] Li Gong, Needham, YAHALOM. Reasoning about belief in cryptographic protocol [A]. Proc of the 1990 IEEE Computer Society Symp on Research in Security & Privacy [C]. USA: IEEE Computer Society, 1990. 234-248.
[4] Abadi, TUTTLE. A Semantics for a logic of authentication [A]. Proc 10th Annual ACM Symp on Principles of Distributed Computing [C]. USA: ACM, 1991. 201-216.
[5] Vanoorscho. Extending cryptographic logics of belief to key agreement protocols (extended abstract) [A]. In Proceedings of the First ACM Conference on Computer and Communications Security [C]. Virginia, USA, 1993.
[6] Needham, Schroeder. Using Encryption for Authentication of Large Networks of Computers [J]. Communication of the ACM, 1978, 21(12): 993-999.
[7] 繆祥華，何大可. Needham-Schroeder私鑰協議的改進[A].計算機工程，2006.
MIAO Xiang-hua, HE Da-ke. The Improvement of Needham-Schroeder private-key Protocol[A].Computer engineering，2006.
[8] 王倩.BAN類邏輯研究[D].山東大學碩士學位論文，2007.
WANG Qian.The Study of BAN-like Logic[D].The Master Paper of Shan dong University，2007.
作者簡介：
仇細平，女，湖南株洲人，1983年生，碩士研究生，主要研究方向為信息安全理論與技術.
繆祥華，男，貴州盤縣人，1972年生，副教授，博士，碩士生導師，主要研究方向為信息安全理論與技術.
楊曉婕，女，云南大理人，彝族，1986年生，碩士研究生，主要研究方向為信息安全理論與技術.
09092
|
