王建華, 張 嵐

1. 93114 部隊, 北京 100195

2. 信息工程大學(xué), 鄭州 450001

1 引言

形式化方法用于安全協(xié)議分析已有四十多年的發(fā)展歷史, Dolev-Yao 模型[1]開創(chuàng)了安全協(xié)議形式化方法的先河, 定義了協(xié)議并發(fā)運(yùn)行環(huán)境的形式化模型、密碼算法無關(guān)的驗證以及攻擊者行為等, 奠定了安全協(xié)議形式化方法研究的基礎(chǔ). 人們在安全協(xié)議的設(shè)計和分析上投入了大量的精力, 形成了為數(shù)眾多的研究方法和理論. 邏輯推理方法[2–5]雖然可以發(fā)現(xiàn)安全協(xié)議設(shè)計出錯的原因, 但是由于抽象性較高, 不能發(fā)現(xiàn)協(xié)議存在的攻擊且難以反映協(xié)議運(yùn)行整個過程, 有著自身的局限性. 模型檢測技術(shù)[6–8]是驗證有限狀態(tài)系統(tǒng)的自動化分析技術(shù), 可以發(fā)現(xiàn)協(xié)議存在的攻擊, 但最大的不足就是無法避免狀態(tài)空間爆炸問題. 定理證明技術(shù)是用邏輯符號對安全協(xié)議進(jìn)行模型化, 再用定理證明技術(shù)證明安全協(xié)議的正確性, 具有代表性有Paulson 的歸納法[9]和串空間模型[10].

密碼協(xié)議自設(shè)計之初就遭受各種各樣形式化分析方法[2–6]的檢測, 由于協(xié)議運(yùn)行時的高并發(fā)性、設(shè)計者能力程度的差異性、應(yīng)用環(huán)境的復(fù)雜性,導(dǎo)致了諸如消息重放、中間人、并行會話等眾多協(xié)議缺陷攻擊[7]被相繼發(fā)現(xiàn). 類型缺陷攻擊[8]由于消息格式的相似性而導(dǎo)致部分消息類型重置, 是最不易檢測到的一類攻擊. 為此各類形式化方法陸續(xù)用于檢測類型缺陷攻擊, 基于定理證明器的Paulson 歸納法[9]分析了ffgg 協(xié)議[11]以及Yahalom-Paulson 協(xié)議[12], 分析結(jié)果顯示是安全的, 實則暗含著類型缺陷攻擊[13]. 串空間理論構(gòu)造攻擊方法[14]通過密碼協(xié)議中各個狀態(tài)的偏序關(guān)系構(gòu)造非空集合, 遍歷Dolev-Yao 模型[1]約定的攻擊者能力規(guī)則集, 分析檢測該非空集合的最小元節(jié)點是否在攻擊者串上, 由于不能識別未知的消息類型屬性, 未能發(fā)現(xiàn)文獻(xiàn)[11,15] 出現(xiàn)的類型缺陷攻擊; 文獻(xiàn)[16] 改進(jìn)了串空間理論構(gòu)造攻擊方法, 通過檢測含有測試元素的非空集合極小元節(jié)點后續(xù)的發(fā)送和接收情況, 實例化攻擊者串, 可用于形式化驗證;認(rèn)證測試?yán)碚揫17]是基于串空間模型提出來的一種用于證明安全協(xié)議認(rèn)證屬性的方法, 雖然簡化了協(xié)議認(rèn)證屬性的證明過程, 但是對于未知的消息類型屬性仍舊不能識別; 文獻(xiàn)[18] 改進(jìn)了認(rèn)證測試方法, 定義了消息類型屬性, 提出若測試元素中隨機(jī)數(shù)類型之前的類型與變換后的組成元素類型一致, 則存在類型缺陷攻擊, 該論斷僅是一些協(xié)議類型缺陷特例, 對于像ffgg* 協(xié)議[16]中的類型缺陷仍然發(fā)現(xiàn)不了; 文獻(xiàn)[19] 通過引入一個多分支標(biāo)簽樹, 建立一個強(qiáng)攻擊者模型, 并做了分類用以擴(kuò)展串空間模型, 用于檢測密碼協(xié)議中的類型缺陷攻擊. 文獻(xiàn)[20,21] 總結(jié)了類型缺陷攻擊形式, 給出了設(shè)計認(rèn)證協(xié)議時檢測類型缺陷攻擊的方法, 為后續(xù)理論研究類型缺陷攻擊提供了很好的借鑒. SAT 模型檢測器[22]增加了消息類型匹配算法,用于檢測類型缺陷攻擊. 文獻(xiàn)[23—25] 在協(xié)議格式中引入類型標(biāo)簽并強(qiáng)制檢查, 雖然能檢測類型錯誤攻擊,但是會大大增加協(xié)議執(zhí)行的代價. 對于采用CAESAR[26]中帶有關(guān)聯(lián)數(shù)據(jù)認(rèn)證加密模式的密碼協(xié)議, 認(rèn)證碼是對報頭和報文密文所做的密碼處理, 任何數(shù)據(jù)的改變都會影響認(rèn)證碼的完整性, 但是在選擇明文攻擊條件下, 攻擊者可以對包括認(rèn)證碼在內(nèi)的指定的協(xié)議數(shù)據(jù)進(jìn)行修改替換, 進(jìn)而達(dá)到類型缺陷攻擊的意圖,因此, 只有在設(shè)計協(xié)議時充分考慮到類型缺陷, 才能從根本上阻止類型缺陷攻擊.

類型缺陷攻擊自被發(fā)現(xiàn)以來, 關(guān)于該攻擊的類型相似性機(jī)理一直沒有得到詳細(xì)研究, 僅僅是停留在表面, 沒有從產(chǎn)生該攻擊的本質(zhì)層面考慮, 而且公開相關(guān)文獻(xiàn)也沒有關(guān)于消息類型結(jié)構(gòu)的成熟研究. 本文從類型缺陷攻擊的消息類型相似性機(jī)理入手, 著重研究密碼協(xié)議原子類加密數(shù)據(jù)消息類型結(jié)構(gòu), 指出若密碼協(xié)議消息序列中存在一組消息類型同態(tài)性、相似性、等價性等代數(shù)結(jié)構(gòu)的原子類消息加密數(shù)據(jù), 則該協(xié)議存在類型缺陷, 并給出了設(shè)計密碼協(xié)議時應(yīng)該遵循的準(zhǔn)則; 克服了其它形式化分析方法不能識別消息類型的相似性等結(jié)構(gòu)而導(dǎo)致類型缺陷的不足, 發(fā)現(xiàn)了Wide-Mouth Frog 協(xié)議[11]的新攻擊.

