1996年，lowe首先使用通信順序進(jìn)程csp和模型檢測技術(shù)分析nspk(needham-schroeder public key)協(xié)議，并成功發(fā)現(xiàn)了協(xié)議中的一個中間人攻擊行為。隨后，roscoe對csp和fdr(fallures-divergence refinenent)的組合做了進(jìn)一步研究，認(rèn)為csp方法是形式分析安全協(xié)議的一條新途徑。事實證明，csp方法對于安全協(xié)議分析及發(fā)現(xiàn)安全協(xié)議攻擊非常有效。但是類似fdr的模型檢測通常受nonce、key等新鮮值大小的限制，而在實際執(zhí)行中所需的數(shù)據(jù)值比這大得多。使用數(shù)據(jù)獨立技術(shù)使結(jié)點能夠調(diào)用無限的新鮮值以保證實例無限序列的運行。本文將研究roscoe這些理論，對csp協(xié)議模型進(jìn)行設(shè)計與實現(xiàn)，從而解決有限檢測的問題。

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

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

　 initiator a的csp進(jìn)程描述如下：

　　響應(yīng)者b與服務(wù)器s也有著相似的描述。
　　
　　攻擊者進(jìn)程被描述為：

　　2 數(shù)據(jù)獨立技術(shù)

　　數(shù)據(jù)獨立技術(shù)是本論文的關(guān)鍵技術(shù)．它起源于lazic的數(shù)據(jù)獨立研究。

　　2．1 一般的數(shù)據(jù)獨立分析

　　如果一個進(jìn)程p對于類型t沒有任何限制，則p對于t類型是數(shù)據(jù)獨立的。此時，t可以被視為p的參數(shù)。

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

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

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

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

　　(1)基本原則

　　對一般數(shù)據(jù)獨立分析結(jié)果進(jìn)行推論所基于的基本原則也是證明數(shù)據(jù)獨立理論最重要的方法。即對進(jìn)程p的參數(shù)類型t應(yīng)用conapsint函數(shù)φ建立映射關(guān)系，證明映射前p(t)的行為經(jīng)過函數(shù)轉(zhuǎn)換，是p(φ(t))行為的子集。
　　
　　對于安全協(xié)議主要研究進(jìn)程的跡�？梢院苤庇^地發(fā)現(xiàn)如果collapsing函數(shù)φ是單映射的(t的所有成員被映射為不同值)，并應(yīng)用于進(jìn)程p的參數(shù)類型t上(p對于t數(shù)據(jù)獨立)，則因為t的所有成員被映射為不同值，所以映射前的行為等價于映射后的行為，如式(1)所示：

　如果使用的collapsing函數(shù)φ為非單映射函數(shù)，則有可能改變等價測試結(jié)果，產(chǎn)生不等式(2)：

　　該不等式只適用于變量，對于程序中的常量，情況有所不同。因此提出下面兩個條件：
　　posconjeqt(positive conjunetions of equality tests)條件由lazic提出，該條件可以使變量使用

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

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

　　(2)明確推理系統(tǒng)

　　協(xié)議模型中的代理進(jìn)程是標(biāo)準(zhǔn)類型進(jìn)程且易于進(jìn)行