一種安全協議自動化分析方法

摘 要:提出了一種基于串空間的安全協議自動化分析模型，該模型運用一系列算法實現協議的自動化分析，克服了冗長的理論推導，使協議的分析更加簡潔和直觀。模型的主要功能已在MyEclipse環境下用Java編程實現，并首次運用實現后的自動化分析模型對改進前后的Helsinki協議進行分析驗證，證明了該自動化分析方法的簡潔性和有效性。

關鍵詞:安全協議; 串空間; 自動化分析模型; 算法

中圖分類號:TP309文獻標志碼:A

文章編號:1001-3695(2010)06-2301-03

doi:10.3969/j.issn.10013695.2010.06.088

Kind of automated analysis method of security protocol

WU Xiaoying，ZHOU Qinglei

(College of Information Engineering， Zhengzhou University， Zhengzhou 450001， China)

Abstract:This paper presented an automated analysis model based on strand space of security protocol. The model achieved automatic analysis by using a series of algorithms and overcame the disadvantage of manual analysis of security protocol， so it made security protocol analysis more simple and intuitive.Themodel implemented its function by coding in MyEclipse environment with Java. The proposed approach compares and analyzes Helsinki protocol for the first time， and the results show that the method is simple and efficient.

Key words:security protocol; strand space; automatic analysis method; algorithm

安全協議是以密碼學為基礎的協議，它在網絡和分布式系統中提供各種各樣的安全服務，有著廣泛的應用，在信息系統安全中占據重要的位置。自動化[1，2]分析方法是協議形式化分析領域中一個重要的研究方向，目前安全協議的自動化分析方法尚處于起步階段。本文主要介紹一種基于串空間的安全協議自動驗證模型，并實現了該模型的基本功能，從而有效地對協議進行自動化分析。

1 協議分析方法基礎

串空間[3]模型是基于證明構造方法的典型代表，用于證明安全協議的正確性，它把安全協議的形式化分析推到了一個新的高度。

1.1 串空間主要概念

1)符號項

符號項是一個二元組〈σ，a〉。其中a∈A且σ={+，-}，記符號項為+t或-t。(±A)*是符號項的有限序列集合， 記(±A)*中的元素為〈〈σ1，a1〉 ，… ，〈σn，an〉〉。

2)攻擊者[4]跡

攻擊者串是串空間模型的一個組成部分，攻擊者的能力可由兩部分組成，即攻擊者初始時已知的密鑰集合可使攻擊者從所截獲的消息生成新消息的攻擊者strands集合。具體定義如下:

F. Flushing:〈-g〉;

T. Tee :〈-g，-g，+g〉;

C. Concatenation :〈-g ，-h ，+gh〉 ;

S. Separation into components :〈-gh ，+g，+h〉;

K. Key :〈+K〉 其中K∈KP;

E. Encryption :〈 -K ，-h ，+{h }K〉 ;

D. Decryption解密 :〈 -K-1，-{h }K，+h〉。

1.2 串空間的構造

串空間的構造如下:

a)節點是二元組〈s，i〉。其中s∈且i為滿足1≤i≤length(tr(s))的整數。節點集合記為N，稱節點〈s，i〉屬于串s。顯然，每一個節點屬于惟一的一個串。

b)若n=〈s，i〉∈N，則index(n)=i，且strand(n)=s。定義term(n)為(tr(s))i，即串s的跡中的第i個符號項。定義uns-term(n)=((tr(s))i)2，即串s的跡中的第i個符號項的無符號部分。

c)存在一個邊n1→n2，當且僅當存在某一個a∈A，使得term(n1)=+a且term(n2)=-a。因此，這類邊表示節點n1發送消息a，節點n2接收消息a，記錄了串間的一種因果連接。

d)若n1=〈s，i〉∈N，且n2=〈s，i+1〉∈N，則存在邊n1n2。這類邊表示n1是n2在串s上的直接因果前驅。用n′n表示n′是n在同一個串s上的因果前驅(不一定是直接因果前驅)。

2 模型設計

2.1 模型架構

模型設計如圖1所示，該模型應用初始化協議算法、串序列生成算法、狀態路徑生成算法、狀態路徑分析算法設計，適合于分析兩方通信的協議。首先，獲取需要分析的協議，應用初始化協議算法定義發起者和響應者的角色，生成發起者串和響應者串;其次，應用串序列生成算法，根據攻擊者跡生成串序列，再根據狀態路徑生成算法，結合圖論知識，生成狀態路徑;最后，應用狀態路徑分析算法分析狀態路徑，得出分析結果，驗證協議的安全性。

2.2 算法描述

2.2.1 初始化協議算法

協議兩方通信描述如下:

public class Protocol{

Node SNode;

Node RNode;

String Message;

}