2 基本概念、性質(zhì)與定理

為了更清晰地闡述檢測類型缺陷的形式化構(gòu)造攻擊方法, 便于理解后續(xù)章節(jié)的符號、名詞以及內(nèi)容,給出了與該形式化構(gòu)造攻擊方法有關(guān)的基本概念、性質(zhì)、引理與定理.

定義1(原子消息集) 原子消息集表示為M0={Nounce,Time,Serial,Key,ID,··· ,?},其中Nounce表示隨機(jī)數(shù), Time 表示時間戳, Serial 表示序列號, ID 表示標(biāo)識符, Key 表示密鑰(公鑰、私鑰、對稱密鑰、簽名密鑰等),?表示空消息.

原子消息之間的運(yùn)算法則由串接和密碼運(yùn)算f(包括加密、解密、簽名等) 組成, 使用“x||y” 表示原子消息x與y的串接, 使用“{x1,x2,··· ,xn}k(k ∈Key)” 表示原子消息k對消息序列xi(i=1,2,··· ,n)進(jìn)行密碼運(yùn)算. 經(jīng)過串接或密碼運(yùn)算組合合成密碼協(xié)議中的消息項.

定義2(原子類消息加密數(shù)據(jù)) 密碼協(xié)商協(xié)議中, 對于消息加密數(shù)據(jù)t={h}k, 若消息數(shù)據(jù)序列h中,無形如{···}k的原子消息復(fù)合數(shù)據(jù), 則稱加密數(shù)據(jù)t為原子類消息加密數(shù)據(jù).

定義3(消息類型集) 消息類型集表示為T={R,K,I,Ci(i=1,2,···),?,···}, 其中R表示隨機(jī)因子類,K表示密鑰類, 且K/∈KP,KP表示攻擊者密鑰,I表示主體標(biāo)識類,Ci(i=1,2,···) 表示第i重密文類,?表示空類型,D表示未知原子數(shù)據(jù)類(密鑰、標(biāo)識、隨機(jī)因子、密文類、空類型、協(xié)商數(shù)據(jù)等).

消息類型之間的運(yùn)算法則Tf與原子消息之間的運(yùn)算法則f相似, 也由串接和密碼運(yùn)算組成, 使用“X||Y” 表示原子消息類型X與Y的串接, 使用“{X1,X2,··· ,Xn}K(K ∈Key)” 表示原子消息密鑰類型K對消息類型序列Xi(i=1,2,··· ,n) 進(jìn)行密碼運(yùn)算. 對于x ∈M,

因此, 根據(jù)定義4 可知, 對于?x,y ∈M,Tf(x)*Tf(y)=Tf(x°y), 即類型映射運(yùn)算滿足同態(tài)關(guān)系.

定義5(消息-類型同態(tài)映射) 密碼協(xié)議中, 若存在類型映射Tf:M1→T1,M1?M,T1?T, 對于?x,y ∈M1, 滿足Tf(x°y)=Tf(x)*Tf(y), 則稱Tf為從(M1,°) 到(T1,*) 的一種消息-類型同態(tài)映射.

定義6(類型缺陷攻擊) 通常在認(rèn)證協(xié)議執(zhí)行過程中, 消息的類型不是顯式給出的, 這就意味著無法檢查消息是否被加以正確的類型, 由此導(dǎo)致的協(xié)議攻擊稱為類型缺陷攻擊.

定義7(消息類型同態(tài)結(jié)構(gòu)) 密碼協(xié)議中的原子類數(shù)據(jù)Aj={hj|dj,1,··· ,dj,n-1,dj,n}Keyj,j=1,2, 若至少滿足以下情形之一:

(1) 若d1,1=d2,1,Tf(d1,2||···||d1,n-1||d1,n)=Tf(d1,2)*···*Tf(d1,n-1)*Tf(d1,n)(首項相同);

(2) 若d1,n=d2,n,Tf(d1,1||···||d1,n-1)=Tf(d1,1)*···*Tf(d1,n-1)(尾項相同);

(3) 若d1,1=d2,1且d1,n=d2,n,Tf(d2,2||···||d2,n-1) =Tf(d2,2)*···*Tf(d2,n-1) =P(?P ∈T)(首尾相同);

(4) 若d1,1/=d2,1,···,d1,i-1/=d2,i-1,d1,i=d2,i,d1,i+1/=d2,i+1,···,d1,n/=d2,n(中間某一項相同),

則可稱Aj(j=1,2) 為具有消息類型同態(tài)結(jié)構(gòu)的一組加密數(shù)據(jù).

定義 8(消息類型相似性結(jié)構(gòu)) 密碼協(xié)議中的原子類數(shù)據(jù)Aj={hj|dj,1,··· ,dj,n-1,dj,n}Keyj,(j=1,2), 若該原子類消息的對應(yīng)項類型相同, 數(shù)據(jù)至少有一對不同, 即若Tf(d1,1) =Tf(d2,1),···,Tf(d1,n) =Tf(d2,n), 且至少存在一個i ∈{1,2,··· ,n}, 使i ∈d1,i/=d2,i. 則可判斷Aj(j=1,2) 為具有消息類型相似性結(jié)構(gòu)的一組加密數(shù)據(jù).

定義 9(消息類型等價性結(jié)構(gòu)) 密碼協(xié)議中的原子類數(shù)據(jù)Aj={hj|dj,1,··· ,dj,n-1,dj,n}Keyj,(j=1,2), 若該原子類消息的數(shù)據(jù)項次序經(jīng)過排列組合后, 與另一個原子類加密數(shù)據(jù)相同, 即存在一個位置置換L, 使d1,L(1)=d2,i1,d1,L(2)=d2,i2,···,d1,L(n)=d2,in. 則可稱為具有消息類型等價性結(jié)構(gòu)的一組加密數(shù)據(jù).

