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

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

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

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

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