基于串空間模型的安全協(xié)議形式化分析技術(shù)研究.pdf

1、隨著網(wǎng)絡(luò)技術(shù)的發(fā)展，網(wǎng)絡(luò)應(yīng)用己經(jīng)日益滲透到我們生活的方方面面，但網(wǎng)絡(luò)給人們帶來巨大便利的同時也帶來了一些潛伏的不安全因素。作為通信基礎(chǔ)的協(xié)議，承載著網(wǎng)絡(luò)中通信的所有數(shù)據(jù)和信息，擔(dān)當(dāng)著通信方之間的通信橋梁，如何從協(xié)議的角度實(shí)現(xiàn)安全是一個重要而基本的研究課題。使用密碼算法的安全協(xié)議為開放網(wǎng)絡(luò)中的安全通信提供了基本保證，但實(shí)踐證明，即便是一個簡單的協(xié)議，其分析也是不容易的。協(xié)議的分析需要一套嚴(yán)格的形式化方法。 形式化的分析方法是采用各

2、種形式化的語言或者模型，為安全協(xié)議建立模型，并按照規(guī)定的假設(shè)和分析、驗(yàn)證方法證明協(xié)議的安全性。形式化的分析方法是當(dāng)前分析安全協(xié)議領(lǐng)域研究的熱點(diǎn)。近幾年來，密碼學(xué)家提出了許多關(guān)于安全協(xié)議的形式化分析方法，以檢驗(yàn)協(xié)議中是否存在安全缺陷。 串空間模型是一種著名的安全協(xié)議形式化模型，它的提出本身體現(xiàn)了協(xié)議形式化分析領(lǐng)域的發(fā)展方向，它結(jié)合了多種形式化方法的思想和技術(shù)，而且串空間理論是定理證明方法，可以手動的完成證明，得到可信的結(jié)果。該理論

3、簡潔易用，而且基于圖論對協(xié)議進(jìn)行描述，可以使用圖形表示在協(xié)議證明中提供輔助說明。從串空間模型提出到現(xiàn)在，已經(jīng)有研究者利用它發(fā)現(xiàn)了一些協(xié)議的漏洞，也有不少研究者利用它設(shè)計出了新型的安全協(xié)議自動分析工具?？梢姡@是一種很有研究前景的形式化模型。 但是基本的串空間理論只能分析簡單的使用連接、加密操作的安全協(xié)議，且對攻擊者的能力描述有限，大大限制了其可分析的協(xié)議的范圍。隨著二十世紀(jì)七十年代以來，各種密碼算法已經(jīng)大量應(yīng)用于安全協(xié)議中，如簽

4、名、散列函數(shù)等。為了能夠分析更多類型的數(shù)據(jù)類型和操作，我們對串空間理論進(jìn)行了擴(kuò)展和完善。 本文的主要工作有以下幾個方面： ·原理性闡述了幾個具有代表性的安全協(xié)議形式化分析技術(shù)，其中詳細(xì)闡述了串空間理論的定義、分析協(xié)議的方法和原理。 ·從語義上研究串空間模型，針對BAN邏輯語義不明確的問題，給出了基于串空間模型的邏輯的語義表示，并對BAN邏輯進(jìn)行擴(kuò)展，重新定義了BAN邏輯的協(xié)議分析過程。 ·介紹了串空間理論