定理1(類型缺陷攻擊存在性定理I) 若密碼認(rèn)證協(xié)議中存在一組消息類型同態(tài)結(jié)構(gòu)的原子類消息加密數(shù)據(jù), 則該協(xié)議中存在一類類型缺陷攻擊.

證明:若該協(xié)議存在一組消息類型同態(tài)結(jié)構(gòu)的原子類消息加密數(shù)據(jù), 由定義7 可知: 該加密數(shù)據(jù)可表示為:tj={hj|dj,1,··· ,dj,n-1dj,n}Keyj(j=1,2).

(1) 若d1,1=d2,1,Tf(d1,2||···||d1,n-1||d1,n)=Tf(d1,2)*···*Tf(d1,n-1)*Tf(d1,n)(首項相同),Tf(d2,2||···||d2,n)=Tf(d2,2)*···*Tf(d2,n)=P(?P ∈T), 則令Tf(d1,2||···||d1,n)=Tf(d1,2)*···*Tf(d1,n)=P, 且d1,2||···||d1,n=d2,2||···||d2,n.由定義6 可知, 可以重放消息t1代替t2, 構(gòu)造類型缺陷攻擊.

(2) 若d1,n=d2,n,Tf(d1,1||···||d1,n-1)=Tf(d1,1)*···*Tf(d1,n-1)(尾項相同),Tf(d2,1||···||d2,n-1) =Tf(d2,1)*···*Tf(d2,n-1) =P(?P ∈T), 令Tf(d1,1||···||d1,n-1) =Tf(d1,1)*···*Tf(d1,n-1)=P, 且d1,1||···||d1,n-1=d2,1||···||d2,n-1. 由定義6 可知, 可以重放消息t1代替t2, 構(gòu)造類型缺陷攻擊.

(3) 若d1,1=d2,1, 且d1,n=d2,n,Tf(d2,2||···||d2,n-1) =Tf(d2,2)*···*Tf(d2,n-1) =P(?P ∈T)(首尾相同) 令Tf(d1,2||···||d1,n-1) =Tf(d1,2)*···*Tf(d1,n-1) =P,d1,2||···||d1,n-1=d2,2||···||d2,n-1. 由定義6 可知, 可以重放消息t1代替t2, 構(gòu)造類型缺陷攻擊.

(4) 若d1,1/=d2,1,···,d1,i-1/=d2,i-1,d1,i=d2,i,d1,i+1/=d2,i+1,···,d1,n/=d2,n(中間某一項相同),Tf(d2,1||···||d2,i-1)=Tf(d2,1)*···*Tf(d2,i-1)=P1(P1∈T),Tf(d2,i+1||···||d2,n)=Tf(d2,i+1)*···*Tf(d2,n) =P2(P2∈T). 令:Tf(d1,1||···||d1,i-1) =Tf(d1,1)*···*Tf(d1,i-1) =P1,d1,1||···||d1,i-1=d2,1||···||d2,i-1,Tf(d1,i+1||···||d1,n) =Tf(d1,i+1)*···*Tf(d1,n) =P2,d1,i+1||···||d1,n=d2,i+1||···||d2,n. 由定義6 可知, 可以重放消息t1代替t2, 構(gòu)造類型缺陷攻擊.

定理2(類型缺陷攻擊存在性定理II) 若密碼協(xié)議中存在一組消息-類型相似性結(jié)構(gòu)的原子類消息加密數(shù)據(jù), 則該協(xié)議中存在一類類型缺陷攻擊.

證明:若該協(xié)議存在一組消息類型相似性結(jié)構(gòu)的原子類消息加密數(shù)據(jù), 由定義8 可知: 該加密數(shù)據(jù)可表示為:tj={hj|dj,1,··· ,dj,n-1dj,n}Keyj(j=1,2).

即若Tf(d1,1) =Tf(d2,1),··· ,Tf(d1,n) =Tf(d2,n), 且至少存在一個i ∈{1,2,··· ,n}, 使d1,i/=d2,i. 即h1與h2之間對應(yīng)原子消息具有相似性, 由于t1與t2的原子消息類型一致, 而且發(fā)送數(shù)據(jù)的消息格式一致, 通過反復(fù)重放該類加密數(shù)據(jù)消息, 構(gòu)造類型缺陷攻擊. 舉例說明如下:t1={h1|r1,i1,k}k,t2={h2|r2,i2,k}k. 其中A為發(fā)送方,B為接收方,S為可信第三方.

(1)A →S:{h1|ra,ib,k}kas

(2)S →B:{h2|rs,ia,k}kbs

(1)P(B)→S:{h2|rs,ia,k}kbs

(2)S →A:{h′21|rs1,ib,k}kas

(1)P(A)→S:{h′21|rs1,ib,k′}kas

(2)S →B:{h22|rs2,ia,k′}kbs

該實例通過消息類型的相似性構(gòu)造類型缺陷攻擊, 也可以因為消息類型的相似性借助于重放消息構(gòu)造類型缺陷攻擊, 從而使攻擊者與合法主體得到認(rèn)證或擁有相同密鑰.

定理3(類型缺陷攻擊存在性定理III) 若密碼協(xié)議中存在一組消息-類型等價性結(jié)構(gòu)的原子類消息加密數(shù)據(jù), 則該協(xié)議中存在一類類型缺陷攻擊.

證明:若該協(xié)議存在一組消息類型等價性結(jié)構(gòu)的原子類消息加密數(shù)據(jù), 由定義9 可知: 該加密數(shù)據(jù)可表示為:tj={hj|dj,1,··· ,dj,n-1dj,n}Keyj(j=1,2). 即存在一個位置置換L, 使d1,L(1)=d2,i1,d1,L(2)=d2,i2,···,d1,L(n)=d2,in. 由于這樣的原子類消息數(shù)據(jù)不變, 僅僅是數(shù)據(jù)位置發(fā)生了平移, 根據(jù)此特點, 可以構(gòu)造類型缺陷攻擊. 舉例說明如下: 其中A為發(fā)送方,B為接收方.

