基于Ｐｒｏｌｏｇ的安全協議在線自動化分析

摘 要：基于串空間理論和約束消減方法，提出安全協議可達性分析模型；采用Prolog實現模型自動推理，利用XSB的Java接口實現基于Web的自動分析工具。

關鍵詞：形式化；串空間；參數串；約束消減；Prolog

中圖分類號：TP309 文獻標志碼：A 文章編號：1001-3695(2008)08-2447-03

Prolog-based on-line automatic analysisfor security protocols

CHEN Tie-ming1，2，ZHANG Jie2，CAI Jia-mei2

(1.College of Software Engineering， Zhejiang Univeristy of Technology， Hangzhou 310032， China；2.State Key Laboratory of Software Deve-lopment Environment， Beihang University， Beijing 100083， China)

Abstract:This paper introduced a security reachability analysis model based on the strand space theory and the constraint elimination method. Then proposed a Prolog-based automatic reasoning scheme. At last，described a Web-based on-line automatic analysis implementation utilizing the Java interface of XSB (a prolog interpreter).

Key words:formal method; strand space; parametric strand; constraint elimination; Prolog

自BAN邏輯^[1]問世以來，安全協議形式化分析技術迅速發展，主要包括邏輯推理分析、狀態機模型、代數系統檢測等方法^[2]。其中，串空間模型^[3]是一種結合定理證明和協議跡的新方法。

協議的安全性可通過可達性^[4]問題來分析，即分析協議能否由初始狀態到達某個不安全的狀態。本文利用協議各方的公共信息初始化串空間，構建協議約束集模型^[5]，并通過Prolog實現約束消減過程的自動推理。安全協議的自動化分析工具是當前的一個研究熱點^[6]，本文利用XSB和YAJXB實現在線形式化分析系統原型。

1 串空間的可達性

1.1 消息項

記協議所有參與者間可能交換的消息集合為消息項集A。消息項可分為明文消息項（如參與者標志、隨機數等）和密鑰消息項（包括對稱密鑰、非對稱密鑰等）。消息項集A可劃分為明文消息項集T和密鑰消息項集K。

下面先給出本文將用到的符號項：

ε為攻擊者；

[t1，t2]為消息對；

Pk（P）為參與者P的公鑰（假設攻擊者無法獲得P的私鑰，攻擊者ε只能解密由Pk(ε)加密的信息）；

h(t)為信息項t的哈希值；

[t]k為對稱密鑰k加密消息項t；

[t]k為公鑰k加密消息項t；

Sigk(t)為私鑰k對消息項t簽名。

1.2 串空間

協議執行過程中參與者行為主要包括發送消息和接收消息，因此定義有符號消息項為二元組〈S，a〉。其中：a∈A，S= +表示發送消息，S =- 表示接收消息。〈S，a〉 通常簡寫為+a 或-a 。

串是一個參與者可能參與的事件序列。對于合法參與者，每個串是一系列接收和發送的消息，代表該參與者在一次特定協議執行中的行為以及所有消息項的值。攻擊者串是攻擊者可能發送和接收的消息序列。

串空間是包含各種合法主體串和攻擊者串的集合及一個軌跡映射：