其中:SNode表示每次通信的發起者，RNode表示每次通信的響應者，SNode為RNode的前驅節點，Message為通信內容。輸入協議存放在鏈表中。

算法描述如下:

public List〈List〉 init_Protocol(List〈Protocol〉 L){

List〈Node〉 NL; List〈Strand〉 SL; Node S;

Node R; Strand SS; Strand RS;

S=L.getItem(0).SNode;

R=L.getItem(0).RNode;

for(int i=0; i

if(L.getItem(i).SNode.equals(S)){

SS += “+”+ L.getItem(i).Message;

RS +=“-”+L.getItem(i).Message;

}else{

SS+=“-”+L.getItem(i).Message;

RS+=“+”+L.getItem(i).Message;

}

}

return(NL.add(S， R)， SL.add(SS， RS));

}

其中:L為存儲協議的鏈表，NL為存放發起者角色和響應者角色的鏈表，SL為存放發起者串和響應者串的鏈表，S為發起者角色，R為響應者角色，SS為發起者串，RS為響應者串。算法中，定義發起者為兩方第一次通信發送信息一方，響應者為兩方第一次通信接收信息一方，發送信息采用“+”，接收信息采用“-”。

2.2.2 串序列生成算法

本文中串定義如下:

public class Trace{

Node Role;

String Goal;

String Strand;

}

其中:Role表示角色，Goal表示目標，Strand表示串。

算法描述如下:

public List〈Trace〉 establish_TraceSet(List〈Protocol〉 L，Node S， Node R， Strand SS， Strand RS){

List〈Trace〉 TS; Protocol P; Node N;

int length = L.getItemCount();

N=L.getItem(length - 1).RNode;

for(int i = length-1; i>=0; i--){

P=L.getItem(i);

TS.add(establishTrace(N， S， R， SS， RS));

if(i ==0){

N=1;

TS.add(establishTrace(N， S， R， SS， RS));

}else{

N=P.SNode;

}}

return(TS);

}

其中:TS為存放生成串序列的鏈表，P為協議當前兩方通信，N為當前節點，establishTrace()函數的作用是根據當前角色N生成串并代入攻擊者跡生成攻擊者串。該算法根據對目標的綁定從兩方最后一次通信開始逆向生成串序列。首先根據最后一次通信的節點生成串，然后代入相應的攻擊者跡生成攻擊者串，同理依次尋找其前驅節點進行判斷，直到前驅節點目標為空，并判斷目標為空的情況。

2.2.3 狀態路徑生成算法

定義1 節點訪問完畢。當前節點及其鄰節點訪問完畢，即當前節點及其鄰節點的wasvisited屬性值為true。

狀態節點對象定義如下:

public class Vertex{

String label;

boolean visited;

}

其中:label表示節點，visited記錄節點是否被訪問。

狀態路徑生成算法描述如下:

public List〈Stack〉 establish_StateRoute(List〈Trace〉 TS){

int num=0; List〈Stack〉 RS; Stack〈Vertex〉 R;

Graph G=establish_StateGraph(TS); //根據串序列生成狀態圖

Stack〈Vertex〉 VS=get_StrandSet(G);

List establish_Route(){

if (VS[0].hasNext()){

R.push(VS[0]);

}

while(!R.isEmpty()){

Vertex v = R.peek();

if(v.hasNext()){

R.push(v.next());

if(!(R.peek()).hasNext()){

v.visited = true;

RS.add(R);

num++;

R.pop();

}

}else{

v.visited = true;

R.pop();

}}}

return(RS);

}

其中:TS表示串序列的集合，RS表示存放狀態路徑集合的鏈表，VS為狀態樹中所有頂點集合， R表示存放當前狀態路徑的容器，establish_StateGraph()的作用是根據串序列生成狀態圖，狀態圖用鄰接矩陣表示，get_StrandSet()的作用是獲取狀態圖的所有狀態節點與節點之間的關系。該算法首先獲取串序列，根據串序列生成狀態圖;然后，運用圖論知識，結合深度優先遍歷的方法，從初始節點開始尋找，找到的狀態路徑存放在RS中。

2.2.4 狀態路徑分析算法

定義2 可達性。狀態路徑最后節點目標為空。

定義3 合法性。滿足可達性的狀態路徑中同一角色用相同隨機數和同一個角色進行協議。

定義4 安全性。滿足合法性的狀態路徑中不包含攻擊者串。

算法描述如下:

public void routeAnalysis(List〈Stack〉 RS){

int i=0;

while(RS.getItemCount() != 0){

StateRoute R = RS.getItem(i);

RS.remove(i); i++;

if(R滿足可達性){

if(R滿足合法性){

if(R滿足安全性){

R為安全路徑;

}else{

R為不安全路徑;

該協議不安全;

break;

}

}else{

R不滿足合法性;

continue;

}

}else{

R為不可達路徑;

continue;

}

if(RS.getItemCount() == 0){

該協議為安全協議;

}}}