(1)A →B:{r1,r2,k12}k

(2)B →A:{r2,k12,r1}k

(1)P(A)→B:{r1,r2,k12}k

(2)B →P(A):{r2,k12,r1}k

(1)P(B)→A:{r2,k12,r1}k

(2)A →P(B):{k12,r1,r2}k

該實例通過消息類型的等價性構(gòu)造類型缺陷攻擊, 從而使攻擊者與合法主體得到認(rèn)證或擁有相同密鑰.

性質(zhì)1 在密碼認(rèn)證協(xié)議中, 對于原子類消息加密數(shù)據(jù)tj={hj}kj(j=1,2),kj/∈KP, 若h1的形式表示為h1:r1,i1,h2的形式表示為h2:r1,r2, 則h1與h2之間存在一個消息類型同態(tài)結(jié)構(gòu).

證明:對于h1:r1,i1,Tf1(r1) =R,Tf1(i1) =I; 對于h2:r1,r2,Tf2(r2) =Tf2(r1) =R. 令Tf1(i1)=Tf2(r2)=R, 又由于Tf1(r1)=Tf2(r1)=R, 根據(jù)定義7,h1與h2之間存在一個消息類型同態(tài)結(jié)構(gòu).

性質(zhì)2 在密碼認(rèn)證協(xié)議中, 對于原子類消息加密數(shù)據(jù)tj={hj}k(j=1,2),k/∈KP, 若h1的形式表示為h1:i,k,h2的形式表示為h2:i,r1,r2, 則h1與h2之間存在一個消息類型同態(tài)結(jié)構(gòu).

證明:對于h1:i,k,Tf1(i) =I,Tf1(k) =K; 對于h2:i,r1,r2,Tf2(r2) =Tf2(r1) =R. 令Tf2(r1||r2)=K, 可得Tf1(h1)=Tf2(h2)={I,K}. 又由于Tf1(i)=I=Tf2(i), 根據(jù)定義7,h1與h2之間存在一個消息-類型同態(tài)結(jié)構(gòu).

性質(zhì)3 在密碼認(rèn)證協(xié)議中, 對于原子類消息加密數(shù)據(jù)tj={hj}k(j=1,2),k/∈KP, 若h1的形式表示h1:r,d,i1,i2,h2的形式表示為h2:r,k, 則h1與h2之間存在一個消息類型同態(tài)結(jié)構(gòu).

證明:對于h1:r,d,i1,i2,Tf1(r) =R,Tf1(d) =D,Tf1(i1) =Tf1(i2) =I; 對于h2:r,k,Tf2(r) =R,Tf2(k) =K. 令Tf1(d||i1||i2) =K, 可得Tf1(h1) =Tf2(h2) ={R,K}, 又由于Tf1(r) =R=Tf2(r), 根據(jù)定義7,h1與h2之間存在一個消息-類型同態(tài)結(jié)構(gòu).

性質(zhì)4 在密碼認(rèn)證協(xié)議中, 對于原子類消息加密數(shù)據(jù)tj={hj}kj(j=1,2),kj/∈KP, 若h1的形式表示為h1:T1,i1,k12,h2的形式表示為h2:i2,T2,k12, 則h1與h2之間存在一個消息類型同態(tài)性結(jié)構(gòu).

證明:對于h1:T1,i1,k12,Tf1(T1) =R,Tf1(i1) =I,Tf1(k12) =K; 對于h2:i2,T2,k12,Tf2(T2) =R,Tf2(i2) =I,Tf2(k12) =K, 可知Tf1(h1) =Tf2(h2) ={R,I,K}, 且Tf1(k12) =Tf2(k12) =K, 由定義8 可知,h1與h2之間對應(yīng)原子消息具有同態(tài)性,h1與h2之間存在一個消息類型相似性結(jié)構(gòu).

性質(zhì)5 在密碼認(rèn)證協(xié)議中, 對于原子類消息加密數(shù)據(jù)tj={hj}kj(j=1,2),kj/∈KP, 若h1形式表示為h1:T1,i1,k12,h2形式表示為h2:T2,i2,k12, 則h1與h2之間存在一個消息類型相似性結(jié)構(gòu).

證明:對于h1:T1,i1,k12,Tf1(T1) =R,Tf1(i1) =I,Tf1(k12) =K; 對于h2:T2,i2,k12,Tf2(T2)=R,Tf2(i2)=I,Tf2(k12)=K, 可知Tf1(h1)=Tf2(h2)={R,I,K}, 且T1/=T2,i1/=i2, 由定義8 可知,h1與h2之間對應(yīng)原子消息具有相似性,h1與h2之間存在一個消息類型相似性結(jié)構(gòu).

性質(zhì)6 在密碼認(rèn)證協(xié)議中, 對于原子類消息加密數(shù)據(jù)tj={hj}kj(j=1,2),kj/∈KP, 若h1的形式表示為h1:r1,r2,k12,h2的形式表示為h2:r2,k12,r1, 則h1與h2之間存在一個消息類型等價性結(jié)構(gòu).

證明:對于h1:r1,r2,k12,Tf1(r1)=Tf1(r2)=R,Tf1(k12)=K; 對于h2:r2,k12,r1,Tf2(r2)=R,Tf2(k12) =K,Tf2(r1) =R, 可得Tf1(h1) =Tf2(h2) ={R,K}, 由定義9 可知,h1與h2之間的原子消息具有等價性性,h1與h2之間存在一個消息類型等價性結(jié)構(gòu).

性質(zhì)7 在密碼認(rèn)證協(xié)議中, 對于原子類消息加密數(shù)據(jù)tj={hj}kj(j=1,2),kj/∈KP, 若h1的形式表示為h1:r2,k12,r1,h2的形式表示為h2:k12,r1,r2, 則h1與h2之間存在一個消息類型等價性結(jié)構(gòu).

證明:對于h1:r2,k12,r1,Tf1(r2) =R,Tf1(k12) =K,Tf1(r1) =R; 對于h2:k12,r1,r2,Tf2(k12) =K,Tf2(r1) =R,Tf2(r2) =R, 可得Tf1(h1) =Tf2(h2) ={R,K}, 由定義9 可知,h1與h2之間的原子消息具有等價性性,h1與h2之間存在一個消息類型等價性結(jié)構(gòu).

