數據獨立技術在CSP協議模型中的設計

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

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

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

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

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

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

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

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

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

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

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

　　 (3)Intmdez進程

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

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

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

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

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