安全協(xié)議及其BAN邏輯分析研究.pdf

1、隨著計算機(jī)網(wǎng)絡(luò)的廣泛應(yīng)用和各種應(yīng)用領(lǐng)域的不斷擴(kuò)大，信息的安全問題成為大家關(guān)注的焦點(diǎn)。信息安全(Information Security)問題從某種程度上已成為制約計算機(jī)網(wǎng)絡(luò)應(yīng)用的一個瓶頸。傳統(tǒng)的對信息的安全性處理是依賴于好的加解密算法來保證。但是，隨著網(wǎng)絡(luò)應(yīng)用的深入，僅僅依賴一個好的加解密算法已經(jīng)不能很好地解決信息的安全問題，它需要安全理論、安全措施和安全技術(shù)來保證。在這些信息安全的理論、措施和技術(shù)中，安全協(xié)議起著至關(guān)重要的作用。在實(shí)際

2、應(yīng)用中，人們需要可信的機(jī)制來為通信的各方進(jìn)行身份認(rèn)證和分發(fā)密鑰，這就迫使人們研究和設(shè)計出了各種安全協(xié)議(Security Protocol)。然而事與愿違，已有的安全協(xié)議往往被證實(shí)并不如它們的設(shè)計者所期望的那樣安全，開放的、復(fù)雜的網(wǎng)絡(luò)環(huán)境使得攻擊者可利用安全協(xié)議設(shè)計中的缺陷和漏洞來實(shí)施各種各樣的攻擊，從而非法獲取網(wǎng)絡(luò)資源，竊取非授權(quán)使用的信息，危及到網(wǎng)絡(luò)的安全和應(yīng)用。因此，安全協(xié)議自身的安全性成了網(wǎng)絡(luò)安全的關(guān)鍵問題之一?？剂亢头治鲆粋€安

3、全協(xié)議的安全性稱為安全協(xié)議的分析。目前，使用最為廣泛的安全協(xié)議分析方法是各種形式化分析方法，即采用各種形式化的語言或模型，為安全協(xié)議建立模型，并按照規(guī)定的假設(shè)、分析和驗(yàn)證規(guī)則，驗(yàn)證安全協(xié)議的安全性。 本文以如何保障安全協(xié)議的安全性為切入點(diǎn)，研究和分析了與安全協(xié)議息息相關(guān)的密碼學(xué)的諸多問題，例如，對稱密碼體制、公鑰密碼體制、橢圓曲線密碼體制、數(shù)字簽名等基本算法。進(jìn)一步討論了具有代表性的認(rèn)證協(xié)議，密鑰管理和分配的方法等。研究和分析了

4、安全協(xié)議的非形式化分析的方法和形式化分析方法，重點(diǎn)是對BAN邏輯的分析和討論，并利用BAN邏輯分析了部分認(rèn)證協(xié)議。 本文通過BAN邏輯的實(shí)例分析，說明了BAN邏輯在分析認(rèn)證協(xié)議中具有積極的作用，發(fā)現(xiàn)了認(rèn)證協(xié)議中一些原來沒有發(fā)現(xiàn)的漏洞和冗余。但是，文中通過對兩個認(rèn)證協(xié)議的分析，指出了BAN邏輯在對中間人攻擊和口令猜測攻擊的安全協(xié)議分析中存在的缺陷，并對被分析的認(rèn)證協(xié)議進(jìn)行了改進(jìn)。最后提出了基于安全協(xié)議的電子公文安全流轉(zhuǎn)方案和基于安