摘 要： 在研究Roscoe數據獨立技術" title="數據獨立技術">數據獨立技術的基礎上，引入新的進程擴展CSP協議模型，并以Yahalom協議為例給出了完整的協議模型。隨后對擴展的協議模型進行形式化描述。最后使用腳本語言CSPM對其進行編寫，完成驗證。
關鍵詞： CSP(Communication Sequential Processes) 數據獨立 進程 映射
1996年，Lowe首先使用通信順序進程CSP和模型檢測技術分析NSPK(Needham-Schroeder Public Key)協議，并成功發現了協議中的一個中間人攻擊行為。隨后，Roscoe對CSP和FDR(Failures-Divergence Refinenent)的組合做了進一步研究，認為CSP方法是形式分析安全協議" title="安全協議">安全協議的一條新途徑。事實證明，CSP方法對于安全協議分析" title="協議分析">協議分析及發現安全協議攻擊非常有效。但是類似FDR的模型檢測通常受Nonce、Key等新鮮值大小的限制，而在實際執行中所需的數據值比這大得多。使用數據獨立技術使結點能夠調用無限的新鮮值以保證實例無限序列的運行。本文將研究Roscoe這些理論，對CSP協議模型進行設計與實現" title="設計與實現">設計與實現，從而解決有限檢測的問題。
1 CSP協議模型
在CSP模型中，協議參與者被表示為CSP的進程(process)，消息被表示為事件(event)，進而協議被表示為一個通信順序進程的集合。
CSP協議模型由一些可信的參與者進程和入侵者進程組成，進程并行運行且通過信道交互。以NSPK協議為例。該協議的CSP模型包括兩個代理(初始者a，響應者b)和一個能執行密鑰產生、傳送或認證服務的服務器s，它們之間通過不可信的媒介(入侵者)通信，所以存在四個CSP進程，如圖1所示。
Initiator a的CSP進程描述如下：
2 數據獨立技術
數據獨立技術是本論文的關鍵技術，它起源于Lazic的數據獨立研究。
2.1 一般的數據獨立分析
如果一個進程P對于類型T沒有任何限制，則P對于T類型是數據獨立的。此時，T可以被視為P的參數。
通常，數據獨立分析是為以類型T為參數的驗證問題發現有限閾值。如果對于T的閾值，可以驗證系統成立，則對于所有較大的T值也可以驗證系統成立。這點對于很多問題都是成立的。
安全協議模型中的許多特征都可以被視為數據獨立實體。常見的key、nonce可以作為模型中進程的參數。
對依賴nonce和密鑰(和依賴協議的其他簡單數據對象)惟一性的安全協議進行的閥值計算，主要是發現進程存儲量的閾值，并不能直接解決驗證的局限性，也就不能直接應用于安全協議模型。
2.2 Roscoe的數據獨立技術
上節證明了一般目標的數據獨立結果不適用于安全協議分析。所以Roscoe對這些結果進行推論，發展了數據獨立技術。本節將介紹幾條對課題研究具有重要理論意義的推論。
(1)基本原則
對一般數據獨立分析結果進行推論所基于的基本原則也是證明數據獨立理論最重要的方法。即對進程P的參數類型T應用Collapsing函數Φ建立映射關系，證明映射前P(T)的行為經過函數轉換，是P(Φ(T))行為的子集。
對于安全協議主要研究進程的跡。可以很直觀地發現如果Collapsing函數Φ是單映射的(T的所有成員被映射為不同值)，并應用于進程P的參數類型T上(P對于T數據獨立)，則因為T的所有成員被映射為不同值，所以映射前的行為等價于映射后的行為，如式(1)所示：
traces(P(Φ(T)))={Φ(t)|t∈traces(P(T))} (1)
如果使用的Collapsing函數Φ為非單映射函數，則有可能改變等價測試結果，產生不等式(2)：
traces(P(Φ(T)))
{Φ(t)|t∈traces(P(T))} (2)
該不等式只適用于變量，對于程序中的常量，情況有所不同。因此提出下面兩個條件：
PosConjEqT條件：如果進程P中的每一次等價測試失敗都會引發STOP進程，則稱進程P滿足PosConjEqT條件。
PosConjEqT(Positive Conjunctions of Equality Tests)條件由Lazic提出，該條件可以使變量使用非單映射函數的進程再度滿足等式(1)。
對于常量雖然不能重新滿足等式(1)，但可滿足不等式(3)：
{Φ(t)|t∈traces(P(T))}traces(P(Φ(T))) (3)
協議的某些方面可能并不滿足PosConjEqT條件，如代理進程可能需要執行擁有常量(例如名字)的不等式測試。因此，針對常量集C定義PosConjEqT′C條件如下：
如果進程P對于常量集C滿足下列條件，則稱進程P滿足PosConjEqT′C條件。該條件滿足PosConjEqT條件，但與PosConjEqT條件的不同之處是：對于至少包含常量集C一個成員的等價測試，P可能擁有non-STOP結果。
(2)明確推理系統
協議模型中的代理進程是標準類型進程且易于進行滿足PosConjEqT′C條件的特性檢測。但Intruder進程可以依靠推理系統指定產生或破壞信息的規則，這一特性決定了其更為復雜。
如果推理系統滿足這樣的條件，即對于類型間的任意函數Φ：T1→T2，只要(X，f)是系統產生的適用于類型T1推論，則(Φ(X)，Φ(f))就是適用于T2的推論，進而稱該推理系統與這些類型參數T明確相關。其中要求推理的產生在T上對稱(也就是平等對待T的所有成員)并且對出現在推理左邊的T成員不再具有不等的要求。
從上述定義可以確定這樣的性質：如果在明確推理系統中建立攻擊者，并且攻擊者的初始知識集不包含對于類型T成員(除了常數C)的非等價測試，那么該進程滿足PosConjEqT′C條件(并且因此，整個協議模型滿足網絡其他部分的條件)。
可以看出系統成分是否滿足上述性質對研究至關重要。只有滿足這些條件才能夠在協議分析的CSP模型中構造更為復雜的事件。
(3)Roscoe數據獨立技術的意義
Roscoe在文獻[1]中引入了NM進程，負責產生系統所需的無限新鮮值。那么在以前運行中，一個進程要在每一次輸出通信時產生一個新鮮值v；而現在就會將這次通信變為向該進程輸入v，并且要求其與相應的NM進程同步。
為了滿足新鮮值的惟一性和新鮮性，引入的NM進程需進行下列操作：存儲所有發送的新鮮值，相同的新鮮值只發送一次，不發送屬于攻擊者的新鮮值。顯然這些操作并不滿足PosConjEqT條件。
Roscoe沒有單獨使用NM進程進行無限新鮮值的分發，而是應用數據獨立技術，在NM進程中執行Collapse轉換，通過轉換從有限集生成無限新鮮值。
Roscoe的數據獨立技術提供了這樣的理論基礎：若系統的所有成分滿足PosConjEqT′C條件，則大協議系統中轉換前的全部行為(就系統跡而言)可以用經過映射的相應的有限系統描述" title="系統描述">系統描述。這一技術保證了可以在大協議中應用非單映射轉換，將問題簡化為相應的有限系統。
3 數據獨立技術在CSP協議模型中的設計
數據獨立技術使模型檢測器的證明更加完整，因為它的應用使大協議的建模成為可能。
3.1 協議模型的擴展
為了解決驗證的局限性，需要系統代理能夠在實際類型保持有限的情況下，調用無限的不同的新鮮值。沿用Roscoe的方法，引入Manager進程擴展CSP協議模型。以Yahalom協議為例，擴展后模型如圖2所示。
與以前的協議模型相比，該模型引入了Manager進程。此進程與Intruder進程相互配合以實現新鮮值的循環利用，因此可視為新鮮值的循環機制。可以說，該模型是對Roscoe文獻的一個擴展和細化，可以證明其滿足PosConjEqT′C條件：
(1)進程中的數據類型隨機數Na、Nb和密鑰Kab均為數據獨立類型。
(2)可信代理進程為標準類型進程，滿足PosConjEqT′C條件。
(3)攻擊者進程在明確推理系統中建立，并且其初始知識集不包含對類型T成員(除了常數C)的非等價測試，滿足PosConjEqT′C條件。
因此該系統中轉換前全部行為可以用經過映射的、相應的有限系統描述。也正基于此，可以在無限新鮮值的產生過程中應用非單映射轉換，從而將其簡化為相應的有限過程，以形成完整的形式化描述。
3.2 協議各對象的描述
對于每一個新鮮值引入對應的Manager進程，取消可信代理分發新鮮值的能力，只在單次運行期間存儲新鮮值，并要求其在完成協議一次運行時“遺忘”所有存儲的新鮮值。當新鮮值v不再被可信參與者所知(存儲)時，稱v被“遺忘”。攻擊者能夠存儲在網絡中所見的所有新信息。為了能夠產生無限的新鮮值，可以對攻擊者存儲的新鮮值應用collasping函數，從而啟動所提出的新鮮值循環機制。即當新鮮值v在網絡中被“遺忘”時可以被循環再利用。一旦該值被循環利用，相應的Manager進程可以在網絡中再次將其作為新鮮值使用。
(1)可信進程
在擴展的CSP協議模型中，進程描述如下：
擴展后的描述主要有三處變動：第一，進程被定義為遞歸進程，表示Initiator可以執行無限數量的序列運行；而在之前的模型描述中，進程在SKIP終止。第二，新鮮Nonce NA不再是參數，而是來自集合NonceF(通過定義，進程可以接收該集合中的任意值)；之后將會介紹Manager進程如何終止這些值的產生。第三，添加了close事件表示進程重新開始執行初始狀態。該事件標志著進程一次運行的結束，在新鮮值的循環機制中發揮重要作用。
(2)Manager進程
Manger進程負責利用有限資源向網絡提供無限的新鮮值。需要為每一種數據獨立類型分別定義一個Manager進程，在上述的Yahalom協議中需要定義一個管理Nonce類型值的Manager進程——Nonce Manager和一個管理SessionKey類型值的Manager進程——SessionKey Manager。本節研究Manager進程的CSP設計和實現。
將協議中的每一種數據獨立類型T所擁有的值分為兩類集合。第一類集合稱為Foreground值，這些值被網絡視為新鮮值。第二類集合由Background值組成，表示類型T舊的或靜態的值。當循環利用Intruder存儲的新鮮值時，將使用這一集合進行映射。
可以說Manager進程是建模過程中的人造產物，并不代表實際對象而只代表了對于新鮮值的某種操作，主要完成觸發“遺忘”值的循環和分發新鮮值的功能。
為了對Manager進程進行形式化描述，此處定義兩個新的事件：
①ifclose.(v)：表示最后一個存儲v的進程是否已經“遺忘”了v，如果“遺忘”為true，否則為false。
②replace.(v，b)：表示對intruder存儲中含有v的所有信息進行操作，將v的所有實例替換為Background值b，即完成Collapse函數的非單映射。在相對意義上，v又會被視為新鮮，即實現了有限值產生無限新鮮值。
同時，使用下述策略確定循環值映射為哪個Background值：對于每一種數據獨立類型T，定義兩個不同的Background值TBk和TBu。將所有intruder所知的Foreground值映射為TBk，不知的映射為TBk。
通過上述定義和策略研究，描述Manager進程如下：
(3)Intruder進程
擴展Intruder進程，使其與Manager進程一起形成(數據獨立類型)新鮮值循環機制。當啟動新鮮值v的循環機制時，對存儲中含有v的所有信息進行操作，將v的所有實例替換為Background值b。
沿用在Manager進程中的定義和研究，Intruder進程描述如下：
4 數據獨立技術在CSP協議模型中的實現
CSPM是CSP的機器可讀語言，適用于FDR、ProBE等各種工具。一般的程序語言以可執行的形式描述算法。CSPM也包含功能程序語言，但是其主要目標不同：此處它以自動操作的形式支持并行系統的描述。因此，CSPM腳本通常被定義為一組進程而不是程序。作為基礎層，CSPM腳本還支持表達式和函數。為了能夠將擴展后的協議模型輸入驗證工具ProBE并完成驗證，需要將擴展CSP描述編寫成CSPM腳本(因為ProBE編譯接口無法擴展)。因此在編寫CSPM腳本過程中定義了相應的新事件、新進程以實現擴展，最終將手工完成的CSPM腳本輸入工具，完成驗證。
本文的研究確保了協議中每個代理都可以執行無限數量的序列運行，解決了有限檢測問題。但是，并行運行的代理實體數量的無限問題沒有得到解決；如果在模型中沒有發現攻擊，不能夠證明在更高的并行度不存在攻擊。這也是今后的一個研究方向。
數據獨立技術可以在一定的協議范圍內使用，不可以直接運用在包含時戳的協議中。因為執行的典型操作超出了數據獨立范圍，如使用對比算子x
1 Roscoe A W.Proving security protocols with model checkers by data independence techniques.In 11th IEEE Computer Security Foundations Workshop.IEEE Computer Society Press，1998
2 Lazic R S.A semantic study of data-independence with applications to the mechanical verification of concurrent systems.D.Phil.Thesis，University of Oxford，1999
3 Failures-Divergence Refinement—FDR2 User Manual.Formal Systems(Europe)Ltd.http：//www.fsel.com/，2003
4 Lazic R S，Roscoe A W.Verifying determinism of data- in-dependence systems with labellings，arrays and constants.Submitted for publication，1998