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

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

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

　　為了對Manager進程進行形式化描述，此處定義兩個新的事件：

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

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

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

　　通過上述定義和策略研究，描述Manager進程如下：

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

　　為了編譯階段的效率，將其分解為并行結構。因為對每一個新鮮值的控制都是獨立的。在Yahalom協(xié)議中，假設定義新鮮Nonce集為{N1，N2}，新鮮SessionKey集為{K1}，則可建模為下面的并行結構：

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

　　為了編譯階段的效率，將其分解為并行結構。因為對每一個新鮮值的控制都是獨立的。在Yahalom協(xié)議中，假設定義新鮮Nonce集為{N1，N2}，新鮮SessionKey集為{K1}，則可建模為下面的并行結構：

　　 (3)Intmdez進程

　　擴展Intruder進程，使其與Manager進程一起形成(數(shù)據(jù)獨立類型)新鮮值循環(huán)機制。當啟動新鮮值v的循環(huán)機制時，對存儲中含有v的所有信息進行操作，將v的所有實例替換為Background值b。

　　沿用在Manager進程中的定義和研究，Intruder進程描述如下：

　　4 數(shù)據(jù)獨立技術在CSP協(xié)議模型中的實現(xiàn)
　　
　　CSPM是CSP的機器可讀語言，適用于FDR、ProBE等各種工具。一般的程序語言以可執(zhí)行的形式描述算法。CSPM也包含功能程序語言，但是其主要目標不同：此處它以自動操作的形式支持并行系統(tǒng)的描述。因此，CSPM腳本通常被定義為一組進程而不是程序。作為基礎層，CSPM腳本還支持表達式和函數(shù)。為了能夠將擴展后的協(xié)議模型輸入驗證工具ProBE并完成驗證，需要將擴展CSP描述編寫成CSPM腳本(因為ProBE編譯接口無法擴展)。因此在編寫CSPM腳本過程中定義了相應的新事件、新進程以實現(xiàn)擴展，最終將手工完成的CSPM腳本輸入工具，完成驗證。

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

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