數(shù)據(jù)獨(dú)立技術(shù)在CSP協(xié)議模型中的設(shè)計(jì)
1996年,Lowe首先使用通信順序進(jìn)程CSP和模型檢測(cè)技術(shù)分析NSPK(Needham-Schroeder Public Key)協(xié)議,并成功發(fā)現(xiàn)了協(xié)議中的一個(gè)中間人攻擊行為。隨后,Roscoe對(duì)CSP和FDR(Fallures-Divergence Refinenent)的組合做了進(jìn)一步研究,認(rèn)為CSP方法是形式分析安全協(xié)議的一條新途徑。事實(shí)證明,CSP方法對(duì)于安全協(xié)議分析及發(fā)現(xiàn)安全協(xié)議攻擊非常有效。但是類似FDR的模型檢測(cè)通常受NONce、Key等新鮮值大小的限制,而在實(shí)際執(zhí)行中所需的數(shù)據(jù)值比這大得多。使用數(shù)據(jù)獨(dú)立技術(shù)使結(jié)點(diǎn)能夠調(diào)用無(wú)限的新鮮值以保證實(shí)例無(wú)限序列的運(yùn)行。本文將研究Roscoe這些理論,對(duì)CSP協(xié)議模型進(jìn)行設(shè)計(jì)與實(shí)現(xiàn),從而解決有限檢測(cè)的問(wèn)題。
1 CSP協(xié)議模型
在CSP模型中,協(xié)議參與者被表示為CSP的進(jìn)程(process),消息被表示為事件(event),進(jìn)而協(xié)議被表示為一個(gè)通信順序進(jìn)程的集合。
CSP協(xié)議模型由一些可信的參與者進(jìn)程和入侵者進(jìn)程組成,進(jìn)程并行運(yùn)行且通過(guò)信道交互。以NSPK協(xié)議為例。該協(xié)議的CSP模型包括兩個(gè)代理(初始者a,響應(yīng)者b)和一個(gè)能執(zhí)行密鑰產(chǎn)生、傳送或認(rèn)證服務(wù)的服務(wù)器s,它們之間通過(guò)不可信的媒介(入侵者)通信,所以存在四個(gè)CSP進(jìn)程.
Initiator a的CSP進(jìn)程描述如下:
響應(yīng)者b與服務(wù)器s也有著相似的描述。
攻擊者進(jìn)程被描述為:
2 數(shù)據(jù)獨(dú)立技術(shù)
數(shù)據(jù)獨(dú)立技術(shù)是本論文的關(guān)鍵技術(shù).它起源于Lazic的數(shù)據(jù)獨(dú)立研究。
2.1 一般的數(shù)據(jù)獨(dú)立分析
如果一個(gè)進(jìn)程P對(duì)于類型T沒(méi)有任何限制,則P對(duì)于T類型是數(shù)據(jù)獨(dú)立的。此時(shí),T可以被視為P的參數(shù)。
通常,數(shù)據(jù)獨(dú)立分析是為以類型T為參數(shù)的驗(yàn)證問(wèn)題發(fā)現(xiàn)有限閾值。如果對(duì)于T的閾值,可以驗(yàn)證系統(tǒng)成立,則對(duì)于所有較大的T值也可以驗(yàn)證系統(tǒng)成立。這點(diǎn)對(duì)于很多問(wèn)題都是成立的。
安全協(xié)議模型中的許多特征都可以被視為數(shù)據(jù)獨(dú)立實(shí)體。常見(jiàn)的key、nonce可以作為模型中進(jìn)程的參數(shù)。
對(duì)依賴nonce和密鑰(和依賴協(xié)議的其他簡(jiǎn)單數(shù)據(jù)對(duì)象)惟一性的安全協(xié)議進(jìn)行的閥值計(jì)算,主要是發(fā)現(xiàn)進(jìn)程存儲(chǔ)量的閾值,并不能直接解決驗(yàn)證的局限性,也就不能直接應(yīng)用于安全協(xié)議模型。
2.2 Roscoe的數(shù)據(jù)獨(dú)立技術(shù)
上節(jié)證明了一般目標(biāo)的數(shù)據(jù)獨(dú)立結(jié)果不適用于安全協(xié)議分析。所以Roscoe對(duì)這些結(jié)果進(jìn)行推論。發(fā)展了數(shù)據(jù)獨(dú)立技術(shù)。本節(jié)將介紹幾條對(duì)課題研究具有重要理論意義的推論。
(1)基本原則
對(duì)一般數(shù)據(jù)獨(dú)立分析結(jié)果進(jìn)行推論所基于的基本原則也是證明數(shù)據(jù)獨(dú)立理論最重要的方法。即對(duì)進(jìn)程P的參數(shù)類型T應(yīng)用Conapsint函數(shù)φ建立映射關(guān)系,證明映射前P(T)的行為經(jīng)過(guò)函數(shù)轉(zhuǎn)換,是P(φ(T))行為的子集。
對(duì)于安全協(xié)議主要研究進(jìn)程的跡??梢院苤庇^地發(fā)現(xiàn)如果Collapsing函數(shù)φ是單映射的(T的所有成員被映射為不同值),并應(yīng)用于進(jìn)程P的參數(shù)類型T上(P對(duì)于T數(shù)據(jù)獨(dú)立),則因?yàn)門的所有成員被映射為不同值,所以映射前的行為等價(jià)于映射后的行為,如式(1)所示:
如果使用的Collapsing函數(shù)φ為非單映射函數(shù),則有可能改變等價(jià)測(cè)試結(jié)果,產(chǎn)生不等式(2):
該不等式只適用于變量,對(duì)于程序中的常量,情況有所不同。因此提出下面兩個(gè)條件:
PosConjEqT(Positive Conjunetions of Equality teSTs)條件由Lazic提出,該條件可以使變量使用
非單映射函數(shù)的進(jìn)程再度滿足等式(1)。
對(duì)于常量雖然不能重新滿足等式(1),但可滿足不等式(3):
協(xié)議的某些方面可能并不滿足PosConjEqT條件,如代理進(jìn)程可能需要執(zhí)行擁有常量(例如名字)的不等式測(cè)試。因此,針對(duì)常量集C定義PosConjEqT′c條件如下:
如果進(jìn)程P對(duì)于常量集C滿足下列條件,則稱進(jìn)程P滿足PosConjEqT′c條件。該條件滿足PosConjEqT條件,但與PosConjEqT條件的不同之處是:對(duì)于至少包含常量集C一個(gè)成員的等價(jià)測(cè)試,P可能擁有non-STOP結(jié)果。(2)明確推理系統(tǒng)
協(xié)議模型中的代理進(jìn)程是標(biāo)準(zhǔn)類型進(jìn)程且易于進(jìn)行滿足PosConjEqT′c條件的特性檢測(cè)。但I(xiàn)ntruder進(jìn)程可以依靠推理系統(tǒng)指定產(chǎn)生或破壞信息的規(guī)則,這一特性決定了其更為復(fù)雜。
如果推理系統(tǒng)滿足這樣的條件,即對(duì)于類型間的任意函數(shù)φ:T1→T2,只要(X,f)是系統(tǒng)產(chǎn)生的適用于類型T1推論,則(φ(X),φ(f))就是適用于T2的推論,進(jìn)而稱該推理系統(tǒng)與這些類型參數(shù)T明確相關(guān)。其中要求推理的產(chǎn)生在T上對(duì)稱(也就是平等對(duì)待T的所有成員)并且對(duì)出現(xiàn)在推理左邊的T成員不再具有不等的要求。
從上述定義可以確定這樣的性質(zhì):如果在明確推理系統(tǒng)中建立攻擊者,并且攻擊者的初始知識(shí)集不包含對(duì)于類型T成員(除了常數(shù)C)的非等價(jià)測(cè)試,那么該進(jìn)程滿足PosConjEqT′c條件(并且因此,整個(gè)協(xié)議模型滿足網(wǎng)絡(luò)其他部分的條件)。
可以看出系統(tǒng)成分是否滿足上述性質(zhì)對(duì)研究至關(guān)重要。只有滿足這些條件才能夠在協(xié)議分析的CSP模型中構(gòu)造更為復(fù)雜的事件。
(3)Roscoe數(shù)據(jù)獨(dú)立技術(shù)的意義
Roscoe在文獻(xiàn)中引入了NM進(jìn)程,負(fù)責(zé)產(chǎn)生系統(tǒng)所需的無(wú)眼新鮮值。那么在以前運(yùn)行中,一個(gè)進(jìn)程要在每一次輸出通信時(shí)產(chǎn)生一個(gè)新鮮值v;而現(xiàn)在就會(huì)將這次通信變?yōu)橄蛟撨M(jìn)程輸入v,并且要求其與相應(yīng)的NM進(jìn)程同步。
為了滿足新鮮值的惟一性和新鮮性,引入的NM進(jìn)程需進(jìn)行下列操作:存儲(chǔ)所有發(fā)送的新鮮值,相同的新鮮值只發(fā)送一次,不發(fā)送屬于攻擊者的新鮮值。顯然這些操作并不滿足PosConjEqT條件。
Roscoe沒(méi)有單獨(dú)使用NM進(jìn)程進(jìn)行無(wú)限新鮮值的分發(fā),而是應(yīng)用數(shù)據(jù)獨(dú)立技術(shù),在NM進(jìn)程中執(zhí)行Collapse轉(zhuǎn)換,通過(guò)轉(zhuǎn)換從有限集生成無(wú)限新鮮值。
Roscoe的數(shù)據(jù)獨(dú)立技術(shù)提供了這樣的理論基礎(chǔ):若系統(tǒng)的所有成分滿足PosConjEqT′c條件,則大協(xié)議系統(tǒng)中轉(zhuǎn)換前的全部行為(就系統(tǒng)跡而言)可以用經(jīng)過(guò)映射的相應(yīng)的有限系統(tǒng)描述。這一技術(shù)保證了可以在大協(xié)議中應(yīng)用非單映射轉(zhuǎn)換,將問(wèn)題簡(jiǎn)化為相應(yīng)的有限系統(tǒng)。
3 數(shù)據(jù)獨(dú)立技術(shù)在CSP協(xié)議模型中的設(shè)計(jì)
數(shù)據(jù)獨(dú)立技術(shù)使模型檢測(cè)器的證明更加完整,因?yàn)樗膽?yīng)用使大協(xié)議的建模成為可能。
3.1 協(xié)議模型的擴(kuò)展
為了解決驗(yàn)證的局限性,需要系統(tǒng)代理能夠在實(shí)際類型保持有限的情況下,調(diào)用無(wú)限的不同的新鮮值。沿用Roscoe的方法,引入Manager進(jìn)程擴(kuò)展CSP協(xié)議模型。與以前的協(xié)議模型相比,該模型引入了Manager進(jìn)程。此進(jìn)程與Intruder進(jìn)程相互配合以實(shí)現(xiàn)新鮮值的循環(huán)利用,因此可視為新鮮值的循環(huán)機(jī)制??梢哉f(shuō),該模型是對(duì)Roscoe文獻(xiàn)的一個(gè)擴(kuò)展和細(xì)化,可以證明其滿足PosConjEqT′c條件:
(1)進(jìn)程中的數(shù)據(jù)類型隨機(jī)數(shù)Na、Nb和密鑰Kdo均為數(shù)據(jù)獨(dú)立類型。
(2)可信代理進(jìn)程為標(biāo)準(zhǔn)類型進(jìn)程,滿足PosConjEqT′c條件。
(3)攻擊者進(jìn)程在明確推理系統(tǒng)中建立,并且其初始知識(shí)集不包含對(duì)類型T成員(除了常數(shù)C)的非等價(jià)測(cè)試,滿足P0sConjEqT′c條件。
因此該系統(tǒng)中轉(zhuǎn)換前全部行為可以用經(jīng)過(guò)映射的、相應(yīng)的有限系統(tǒng)描述。也正基于此,可以在無(wú)限新鮮值的產(chǎn)生過(guò)程中應(yīng)用非單映射轉(zhuǎn)換,從而將其簡(jiǎn)化為相應(yīng)的有限過(guò)程,以形成完整的形式化描述。
3.2 協(xié)議各對(duì)象的描述
對(duì)于每一個(gè)新鮮值引入對(duì)應(yīng)的Manager進(jìn)程,取消可信代理分發(fā)新鮮值的能力,只在單次運(yùn)行期間存儲(chǔ)新鮮值,并要求其在完成協(xié)議一次運(yùn)行時(shí)“遺忘”所有存儲(chǔ)的新鮮值。當(dāng)新鮮值v不再被可信參與者所知(存儲(chǔ))時(shí),稱v被“遺忘”。攻擊者能夠存儲(chǔ)在網(wǎng)絡(luò)中所見(jiàn)的所有新信息。為了能夠產(chǎn)生無(wú)限的新鮮值,可以對(duì)攻擊者存儲(chǔ)的新鮮值應(yīng)用collasphag函數(shù),從而啟動(dòng)所提出的新鮮值循環(huán)機(jī)制。即當(dāng)新鮮值v在網(wǎng)絡(luò)中被“遺忘”時(shí)可以被循環(huán)再利用。一旦該值被循環(huán)利用,相應(yīng)的Manager進(jìn)程可以在網(wǎng)絡(luò)中再次將其作為新鮮值使用。
(1)可信進(jìn)程
在擴(kuò)展的CSP協(xié)議模型中,進(jìn)程描述如下:
擴(kuò)展后的描述主要有三處變動(dòng):第一,進(jìn)程被定義為遞歸進(jìn)程,表示Initiator可以執(zhí)行無(wú)限數(shù)量的序列運(yùn)行;而在之前的模型描述中,進(jìn)程在SKIP終止。第二,新鮮Nonce NA不再是參數(shù),而是來(lái)自集合NonceF(通過(guò)定義,進(jìn)程可以接收該集合中的任意值);之后將會(huì)介紹Manager進(jìn)程如何終止這些值的產(chǎn)生。第三,添加了close事件表示進(jìn)程重新開(kāi)始執(zhí)行初始狀態(tài)。該事件標(biāo)志著進(jìn)程一次運(yùn)行的結(jié)束,在新鮮值的循環(huán)機(jī)制中發(fā)揮重要作用。(2)Manager進(jìn)程
Manger進(jìn)程負(fù)責(zé)利用有限資源向網(wǎng)絡(luò)提供無(wú)限的新鮮值。需要為每一種數(shù)據(jù)獨(dú)立類型分別定義一個(gè)Manager進(jìn)程,在上述的Yahalom協(xié)議中需要定義一個(gè)管理Nonce類型值的Manager進(jìn)程——Nonce Manager和一個(gè)管理SESSionKey類型值的Manager進(jìn)程——SessionKeyManager。本節(jié)研究Manager進(jìn)程的CSP設(shè)計(jì)和實(shí)現(xiàn)。
將協(xié)議中的每一種數(shù)據(jù)獨(dú)立類型T所擁有的值分為兩類集合。第一類集合稱為Foreground值,這些值被阿絡(luò)視為新鮮值。第二類集合由Background值組成,表示類型r舊的或靜態(tài)的值。當(dāng)循環(huán)利用Intruder存儲(chǔ)的新鮮值時(shí),將使用這一集合進(jìn)行映射。
可以說(shuō)Manager進(jìn)程是建模過(guò)程中的人造產(chǎn)物,并不代表實(shí)際對(duì)象而只代表了對(duì)于新鮮值的某種操作,主要完成觸發(fā)“遺忘”值的循環(huán)和分發(fā)新鮮值的功能。
為了對(duì)Manager進(jìn)程進(jìn)行形式化描述,此處定義兩個(gè)新的事件:
?、賗fclose.(v):表示最后一個(gè)存儲(chǔ)v的進(jìn)程是否已經(jīng)“遺忘”了v,如果“遺忘”為true,否則為false。
②replace.(v,b):表示對(duì)intruder存儲(chǔ)中含有v的所有信息進(jìn)行操作,將v的所有實(shí)例替換為Background值b,即完成Collapse函數(shù)的非單映射。在相對(duì)意義上,v又會(huì)被視為新鮮,即實(shí)現(xiàn)了有限值產(chǎn)生無(wú)限新鮮值。
同時(shí),使用下述策略確定循環(huán)值映射為哪個(gè)Background值:對(duì)于每一種數(shù)據(jù)獨(dú)立類型T,定義兩個(gè)不同的Background值TPk和TBu。將所有intruder所知的Foreground值映射為TBk,不知的映射為TBk。
通過(guò)上述定義和策略研究,描述Manager進(jìn)程如下:
其中,T表示數(shù)據(jù)類型,TF代表該數(shù)據(jù)類型的Foreground集合,TBk和TBa分別代表不同的Background值TBk和TBu。
為了編譯階段的效率,將其分解為并行結(jié)構(gòu)。因?yàn)閷?duì)每一個(gè)新鮮值的控制都是獨(dú)立的。在Yahalom協(xié)議中,假設(shè)定義新鮮Nonce集為{N1,N2},新鮮SessionKey集為{K1},則可建模為下面的并行結(jié)構(gòu):
其中,T表示數(shù)據(jù)類型,TF代表該數(shù)據(jù)類型的Foreground集合,TBk和TBa分別代表不同的Background值TBk和TBu。
為了編譯階段的效率,將其分解為并行結(jié)構(gòu)。因?yàn)閷?duì)每一個(gè)新鮮值的控制都是獨(dú)立的。在Yahalom協(xié)議中,假設(shè)定義新鮮Nonce集為{N1,N2},新鮮SessionKey集為{K1},則可建模為下面的并行結(jié)構(gòu):
(3)Intmdez進(jìn)程
擴(kuò)展Intruder進(jìn)程,使其與Manager進(jìn)程一起形成(數(shù)據(jù)獨(dú)立類型)新鮮值循環(huán)機(jī)制。當(dāng)啟動(dòng)新鮮值v的循環(huán)機(jī)制時(shí),對(duì)存儲(chǔ)中含有v的所有信息進(jìn)行操作,將v的所有實(shí)例替換為Background值b。
沿用在Manager進(jìn)程中的定義和研究,Intruder進(jìn)程描述如下:
4 數(shù)據(jù)獨(dú)立技術(shù)在CSP協(xié)議模型中的實(shí)現(xiàn)
CSPM是CSP的機(jī)器可讀語(yǔ)言,適用于FDR、ProBE等各種工具。一般的程序語(yǔ)言以可執(zhí)行的形式描述算法。CSPM也包含功能程序語(yǔ)言,但是其主要目標(biāo)不同:此處它以自動(dòng)操作的形式支持并行系統(tǒng)的描述。因此,CSPM腳本通常被定義為一組進(jìn)程而不是程序。作為基礎(chǔ)層,CSPM腳本還支持表達(dá)式和函數(shù)。為了能夠?qū)U(kuò)展后的協(xié)議模型輸入驗(yàn)證工具ProBE并完成驗(yàn)證,需要將擴(kuò)展CSP描述編寫(xiě)成CSPM腳本(因?yàn)镻roBE編譯接口無(wú)法擴(kuò)展)。因此在編寫(xiě)CSPM腳本過(guò)程中定義了相應(yīng)的新事件、新進(jìn)程以實(shí)現(xiàn)擴(kuò)展,最終將手工完成的CSPM腳本輸入工具,完成驗(yàn)證。
本文的研究確保了協(xié)議中每個(gè)代理都可以執(zhí)行無(wú)限數(shù)量的序列運(yùn)行,解決了有限檢測(cè)問(wèn)題。但是,并行運(yùn)行的代理實(shí)體數(shù)量的無(wú)限問(wèn)題沒(méi)有得到解決;如果在模型中沒(méi)有發(fā)現(xiàn)攻擊。不能夠證明在更高的并行度不存在攻擊。這也是今后的一個(gè)研究方向。
數(shù)據(jù)獨(dú)立技術(shù)可以在一定的協(xié)議范圍內(nèi)使用,不可以直接運(yùn)用在包含時(shí)戳的協(xié)議中。因?yàn)閳?zhí)行的典型操作超出了數(shù)據(jù)獨(dú)立范圍,如使用對(duì)比算子x<y決定時(shí)戳y是否比時(shí)戳x舊。擴(kuò)展研究處理時(shí)戳可以作為未來(lái)的研究方向。