網(wǎng)絡(luò)安全協(xié)議的高效分析系統(tǒng).pdf

1、網(wǎng)絡(luò)安全協(xié)議的安全性是網(wǎng)絡(luò)安全的重要基礎(chǔ)，安全協(xié)議的安全性分析與驗(yàn)證是當(dāng)今計(jì)算機(jī)安全領(lǐng)域中研究的熱點(diǎn)和重大課題。形式化方法是安全協(xié)議分析的主要方法和可靠途徑。目前常用的形式化分析方法有邏輯推證、模型檢測(cè)及定理證明等，其中模型檢測(cè)作為一種提高軟硬件系統(tǒng)，特別是Safety-Critical系統(tǒng)的安全性與可靠性的自動(dòng)分析與驗(yàn)證技術(shù)，以其簡(jiǎn)潔明了和自動(dòng)化程度高而倍受注目。本文圍繞安全協(xié)議形式化分析這一前沿領(lǐng)域，研究基于模型檢測(cè)技術(shù)的安全協(xié)議的

2、自動(dòng)分析與驗(yàn)證技術(shù)，主要工作及成果有： 1.為了能夠便于計(jì)算機(jī)自動(dòng)實(shí)現(xiàn)對(duì)安全協(xié)議的分析，本文作者通過(guò)對(duì)大量的安全協(xié)議實(shí)例進(jìn)行分析與驗(yàn)證，歸納出協(xié)議的通用建模算法和協(xié)議存儲(chǔ)的數(shù)據(jù)結(jié)構(gòu)； 2.擴(kuò)展文獻(xiàn)提出的協(xié)議描述語(yǔ)言PDL(Protocol Description Language)的語(yǔ)義描述能力，使其具有更強(qiáng)的語(yǔ)義描述能力，更具通用性； 3.在對(duì)協(xié)議建模時(shí)采用了原子序列atomic和d_step、偏序規(guī)約、語(yǔ)法重