其中:RS為存放狀態路徑的鏈表，R表示當前狀態路徑。算法首先獲取需要分析的狀態路徑集合，依次按照上面的算法判斷所有的狀態路徑，從而對協議的安全性進行判斷。

3 模型實現及應用

3.1 模型實現

用Java[5]語言在MyEclipse環境下編程實現自動化分析模型。其中狀態路徑生成模塊采用圖論的知識實現，狀態圖用鄰接矩陣表示，用棧記錄訪問過的節點，并結合深度遍歷方法遍歷狀態圖生成狀態路徑。

協議通過界面化的形式輸入，并保存在數據庫表tb_protocol中，該表中包含ID、sponsor、responder、message四個字段，分別代表協議中一次兩方通信ID、發起者、響應者、通信內容;生成的串序列保存在數據庫表tb_trace中，該表包含ID、role、goal、strand四個字段，分別表示串ID、角色、目標、串;最終生成的狀態路徑及其分析結果存放在數據庫表tb_stateroute中，該表包含字段有ID、route、ifarrival、iflegal、ifsafe，分別表示狀態路徑ID、狀態路徑、是否滿足可達性、是否滿足合法性、是否滿足安全性。

3.2 模型在具體協議中的應用

本節運用上節實現的自動化分析方法，對改進前后的Helsinki[6]協議進行驗證，說明該自動化分析方法的有效性。Helsinki協議描述如下:

a)A→B:{ A，Ki，Na｝kb

b)B→A:{ Kr，Na，Nb｝ka

c)A→B:Nb

用Navicat以界面化的形式獲取數據庫信息，其所對應的串序列和狀態路徑如圖2、3所示。

根據協議安全性的判斷方法，圖2、3的狀態路徑中存在不安全路徑，因此該協議是不安全的。驗證了這個協議存在的HorngHsu[6]攻擊。 MitchellYeun[6]對其進行了改進，改進后的Helsinki協議描述如下:

a)A→B:{ A，Ki，Na｝kb

b)B→A:{ B，Kr，Na，Nb｝ka

c)A→B:Nb

程序運行所得到的串序列和狀態路徑如圖4、5所示。

狀態路徑中均為安全路徑，因此用該自動化分析方法驗證了MitchellYeun改進后的Helsinki協議是安全的，說明該自動化分析方法的可行性。

4 結束語

本文根據串空間理論，提出了一種安全協議自動化分析模型，并通過Java編程實現了該模型的基本功能，最后運用此方法對Helsinki協議進行分析，發現了該協議的漏洞，并對改進后的Helsinki協議進行分析，從而驗證了MitchellYeun改進后的Helsinki協議的安全性，說明該模型分析協議的有效性。

與安全協議自動化分析模型Athena[7]相比，本文提出的模型的優點主要體現在，該模型是基于串的，逆向生成串序列，從而避免了Athena模型中存在的狀態爆炸的缺陷;該模型用變量描述協議，狀態路徑的生成是依次尋找當前節點的子節點，可以有效保證算法的終止。但是這種形式化的分析模型也有一定的缺點，它只能用來分析雙方通信的加密協議[8]，其分析范圍有一定的局限性。因此，擴大該方法的分析范圍，使這種協議的自動化分析方法更加完善是以后值得深入研究的主要方向。

參考文獻:

[1]周天凌，黃連生. Hlpsl2Cpp一個安全協議編譯器[J].計算機應用研究，2007，24(6):123-126.

[2]PERRIGA，SONG D. A first step toward the automatic generation of security protocols[C]//Proc of Network and Distributed System Security Symposium(NDSS). San Diego:ISOC，2000.

[3]THAYER F， HERZOG J C， GUTTMAN J D. Strand spaces: Why is a security protocol correct?[C]//Proc of IEEE Symposium on Security and Privacy.1998.

[4]LOWE G. Analysing protocols subject to guessing attacks[C]//Proc of Workshop on Issues in the Theory of Security. 2002.

[5]ECKEL B. Thinking in Java[M]. 4th ed.[S.l.]:Prentice Hall PTR ，2007.

[6]卿斯漢. 安全協議[M]. 北京:清華大學出版社，2005.

[7]SONG D X， PERRIG A， BEREZIN S. Athena: a novel approach to efficient automatic security protocol analysis[J]. Journal ofComputer Security， 2001， 9(12):47-74.

[8]MEADOWS C. Formal methods for cryptographic protocol analysis:emerging issues and trenda[J]. IEEE Journal on Selected Areas in Communication， 2003，21(1):44-54.