1、計算機和網絡技術的迅猛發(fā)展，導致對計算機系統(tǒng)和開放式的網絡系統(tǒng)的攻擊日益增多。系統(tǒng)和網絡之所以會受到各種各樣的攻擊，究其原因，最根本的是系統(tǒng)和網絡內部存在各種安全缺陷。為此，人們設計了各種各樣的安全策略、安全模型來確保系統(tǒng)的安全性，并使用密碼協(xié)議來保證網絡通信的安全。在這些安全策略應用到系統(tǒng)之前，我們必須驗證它們是否能夠滿足其“聲稱”的安全目標；同樣，我們也要對密碼協(xié)議進行分析，檢驗其是否存在潛在的、未知的安全漏洞。 不管是直接

2、的或間接的機密數據泄露，都可以看作是信息的非法流動，因此可以采用信息流分析的方法，找出系統(tǒng)或網絡中潛在的各種安全問題。信息流分析方法是信息安全領域較為本質的一種方法。 本文首先介紹了非干擾信息流分析的一般方法，即非確定系統(tǒng)中的信息流非干擾分析技術；然后研究了概率系統(tǒng)和安全協(xié)議中的信息流性質，以及這些安全性質的驗證方法：本文的主要創(chuàng)新工作如下： 1．基于非干擾信息流分析的概率系統(tǒng)安全驗證方法實際系統(tǒng)中，攻擊者可以通過對系統(tǒng)

3、行為觀察進行統(tǒng)計，然后根據統(tǒng)計的概率數據構建概率隱蔽通道，導致機密數據的間接泄露。因此，本文在概率配置下研究了系統(tǒng)的安全性。首先本文對非確定系統(tǒng)中的分析工具SPA進行擴展，得到PSPA，用以描述概率系統(tǒng)的行為。本文提出了P_PBNDC性質，并討論了其在動態(tài)概率環(huán)境下的適用性，也給出了其不同語義等價下的特征描述，以及基于展開條件的特征描述。本文在P_PBNDC性質的基礎上，提出了S PBNDC和CP_PBNDC性質，這些都是PBNDC性質

4、的充分條件。本文還給出了這些PBNDC類性質之間的關系。這些分析是很有意義的，因為本文提出的這些概率系統(tǒng)中的信息流安全性質能夠暴露出那些非確定系統(tǒng)信息流安全性質無法暴露出的系統(tǒng)安全缺陷。 2．基于環(huán)境敏感信息流分析的安全協(xié)議驗證方法為了能夠描述安全協(xié)議的行為，我們對SPA進行擴展，形成了CryptoSPA。本文在CryptoSPA的環(huán)境敏感標記轉換系統(tǒng)語義模型下，定義了環(huán)境敏感的路徑等價和弱互擬等價關系，并提出了基于環(huán)境知識的一

5、般組合上不可演繹的性質框架ESGNDC<'α><,△>。在此框架下，討論了NDC<'σ>、BNDC<'σ>以及P_PBNDC<'σ>性質。本文還在ESGNDC<'α><,△>框架下，討論了安全協(xié)議中的機密性，認證性和公平性，并指出了此框架也適合安全協(xié)議的活性分析。 3．通過模型檢查驗證信息流性質BNDC類性質的定義中都有全程量詞，因此驗證一個系統(tǒng)具有這些性質是非常困難的。本文使用部分模型檢查的方法來對BNDC類性質進行驗證。首先