性質(zhì)8 在密碼認(rèn)證協(xié)議中, 對于原子類消息加密數(shù)據(jù)tj={hj}kj(j=1,2),kj/∈KP, 如果h1形式表示為h1:k12,r1,r2,h2形式表示為h2:r1,r2,k12, 則h1與h2之間存在一個消息類型等價性結(jié)構(gòu).

證明:對于h1:k12,r1,r2,Tf1(k12) =K,Tf1(r1) =R,Tf1(r2) =R; 對于h2:r1,r2,k12,Tf2(r1) =R,Tf2(r2) =R,Tf2(k12) =K, 可得Tf1(h1) =Tf2(h2) ={R,K}, 由定義9 可知,h1與h2之間的原子消息具有等價性,h1與h2之間存在一個消息類型等價性結(jié)構(gòu).

引理1[27]若C是一個叢, 二元關(guān)系≤C是偏序的, 則C的任意非空節(jié)點子集都有≤C最小元.

引理2[27]若{h′}K′?{h}K且K/=K′, 則{h′}K′?h.

引理3[27]自由加密假設(shè): 若{m}k={m′}k′, 則可以推出m=m′,k=k′.

定理4若節(jié)點集合S={n ∈C:t ?uns-term(n)}有一個最小元節(jié)點m, 則它的符號為正.

證明:事實上, 如果m的符號是負(fù)的, 那么由叢的定義可知存在一個節(jié)點n1, 且n1→m, unsterm(n1) = uns-term(m). 在這種情形下,n1在m之前,t ?uns-term(n1), 所以n1∈S, 這與m是集合S的最小元相矛盾.

定理5(隨機(jī)因子新鮮性) 若隨機(jī)因子α在協(xié)議叢C中是新鮮的, 則存在一個節(jié)點n ∈C, 使得α唯一源發(fā)于節(jié)點n.

證明:由隨機(jī)因子的新鮮性可知, 該隨機(jī)因子不可重復(fù), 即在協(xié)議叢中不存在兩個不同的正節(jié)點n1,n2∈C, 使得term(n1)=term(n2)=+α. 即新鮮隨機(jī)因子在協(xié)議叢C中唯一源發(fā).

3 檢測類型缺陷的形式化構(gòu)造攻擊方法

密碼協(xié)議是在不可靠或者敵意的通信環(huán)境下, 保障一定安全特性的網(wǎng)絡(luò)協(xié)議. 在這種環(huán)境中, 敵手對于協(xié)議可以有各種各樣的攻擊手段, 包括竊聽、篡改、截斷協(xié)議的通信, 甚至加入任何可能的消息, 把協(xié)議的消息轉(zhuǎn)向到其它接收者等等. 因此, 這些因素決定了看似完美的協(xié)議, 卻存在著難以察覺的缺陷. 雖然密碼協(xié)議的設(shè)計過程就那么幾步, 然而經(jīng)過精心設(shè)計的協(xié)議往往存在一些微妙的漏洞, 這樣檢測協(xié)議的漏洞并加以改進(jìn)就顯得非常重要.

在串空間模型中, 攻擊者能力使用兩方面的因素來描述: 攻擊者所掌握的密鑰集合和根據(jù)所有已知消息構(gòu)造新消息的能力. 攻擊者所掌握的密鑰集合用KP表示. 集合KP包含了攻擊者初始知道的所有密鑰, 它包括所有的公開密鑰和攻擊者的私有密鑰, 以及根據(jù)協(xié)議規(guī)則所掌握的和其他主體會話的對稱密鑰,也可能會包括被一些粗心的主體丟失的密鑰. 攻擊者能力使用攻擊串來表示, 攻擊者串描述了攻擊者拆分、構(gòu)造、聯(lián)結(jié)和使用已知密鑰加解密消息的能力, 屬于攻擊者串的節(jié)點稱為攻擊者節(jié)點(用P表示), 其余稱為正規(guī)者節(jié)點, 攻擊者能力使用下面列出的攻擊者串[29]來描述.

(a)M.〈+t〉, 其中t ∈T,T為原子消息集合;

(b)F.〈-g〉, 其中g(shù) ∈A,A為消息空間;

(c)T.〈-g,+g,+g〉, 其中g(shù) ∈A;

(d)C.〈-g,-h,+gh〉, 其中g(shù),h ∈A;

(e)S.〈-gh,+g,+h〉, 其中g(shù),h ∈A;

(f)K.〈+k〉, 其中k ∈KP,KP為攻擊者的密鑰集;

(g)E.〈-k,-h,+{h}k〉, 其中h ∈A,k ∈KP;

(h)D.〈-k-1,-{h}k,+h〉, 其中k與k-1為互逆密鑰,k,k-1∈Kp,h ∈A.

由于攻擊者的能力由攻擊者的密鑰集和攻擊者串進(jìn)行定義, 所以這種能力是獨立于任何特定協(xié)議的.下述引理給出了攻擊者的能力范疇, 符號ST表示集合S與T的差.

引理4[27]若C是一個叢, 密鑰k ∈(KKP). 如果k不起源于一個正規(guī)節(jié)點, 那末對于任意節(jié)點n ∈C, 有k/?uns-term(n). 特別地, 對于任意攻擊者節(jié)點p ∈C, 有k/?uns-term(p).

3.1 類型形式化構(gòu)造攻擊方法

檢測類型缺陷的形式化構(gòu)造攻擊方法, 簡稱為類型形式化構(gòu)造攻擊方法, 由于其明顯的代數(shù)結(jié)構(gòu)特征,極易判別, 與其它形式化分析方法相比較, 更適合檢測認(rèn)證協(xié)議的類型缺陷. 如表1 所示. 類型形式化構(gòu)造攻擊方法檢測是否存在一組消息-類型同態(tài)性、相似性、等價性等結(jié)構(gòu)的原子類消息加密數(shù)據(jù), 代數(shù)特征明顯, 易于判別. Paulson 的歸納法基于定理證明器Isabelle 的自動實現(xiàn), 分析結(jié)果安全不代表協(xié)議沒有攻擊, 典型應(yīng)用如文獻(xiàn)[28] 對Yahalom-Paulson 協(xié)議的分析, 及文獻(xiàn)[11] 對ffgg 協(xié)議的分析. 串空間理論構(gòu)造攻擊建立關(guān)于測試元素的非空集合S, 基于Dolev-Yao 模型遍歷攻擊能力規(guī)則, 檢測S的最小元是否在攻擊者串上, 例如文獻(xiàn)[9].

