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

1996年，Lowe首先使用通信順序進程CSP和模型檢測技術分析NSPK(Needham-Schroeder Public Key)協(xié)議，并成功發(fā)現了協(xié)議中的一個中間人攻擊行為。隨后，Roscoe對CSP和FDR(Fallures-Divergence Refinenent)的組合做了進一步研究，認為CSP方法是形式分析安全協(xié)議的一條新途徑。事實證明，CSP方法對于安全協(xié)議分析及發(fā)現安全協(xié)議攻擊非常有效。但是類似FDR的模型檢測通常受NONce、Key等新鮮值大小的限制，而在實際執(zhí)行中所需的數據值比這大得多。使用數據獨立技術使結點能夠調用無限的新鮮值以保證實例無限序列的運行。本文將研究Roscoe這些理論，對CSP協(xié)議模型進行設計與實現，從而解決有限檢測的問題。

　　1 CSP協(xié)議模型
　　
　　在CSP模型中，協(xié)議參與者被表示為CSP的進程(process)，消息被表示為事件(event)，進而協(xié)議被表示為一個通信順序進程的集合。

　　CSP協(xié)議模型由一些可信的參與者進程和入侵者進程組成，進程并行運行且通過信道交互。以NSPK協(xié)議為例。該協(xié)議的CSP模型包括兩個代理(初始者a，響應者b)和一個能執(zhí)行密鑰產生、傳送或認證服務的服務器s，它們之間通過不可信的媒介(入侵者)通信，所以存在四個CSP進程．

　 Initiator a的CSP進程描述如下：

　　響應者b與服務器s也有著相似的描述。
　　
　　攻擊者進程被描述為：

　　2 數據獨立技術

　　數據獨立技術是本論文的關鍵技術．它起源于Lazic的數據獨立研究。

　　2．1 一般的數據獨立分析

　　如果一個進程P對于類型T沒有任何限制，則P對于T類型是數據獨立的。此時，T可以被視為P的參數。

　　通常，數據獨立分析是為以類型T為參數的驗證問題發(fā)現有限閾值。如果對于T的閾值，可以驗證系統(tǒng)成立，則對于所有較大的T值也可以驗證系統(tǒng)成立。這點對于很多問題都是成立的。

　　安全協(xié)議模型中的許多特征都可以被視為數據獨立實體。常見的key、nonce可以作為模型中進程的參數。

　　對依賴nonce和密鑰(和依賴協(xié)議的其他簡單數據對象)惟一性的安全協(xié)議進行的閥值計算，主要是發(fā)現進程存儲量的閾值，并不能直接解決驗證的局限性，也就不能直接應用于安全協(xié)議模型。

　　2．2 Roscoe的數據獨立技術
　　
　　上節(jié)證明了一般目標的數據獨立結果不適用于安全協(xié)議分析。所以Roscoe對這些結果進行推論。發(fā)展了數據獨立技術。本節(jié)將介紹幾條對課題研究具有重要理論意義的推論。

　　(1)基本原則

　　對一般數據獨立分析結果進行推論所基于的基本原則也是證明數據獨立理論最重要的方法。即對進程P的參數類型T應用Conapsint函數φ建立映射關系，證明映射前P(T)的行為經過函數轉換，是P(φ(T))行為的子集。
　　
　　對于安全協(xié)議主要研究進程的跡。可以很直觀地發(fā)現如果Collapsing函數φ是單映射的(T的所有成員被映射為不同值)，并應用于進程P的參數類型T上(P對于T數據獨立)，則因為T的所有成員被映射為不同值，所以映射前的行為等價于映射后的行為，如式(1)所示：

　如果使用的Collapsing函數φ為非單映射函數，則有可能改變等價測試結果，產生不等式(2)：

　　該不等式只適用于變量，對于程序中的常量，情況有所不同。因此提出下面兩個條件：
　　PosConjEqT(Positive Conjunetions of Equality teSTs)條件由Lazic提出，該條件可以使變量使用

　　非單映射函數的進程再度滿足等式(1)。
　　對于常量雖然不能重新滿足等式(1)，但可滿足不等式(3)：

　　協(xié)議的某些方面可能并不滿足PosConjEqT條件，如代理進程可能需要執(zhí)行擁有常量(例如名字)的不等式測試。因此，針對常量集C定義PosConjEqT′c條件如下：
　　
　　如果進程P對于常量集C滿足下列條件，則稱進程P滿足PosConjEqT′c條件。該條件滿足PosConjEqT條件，但與PosConjEqT條件的不同之處是：對于至少包含常量集C一個成員的等價測試，P可能擁有non-STOP結果。