非對稱與異步非對稱χ演算的測試等價關系的研究.pdf

1、隨著計算機網(wǎng)絡的發(fā)展，信息安全問題已變得口益重要。信息的安全性已經(jīng)不是僅僅依賴一個好的加密算法就可以得以解決的問題，它需要綜合的安全理論、安全措施和安全技術來保證。其中，安全協(xié)議起著至關重要的作用。然而事與愿違，已有的安全協(xié)議往往被證實并不如它們的設計者所期望的那樣安全，復雜的網(wǎng)絡環(huán)境使得攻擊者可利用安全協(xié)議設計中的缺陷和漏洞來實施各種各樣的攻擊。因此，安全協(xié)議自身的安全性成了網(wǎng)絡安全的關鍵問題之一。 運用有效的手段和工具對協(xié)議

2、進行安全性分析是保證安全協(xié)議的安全性的重要一環(huán)。形式化分析方法是一種重要的安全協(xié)議分析方法。 進程演算是描述交互系統(tǒng)的建模工具，具有強大的描述能力和嚴格的語義，可以很精確地刻劃仂、議的運行過程。利用進程演算對安全仂、議分析時，既可借鑒其作為代數(shù)模型的基本驗證理論和方法，又可使用其作為抽象程序設計語言的程序分析方法。 在進程演算的框架內(nèi)，安全性質(zhì)可用進程之間的等價性描述。更確切地說，如果一個安全協(xié)議進程與對應的特定理想化進

3、程是等價的，那么安全協(xié)議系統(tǒng)將與該特定理想化系統(tǒng)具有相同的安全性質(zhì)。 測試等價關系就是一種常見的等價關系。安全協(xié)議的安全屬性很自然地可以被描述成特定進程項之間的測試等價關系。而非對稱和異步非對稱χ演算的測試等價關系便是本文的主要研究內(nèi)容。 本文的研究成果主要包括以下幾個方而： ·給出了非對稱和異步非對稱χ演算的語法和操作語義。在語法上，使用一組算子定義非對稱和異步非對稱)C演算的進程；在操作語義上，采用標號轉(zhuǎn)移系

4、統(tǒng)定義非對稱和異步非對稱χ演算的操作語義。而異步非對稱χ演算強調(diào)異步通信。 ·定義了非對稱和異步非對稱χ-演算的測試等價關系，并給出了測試序。 ·定義了范式，并給出了范式的相關定理。特別給出了任意一個進程都可轉(zhuǎn)換成范式進程的結(jié)論。 ·對現(xiàn)有的移動進程演算(如CCS，π演算)的一般公理和規(guī)則進行改造和移植，專門針對非對稱和異步非對稱χ演算的性質(zhì)構(gòu)造了其他一般公理，從而得到公理化系統(tǒng)。 ·給出了非對稱和異步非