表1 協(xié)議分析方法對照表Table 1 Comparison of protocol analysis methods

證明:若密碼協(xié)議原子類消息存在同態(tài)性或相似性或等價性等類型數(shù)據(jù)結(jié)構(gòu), 由同態(tài)性定義7 或相似性定義8 或等價性定義9, 以及類型缺陷攻擊的定義6 可知, 該密碼協(xié)議中存在類型缺陷攻擊.

類型構(gòu)造攻擊方法步驟如下:

(1) 檢測該密碼協(xié)議的原子類消息是否存在同態(tài)性或相似性或等價性等類型數(shù)據(jù)結(jié)構(gòu), 若不存在, 則退出; 若存在, 則該協(xié)議存在類型缺陷, 可進(jìn)入第(2) 步.

(2) 依據(jù)協(xié)議叢C中節(jié)點n的隨機(jī)數(shù)a的原子類加密數(shù)據(jù)t={h}k(a ∈h) 構(gòu)造一個非空集合S;根據(jù)引理1, 該非空集合S存在最小元節(jié)點n1, 遍歷Dolev-Yao 攻擊者模型, 判斷節(jié)點n1是否在攻擊者原子串上, 若不存在, 則一定在常規(guī)者串上; 若節(jié)點n1不是I={n:a ?n}的入口點,則在該常規(guī)者串上節(jié)點n1之前還存在另一個節(jié)點n2, 使a源發(fā)于節(jié)點n2.

(3) 由于該常規(guī)者串為發(fā)送包含隨機(jī)數(shù)a的原子類加密數(shù)據(jù)t={h}k(a ∈h) 的節(jié)點值(n1) 所在串,可知在響應(yīng)者串上, 根據(jù)響應(yīng)者串的一般形式, 對該常規(guī)者串實例化, 得到一個偽正規(guī)串S1; 對于收到并解密包含隨機(jī)數(shù)a的原子類加密數(shù)據(jù)t={h}k(a ∈h) 的節(jié)點值所在串, 可知在響應(yīng)者串上, 根據(jù)響應(yīng)者串的一般形式, 對該常規(guī)者串實例化, 得到另一個偽正規(guī)串S2.

(4) 若此偽正規(guī)串不滿足協(xié)議規(guī)約, 則舍棄; 若滿足協(xié)議規(guī)約, 根據(jù)偽正規(guī)串S1與S2, 以及隨機(jī)因子的新鮮性定理和自由加密假設(shè)公理, 則可得到一個攻擊串.

3.2 類型構(gòu)造攻擊方法的應(yīng)用

類型形式化構(gòu)造攻擊方法, 已廣泛應(yīng)用于密碼認(rèn)證協(xié)議的形式化分析, 而且找出了一系列密碼協(xié)議的類型缺陷攻擊.

(a) Needham-Schroeder[15]簡化版本協(xié)議如下:

(1)A →B:{Na,A}KB

(2)B →A:{Na,Nb}KA

(3)A →B:{Nb}KB

對Needham-Schroeder 簡化版本協(xié)議分析如圖1 所示. 一方面, 攻擊者假冒主體A與B通信,同時又與A通信, 通過重放消息{Na,Nb}KA而導(dǎo)致中間人攻擊; 另一方面, 攻擊者將主體標(biāo)識P當(dāng)做隨機(jī)數(shù)與主體B通信, 同時與主體B正常通信, 導(dǎo)致類型錯誤攻擊. 究其原因存在一組消息-類型同態(tài)結(jié)構(gòu)原子類加密數(shù)據(jù)t1={h1|Na,A}KB與t2={h2|Na,Nb}KA, 只有打破這種結(jié)構(gòu), 方能制止這類攻擊, 如圖1 中的Needham-Schroeder-Low 簡化版本協(xié)議.

圖1 N-S 協(xié)議及其類型構(gòu)造攻擊Figure 1 N-S protocol and its type construction attack

(b) Yahalom[29]簡化版本協(xié)議如下:

(1)A →B:A,Na

(2)B →S:B,{A,Na,Nb}KBS

(3)S →A:{B,KAB,Na,Nb}KAS ,{A,KAB}KBS

(4)A →B:{A,KAB}KBS ,{Nb}KAB

對Yahalom 簡化版本協(xié)議分析如圖2 所示, 攻擊者通過假冒主體A將消息{A,Na,Nb}KBS,{}NaNb發(fā)送給主體B, 并與主體B擁有攻擊者構(gòu)造的會話密鑰NaNb, 導(dǎo)致類型錯誤攻擊.

圖2 Yahalom 協(xié)議及其類型構(gòu)造攻擊Figure 2 Yahalom protocol and its type construction attack

(c) Otway-Rees[30,31]認(rèn)證協(xié)議如下:

(1)A →B:M,A,B,{Na,M,A,B}KAS

(2)B →S:M,A,B,{Na,M,A,B}KAS ,{Nb,M,A,B}KBS

(3)S →B:M,{Na,KAB}KAS ,{Nb,KAB}KBS

(4)B →A:M,{Na,KAB}KAS

對Otway-Rees 認(rèn)證協(xié)議分析如圖3 所示, 攻擊者假冒主體B發(fā)送消息M,{Na,M,A,B}KAS給主體A, 并與主體A擁有攻擊者構(gòu)造的會話密鑰M,A,B; 又由于服務(wù)器S 產(chǎn)生的會話密鑰KAB對于主體B而言, 識別不了它的新鮮性, 因此可誘發(fā)重放攻擊; 改進(jìn)后的Otway-Rees認(rèn)證協(xié)議[31], 只是增加了各自的主體標(biāo)識, 對于會話密鑰KAB的新鮮性判別沒有幫助, 所以還會導(dǎo)致重放攻擊, 可通過添加時間戳Ts來克服這類攻擊. 總之, 究其原因Otway-Rees 認(rèn)證協(xié)議存在一組消息-類型同態(tài)結(jié)構(gòu)的原子類加密數(shù)據(jù):t1={h1|Na,M,A,B}KAS與t2={h2|Na,KAB}KAS, 只有打破這種結(jié)構(gòu), 才能制止這類攻擊, 如圖3 中d.Otway-Rees 認(rèn)證協(xié)議.