tr:→(±A）

a）節點n=〈s，i〉。其中:S∈，1≤i≤lengthen(s)。 n∈s表示n屬于串s。每個節點屬于惟一的串，節點集用N表示。

b）若n=〈s，i〉∈N，則index(n)=i，term(n)=(tr(s))i，strand(n)=s。

c）若n1，n2∈N，則n1→n2， 即term(n1)=+a 且term(n2)=-a ，表示n1發送消息給n2 ，表達了串之間的因果關系。

d）若n1，n2∈N ，則n1→n2， 即term(n1)=+a 且term(n2)=-a ，表示n1和n2出現在同一個串中，且滿足index(n1)=index(n2)-1 ，表示n1是n2的直接因果前驅。

e）無符號項t出現在n∈N，當且僅當tterm(n)。

f）令I為無符號項集合，節點n∈N是I的進入點，當且僅當term(n)=+t 。其中:t∈I，且對所有的n′+n，term(n′)I。

g）無符號項t產生于n∈N ，當且僅當term(n) 的符號為正，tterm(n) ，以及對任意n的前驅節點m，有tterm(m)。

1.3 參數串與可達性

這里的參數串即上文提到的串，是參與者的事件序列，通常是發送和接收消息項，不同的是其包含一些變量。變量的不同取值可區別不同的串，如在NSL^[7]協議中，協議發起者的參數串表示如下：

 init(A，B，NA，NB)=+[A，NA]→pk(B)-[NA，NB，B]→pk(A)+[NB]→pk(B)

接收者參數串Re sp(A，B，NA，NB)的表示方式一致，不同在于+和-互換。

[x]→pk(A)表示用參與者A（發起者）的公鑰對信息x加密。+和-表示發送和接收信息，兩者組合在一起就是一個節點，例如+[NB]→pk(B)。這里消息項變量通常由大寫字母表示，如NB。

后文將用約束消減方法分析參數串集，參數串中某些參數可被常量替換。本文將參數串集叫做半叢^[8]。每個串中節點的序列隱含了各參與者之間狀態的轉變，例如：

{init(A，B，NA，NB)，Re sp(A'，B'，N'A，N'B)}即是一個半叢 。半叢中的每個串無須是完全的，它可能是某個參與者參數串的子串。

如果一個半叢是完全的，說明該叢所表示的狀態可由空的初始狀態達到，即協議狀態可達。半叢的完備與否可用來描述攻擊。如果攻擊者能夠通過適當的初始化，通過某些算法到達某種不安全狀態（通常是協議中的保密信息泄漏），則說明協議不安全。可通過這種可達性判斷協議的安全性。

2 約束消減方法

2.1 約束集理論

約束集用m：T表示。其中：m是一個信息項；T是信息項集，T代表攻擊者知道的信息集。攻擊者可通過T中的信息合成m。

帶“＋”號的節點可加入到最終的消息項集T中，而帶“－”號的節點可構建一個新的約束集m：T。

初始消息項集T0包含了初始信息，即假設攻擊者可獲得的初始信息，如A、B的身份ID（a，b），攻擊者ID及公鑰（ε，pk(ε)）等。因此T0可設置為{a，b，pk(a)，pk(b)，ε，pk(ε)}等。對于NSL協議，約束集可表示如下：

[A，B]：T0={a，b，ε，pk(ε)}

[a，NA]→pk(b)：T1=T0∪{[A，na]→pk(B)}

[na，NB，B]→pk(A)：T2=T1∪{[NA，nb，b]→pk(a)}

nb：T3=T2∪{[NB]→pk(B)}

2.2 約束消減過程

基于消減規則，每個約束集會在消減過程中被部分替換或分解，由其他常量取代，或整體替換，或分解為更多的子約束集。如果一個約束集的左邊是一個變量，那么稱該約束集是一個簡單約束集，或不可消減約束集。

一個約束集可能有不止一種消減方法，因此可采取樹狀結構（消減樹）來分析。在消減過程中可在初始約束集中創建一個根節點C0，C0是一個簡單約束集，也可能是一個協議的攻擊方法。

一棵消減樹是由約束集作為節點，消減規則作為邊來構建的。樹的根節點是初始約束集C，包含C0，具體消減過程P如下：

a）初始化：

C：=初始約束集；

σ：=；

b）C=m：T是約束集中的一個約束，并且m不是變量。如果C找不到，則可以滿足，否則對C使用消減規則，枚舉所有可能的約束。

c）對C使用約束消減規則r，若匹配，則令〈C′；σ′〉：=r(C，σ)，建立新節點C′，在遞歸棧中添加該節點。

d）重復步驟b）c）。

C;σ表示消減過程中的狀態。C是當前的約束集，σ是對約束集中變量的部分替換。

2.3 消減規則及實例分析

針對安全協議的密碼學假設，直接給出如下消減規則：

a）（C<，m：T，C>;σ）/（τC<，τC>;τ∪σ）（un）

where τ=mgu(m，t)，t ∈T;

b）（C<，[m1，m2]：T，C>;σ）/（C<，m1：T，m2:T，C>;σ）（pair）

c）（C<，h(m)：T，C>;σ）/（C<，m：T，C>;σ） (hash)

d）（C<，[m]→k：T，C>;σ）/（C<，k：T，m：T，C>;σ） (penc)

e）（C<，[m]k：T，C>;σ）/（C<，k：T，m：T，C>;σ）(senc)

f）（C<，sigpk(ε)(m)：T，C>;σ）/（C<，m：T，C>;σ） (sig)

g）（C<，m：[t1，t2]∪T，C>;σ）/（C<，m：t1∪t2∪T，C>;σ） (split)

h）（C<，m：[t]→pk(ε)∪T，C>;σ）/（C<，m：t∪T，C>;σ） (pdec)

i）（C<，m：[t]→k∪T，C>;σ）/（τC<，τm：τ[t]→k ∪τT，τC>;στ∪σ）(ksub)

where τ=mgu(k，pk(ε)，k≠pk(ε)

下面通過實例，說明如何運用消減規則分析NSL協議的安全性。

首先給出NSL協議的描述：

A→B：{NA，A}→pk(B)

B→A：{B，NA，NB}→pk(A)

A→B：{NB}→pk(B)

本文考慮接收者b和某個發起者A之間交互的參數串（小寫代表常量，大寫代表變量）。協議的最后一步已被省略，在實際分析的半串中包含更多的串。筆者在串的最后加上秘密信息接收串-nb，以測試nb在該過程中是否被泄露。

-[a，NA]→pk(b) to b

+[NA，nb，b]→pk(a)from b to a

-[B，NB]→pk(A)to any A from any B

+[NB，na，A]→pk(B)from A to B

-nbnb暴露

交互的約束集如下：

a） [a，NA]→pk(b)：T0={a，b，ε，pk(a)，pk(b)}

b） [B，NB]→pk(A)：T1=T0∪{[NA，[nb，b]]→pk(a)}

c） nb：T1∪{[NB，[na，A]]→pk(B)}

對a）使用penc規則得到：

(a) pk(b)：T0

(b) [a，NA]：T0

對（a）使用un規則，對（b）使用pair規則得

(a1) a：T0

(b1) NA：T0

對（a1）使用un規則，對（b）使用替換：

B→NA，NＢ→[nb，b]，A→a，即可消去（b）；

對（c）使用ksub規則得到

 NA→ε

說明nb將被暴露，確認協議有安全隱患。

3 Prolog自動推理

Prolog已在自然語言理解、機器定理證明、專家系統等方面得到廣泛的應用，本文將采用Prolog設計實現安全協議的自動推理與分析。串空間描述了協議各方可能參與的事件序列，即發送和接收某種消息的序列。協議中各方的事件序列都可通過Prolog語法準確描述，如在NSPK協議中，A方在協議中的事件序列表示如下：

init(A，B，NA，NB)=+[A，NA]→pk(B)-[NA，NB，B]→pk(A)+[NB]→pk(B)

用Prolog的描述如下：

strand(roleA，A，B，Na，Nb，[recv([A，B])， send([A，Na]*pk(B))，recv([Na，Nb]*pk(A))，send(Nb*pk(B))

]).

協議分析時的消減規則可通過Prolog實現。由于Prolog提供自動遞歸回溯功能，無須考慮程序的運行流程，只需確定邏輯關系。本文將采用XSB系統，XSB是一個用于商業研究的邏輯語言推理系統，支持標準的Prolog語法。

使用XSB可實現消減規則。例如：

reduct([A，B]，T，[[B，T]，[A，T]]) :- !.

表示 pair規則，分解[A，B]->[B，T]U[A，T]；

reduct(M/pk(e)，T，[[M，T]]) :- !.

表示sig規則，因為是e的公鑰簽名，可將M加入C中；

reduct(M，T，[]) :-member(A，T)，hunify(M，A).

表示 un規則，調用hunify謂詞，自動將M加入C中。

其他規則可類似實現，不再贅述。

4 在線自動化分析

鑒于Prolog語法的復雜性，為用戶提供直觀的協議分析工具十分必要。下面給出基于Web的在線自動分析系統實現。

XSB解釋器無服務器及UI方面的功能，但提供了一套Java接口，可采用YAJXB連接Java和XSB。YAJXB基于JNI（Java本地接口）實現，包含調用XSB的API。圖1描述了在線分析系統的設計框架。

服務程序采用Java/Jsp/Servlet/Javabean/Ajax技術。當客戶端發送協議分析請求時，Servlet通過JavaBean轉換請求格式，生成XSB可識別的協議體；通過YAJXB連接XSB系統，啟動XSB，載入協議體執行協議分析；最終截獲XSB系統輸出結果，通過Servlet將結果返回給Web客戶端。

在線分析系統的Web客戶端提供協議輸入框（按固定格式輸入待分析協議），加密消息采用大括號“{}”表示，Ka代表pk(A)，kb代表pk(B)。例如輸入NSPK協議如下：

{A，Na}kb

{Na，Nb}ka

{Nb}kb輸入待分析的保密消息，如nb。輸入完成后，點擊分析按鈕即可執行分析。由于采用Ajax技術，分析結果可快速顯示。若輸出結果中存在trace，說明存在安全隱患，該trace即代表一條攻擊路徑。NSL協議實例分析的結果顯示如圖2所示。

5 結束語

基于串空間的形式化分析方法是近年來分析安全協議的新方法，較傳統BAN類邏輯更為方便、高效，且易擴展。針對約束消減方法，通過增加約束消減規則，可不斷增強模型的協議分析能力。今后的工作將進一步研究約束消減策略及其過程實現，完善在線形式化系統提供的自動分析服務。

參考文獻：

[1]BURROWS M，ABADI M，NEEDHAM R. A logic of authentication[C]//Proc of Royal Society of London.1989:233-271.

[2] 卿斯漢.安全協議20年研究進展[J].軟件學報，2003，14(10):2036-2044.

[3] FBREGA F J T，HERZOG J C，GUTTMAN J D.Strand spaces:proving security protocols correct[J].Journal of Computer Security， 1999，7(2，3):191-230.

[4]MILLEN J， SHMATIKOV V. Constraint solving for bounded-process cryptographic protocol analysis[C]// Proc of the 8th ACM Confe-rence on Computer and Communications Security.Philadelphia: ACM Press， 2001:166-175.

[5]AMADIO R M，LUGIEZ D，VANACKERE V.On the symbolic reduction of processes with cryptographic functions[J]. Theory of Computer Science，2003，290(1): 695-740.

[6]陳鐵明，蔡家楣.安全協議的可視化分析和設計研究[J]. Journal of Communication and Computer，2005，2(12):27-31.

[7]ROBERTO M，AMADIO D L.On the reachability problem in cryptographic protocols[C]//Proc of the 11th International Conference.[S.l.]:Springer-Verlag，2000.

[8]LOWE G. Breaking and fixing the Needham-Schroeder public-key protocol using FDR[C]//Proc of the 2nd International Workshop.[S.l.]:Springer-Verlag，1996.

[9]SONG D X. A new efficient automatic checker for security protocol analysis[C]//Proc of IEEE Computer Security Foundations Workshop.[S.l.]:IEEE Computer Society，1999.

注：本文中所涉及到的圖表、注解、公式等內容請以PDF格式閱讀原文