數(shù)據(jù)獨(dú)立技術(shù)在CSP協(xié)議模型中的設(shè)計(jì)

　　將協(xié)議中的每一種數(shù)據(jù)獨(dú)立類型T所擁有的值分為兩類集合。第一類集合稱為Foreground值，這些值被阿絡(luò)視為新鮮值。第二類集合由Background值組成，表示類型r舊的或靜態(tài)的值。當(dāng)循環(huán)利用Intruder存儲的新鮮值時(shí)，將使用這一集合進(jìn)行映射。

　　可以說Manager進(jìn)程是建模過程中的人造產(chǎn)物，并不代表實(shí)際對象而只代表了對于新鮮值的某種操作，主要完成觸發(fā)“遺忘”值的循環(huán)和分發(fā)新鮮值的功能。

　　為了對Manager進(jìn)程進(jìn)行形式化描述，此處定義兩個(gè)新的事件：

　?、賗fclose．(v)：表示最后一個(gè)存儲v的進(jìn)程是否已經(jīng)“遺忘”了v，如果“遺忘”為true，否則為false。

　?、趓eplace．(v,b)：表示對intruder存儲中含有v的所有信息進(jìn)行操作，將v的所有實(shí)例替換為Background值b，即完成Collapse函數(shù)的非單映射。在相對意義上，v又會被視為新鮮，即實(shí)現(xiàn)了有限值產(chǎn)生無限新鮮值。

　　同時(shí)，使用下述策略確定循環(huán)值映射為哪個(gè)Background值：對于每一種數(shù)據(jù)獨(dú)立類型T，定義兩個(gè)不同的Background值TPk和TBu。將所有intruder所知的Foreground值映射為TBk，不知的映射為TBk。

　　通過上述定義和策略研究，描述Manager進(jìn)程如下：

　　其中，T表示數(shù)據(jù)類型，TF代表該數(shù)據(jù)類型的Foreground集合，TBk和TBa分別代表不同的Background值TBk和TBu。

　　為了編譯階段的效率，將其分解為并行結(jié)構(gòu)。因?yàn)閷γ恳粋€(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)閷γ恳粋€(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)啟動新鮮值v的循環(huán)機(jī)制時(shí)，對存儲中含有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ī)器可讀語言，適用于FDR、ProBE等各種工具。一般的程序語言以可執(zhí)行的形式描述算法。CSPM也包含功能程序語言，但是其主要目標(biāo)不同：此處它以自動操作的形式支持并行系統(tǒng)的描述。因此，CSPM腳本通常被定義為一組進(jìn)程而不是程序。作為基礎(chǔ)層，CSPM腳本還支持表達(dá)式和函數(shù)。為了能夠?qū)U(kuò)展后的協(xié)議模型輸入驗(yàn)證工具ProBE并完成驗(yàn)證，需要將擴(kuò)展CSP描述編寫成CSPM腳本(因?yàn)镻roBE編譯接口無法擴(kuò)展)。因此在編寫CSPM腳本過程中定義了相應(yīng)的新事件、新進(jìn)程以實(shí)現(xiàn)擴(kuò)展，最終將手工完成的CSPM腳本輸入工具，完成驗(yàn)證。

　　本文的研究確保了協(xié)議中每個(gè)代理都可以執(zhí)行無限數(shù)量的序列運(yùn)行，解決了有限檢測問題。但是，并行運(yùn)行的代理實(shí)體數(shù)量的無限問題沒有得到解決；如果在模型中沒有發(fā)現(xiàn)攻擊。不能夠證明在更高的并行度不存在攻擊。這也是今后的一個(gè)研究方向。

　　數(shù)據(jù)獨(dú)立技術(shù)可以在一定的協(xié)議范圍內(nèi)使用，不可以直接運(yùn)用在包含時(shí)戳的協(xié)議中。因?yàn)閳?zhí)行的典型操作超出了數(shù)據(jù)獨(dú)立范圍，如使用對比算子xy決定時(shí)戳y是否比時(shí)戳x舊。擴(kuò)展研究處理時(shí)戳可以作為未來的研究方向。