圖3 Otway-Rees 認(rèn)證協(xié)議及其類型構(gòu)造攻擊Figure 3 Otway-Rees authentication protocol and its type construction attack

(d) Wide-Mouth Frog 協(xié)議[18]如下:

(1)A →S:A,{Ta,B,KAB}KAS

(2)S →B:{Ts,A,KAB}KBS

對Wide-Mouth Frog 協(xié)議分析如圖4 所示, 由于主體發(fā)送的消息類型與服務(wù)器發(fā)送的消息類型一致, 導(dǎo)致了攻擊者可以在中間不斷的重發(fā)消息, 從而不斷的更新時間戳, 導(dǎo)致誘發(fā)了類型缺陷攻擊. 主要原因是該協(xié)議中存在一組消息類型相似性的加密數(shù)據(jù), 即t1={h1|Ta,B,KAB}KAS,t2={h2|Ts,A,KAB}KBS, 只有打破這種結(jié)構(gòu), 方能制止這類攻擊. 由于在改進(jìn)的Wide-Mouth Frog 協(xié)議里, 仍存在一組消息類型同態(tài)性的加密數(shù)據(jù), 即t1={h1|Ta,B,KAB}KAS,t2={h2|A,TS,KAB}KBS, 由性質(zhì)4 可知, 存在類型缺陷, 如圖5 所示.

圖4 大嘴青蛙協(xié)議及其類型缺陷攻擊Figure 4 Wide-Mouth Frog protocol and its type flaw attack

圖5 改進(jìn)后的大嘴青蛙協(xié)議及其類型缺陷攻擊Figure 5 Improved Wide-Mouth Frog protocol and its type flaw attack

(e) ffgg 簡化版協(xié)議[11]如下:

(1)A →B:A,N2

(2)B →A:B,N1,N2

(3)A →B:A,{N1,N2,KAB}P K

(4)B →A:N1,N2,{N2,KAB,N1}P K

對ffgg 協(xié)議分析如圖6 所示, 該協(xié)議的消息(3) 與消息(4) 存在一組消息類型等價性的加密數(shù)據(jù),即t1={h1|N1,N2,KAB}P K,t2={h2|N2,KAB,N1}P K, 導(dǎo)致類型缺陷, 使主體A和B之間的共享密鑰KAB不僅沒有得到彼此確認(rèn), 而且共享密鑰KAB泄漏了, 如圖6(b). 只有打破這種結(jié)構(gòu), 方能制止這類攻擊, 改進(jìn)后的ffgg 協(xié)議如圖6(c).

圖6 ffgg 協(xié)議及其類型缺陷攻擊Figure 6 ffgg protocol and its type flaw attack

3.3 密碼認(rèn)證協(xié)議的設(shè)計準(zhǔn)則

針對密碼認(rèn)證協(xié)議設(shè)計面臨的類型缺陷形式化弊端, 給出了無消息-類型同態(tài)性、相似性、等價性等密碼協(xié)議設(shè)計準(zhǔn)則, 使密碼協(xié)議設(shè)計漸趨精細(xì)化、標(biāo)準(zhǔn)化、科學(xué)化.

提出在密碼協(xié)議設(shè)計中應(yīng)遵循的準(zhǔn)則: 在密碼協(xié)商協(xié)議中,

(1) 無消息-類型同態(tài)性結(jié)構(gòu): 協(xié)議消息序列中原子類消息加密數(shù)據(jù)項之間無消息-類型同態(tài)性結(jié)構(gòu).(2) 無消息-類型相似性結(jié)構(gòu): 協(xié)議消息序列中原子類消息之間無消息-類型相似性結(jié)構(gòu).(3) 無消息-類型等價性結(jié)構(gòu): 協(xié)議消息序列中原子類消息之間無消息-類型等價性結(jié)構(gòu).

4 實例分析

Yahalom-Paulson 協(xié)議是由Paulson 在文獻(xiàn)[12] 中給出的. 該協(xié)議整體框架與原始Yahalom 協(xié)議一致, 共三個參與實體: 協(xié)議發(fā)起者、協(xié)議響應(yīng)者和可信第三方服務(wù)器. 協(xié)議使用對稱密鑰加密, 完成協(xié)議發(fā)起者與響應(yīng)者之間的相互認(rèn)證以及會話密鑰的秘密分發(fā). 描述如下:

(1)A →B:A,Na

(2)B →S:B,Nb,{A,Na}Kbs

(3)S →A:Nb,{B,K,Na}Kas,{A,B,K,Nb}Kbs

(4)A →B:{A,B,K,Nb}Kbs,{Nb}K

使用檢測類型缺陷的構(gòu)造攻擊方法對該協(xié)議進(jìn)行分析.

命題1若Σ 是一個三方協(xié)議串空間,C是Σ 的一個叢,Kas/∈KP,Kbs/∈KP,K/∈KP,KP是攻擊者已知的密鑰集合, 則對所有的節(jié)點m ∈C,{Kas,Kbs,K}/?uns-term(m).

證明:因為{Kas,Kbs,K}從不在一個常規(guī)節(jié)點源發(fā), 由引理1 可知,{Kas,Kbs,K}/?uns-term(m).

命題2假設(shè)Σ 是一個三方協(xié)議串空間,C是Σ 的一個叢. 若下面的條件滿足:

證明:首先, 根據(jù)定義7–9, 檢測該密碼協(xié)議的原子類消息是否存在同態(tài)性或相似性或等價性等類型數(shù)據(jù)結(jié)構(gòu). 對Yahalom-Paulson 協(xié)議進(jìn)行觀察可知, 該協(xié)議存在一組消息類型同態(tài)性結(jié)構(gòu)的原子類加密數(shù)據(jù):t1={h1|A,Na}Kbs與t2={h2|A,B,K,Nb}Kbs, 由定理1 可知, 存在類型缺陷. 由于Nb ?term(〈s,2〉), 且Nb在〈s,2〉唯一源發(fā). 令S={n ∈C:{A,Na}Kbs ?uns-term(n)}, 由于{A,Na}Kbs ?uns-term(〈s,3〉), 所以〈s,3〉 ∈S, 因此S非空. 由引理1 可知, 集合S中有一個最小元n1, 由定理4 可知,n1的符號是正的.n1不可能位于攻擊者串上, 因為攻擊者串是由攻擊者原子行為跡組成的, 所以只需要顯示n1不可能位于攻擊者原子行為跡上即可. 驗證如下:

(1)M串: 若n1在M串上, 則由M串的形式〈+t〉,t ∈M0, 可知{A,Na}Kbs ?n1=t, 這與t僅僅是原子消息相矛盾;

(2) 顯然,F串、T串、K串均不可能;

(3) 由于Kbs/∈KP, 所以D串也不可能;

(4)C串: 若n1在C串上, 則由C串的形式〈-g,-h,+gh〉, 得n1=gh, 由于{A,Na}Kbs是簡單的加密值, 所以{A,Na}Kbs是g或h的子術(shù)語, 因此C串上的正節(jié)點不可能是集合S中的極小元;

(5)E串: 若n1在E串上, 則由E串的形式〈-K,-m,+{m}K〉, uns-term(n1)={A,Na}Kbs,所以{A,Na}Kbs ?{m}K, 由引理2 可知,{A,Na}Kbs={m}K或{A,Na}Kbs ?m. 若{A,Na}Kbs ?m, 則集合S的極小元不是正節(jié)點; 若{A,Na}Kbs={m}K, 由引理3 可知,m={A,Na},K=Kbs, 通過檢查叢中常規(guī)者串節(jié)點的術(shù)語, 沒有一個節(jié)點以明文的形式發(fā)送了包含{Kbs}, 因此這種情形不成立.

(6)S串: 若n1在S串上, 則由S串的形式{-gh,+g,+h}, 假定term(n1) = +g, 因為{A,Na}Kbs ?g, 所以{A,Na}Kbs ?gh, 且在S串上,-gh ?n1, 這與n1是集合S中的最小元相矛盾.

所以,n1不在攻擊者原子行為跡上, 即不在攻擊者串上, 因此一定在常規(guī)者串上, 又因為節(jié)點n1不是I={n:Nb ?n}的入口點, 所以在該常規(guī)者串上節(jié)點n1之前還存在另一個節(jié)點n2, 使Nb源發(fā)于節(jié)點n2, 不妨設(shè)此常規(guī)者串為T.

由于常規(guī)者串T含有包括隨機(jī)數(shù)Nb的最小元節(jié)點n1, 且Nb在〈S1,2〉唯一源發(fā). 所以有:

且發(fā)送了包含原子類加密數(shù)據(jù){C,X1}Kbs的極小元節(jié)點值{D,Nb,{C,X1}Kbs}.

對于收到并解密原子類加密數(shù)據(jù){C,X1}Kbs的極小元節(jié)點值{D,Nb,{C,X1}Kbs}所在串的一般形式為:

由引理3 可得:X2=Nb.

由式(3)和(4)可以刻畫出具體的攻擊過程, 描述如下:

(1) 攻擊者可以成功地冒充協(xié)議發(fā)起者.

攻擊者成功冒充A, 結(jié)束時與B擁有攻擊者構(gòu)造的會話密鑰KI.

(2) 攻擊者可以成功地冒充協(xié)議響應(yīng)者.

其中H為任意加密消息項, 攻擊者成功冒充成B, 并與A擁有攻擊者構(gòu)造的會話密鑰KI.

對Yahalom-Paulson 簡化版本協(xié)議分析如圖7 所示, 攻擊者通過假冒主體A與主體B進(jìn)行了兩次會話, 最后成功將消息{A,B,K,Nb}Kbs,{Nb}K發(fā)送給主體B, 并與主體B擁有攻擊者構(gòu)造的會話密鑰K; 同理, 攻擊者通過假冒主體B與主體A進(jìn)行了兩次會話, 最后成功將消息H,{Nb}K(H為加密的未知消息) 發(fā)送給主體B, 并與主體A擁有攻擊者構(gòu)造的會話密鑰K. 究其原因在Yahalom-Paulson 協(xié)議存在一組消息-類型同態(tài)結(jié)構(gòu)的原子類加密數(shù)據(jù):t21={h21|A,Na}Kbs與t22={h22|A,B,K,Nb}Kbs,只有打破這種結(jié)構(gòu), 方能制止這類攻擊, 如圖7 中Yahalom-Paulson 協(xié)議(c), 改進(jìn)的Yahalom-Paulson協(xié)議具體如下:

(1)A →B:A,Na

(2)B →S:B,{A,Na,Nb}KBS

(3)S →A:{B,KAB,Nb,Na}KAS ,{Nb,KAB}KBS

(4)A →B:{Nb.KAB}KBS ,{Nb}KAB

圖7 Yahalom-Paulson 協(xié)議及其類型構(gòu)造攻擊Figure 7 Yahalom-Paulson protocol and its type construction attack

5 結(jié)束語

檢測類型缺陷的形式化構(gòu)造攻擊方法總結(jié)了密碼認(rèn)證協(xié)議中的消息類型特點, 指出了一組消息-類型同態(tài)性、相似性、等價性等原子類加密數(shù)據(jù)是類型缺陷攻擊存在的充分條件, 并且結(jié)合實例分析了認(rèn)證協(xié)議及其類型缺陷攻擊情況, 指出了在密碼認(rèn)證協(xié)議設(shè)計時應(yīng)遵循的準(zhǔn)則, 為今后密碼認(rèn)證協(xié)議設(shè)計提供了理論依據(jù). 下一步將繼續(xù)研究并完善檢測類型缺陷的形式化構(gòu)造攻擊方法, 研發(fā)基于該方法的密碼協(xié)議自動化分析工具, 以期實現(xiàn)密碼協(xié)議的自動化設(shè)計與分析.