安全協(xié)議形式化自動驗證工具AVISPA的研究
發(fā)布時間:2021-02-20 10:00
近年來,網(wǎng)絡技術的飛速發(fā)展給人類帶來眾多便利的同時也存在著越來越多的網(wǎng)絡信息安全問題。據(jù)統(tǒng)計,到2010年為止,我國網(wǎng)民總數(shù)超過4.2億,但具有獨立網(wǎng)絡安全意識的網(wǎng)民不到40%。2012年我國電子商務交易金額有望突破8萬億元,網(wǎng)絡購物金額超過4000億元。2013年美國提交的2014年國防預算草案中,網(wǎng)絡安全經(jīng)費大幅增至47億,用來攔截來自他國的網(wǎng)絡攻擊。網(wǎng)絡信息安全不僅關系著個人信息安全還關系著國家安全。為了保證網(wǎng)絡信息安全,用建立在復雜密碼體系基礎上的安全協(xié)議擔任網(wǎng)絡中的重要通信協(xié)議。這些安全的通信協(xié)議被應用于廣泛的計算機網(wǎng)絡和分布式系統(tǒng)中,已經(jīng)成為電子商務和計算機通信的一個重要環(huán)節(jié)。但是,雖然這些安全協(xié)議使用了加密算法,但不能保證網(wǎng)絡一直處于安全狀態(tài),只要黑客找到適當?shù)墓ぞ,該網(wǎng)絡安全協(xié)議很快就被攻破,信息很容易被竊取,篡改等受到惡意的破壞。通常采用攻擊檢驗方法和形式化分析方法確保安全協(xié)議的安全性。攻擊檢驗方法是基于已知的各種攻擊對安全協(xié)議進行分析,分析前必須已知各種攻擊,但在實際應用中大多數(shù)攻擊在分析前是不可知的。另一種安全協(xié)議分析方法形式化分析在分析前不需要已知攻擊,因此形式...
【文章來源】:吉林大學吉林省 211工程院校 985工程院校 教育部直屬院校
【文章頁數(shù)】:47 頁
【學位級別】:碩士
【部分圖文】:
丫ahalom協(xié)議交互過程圖
26圖 4-2 Yahalom 協(xié)議的協(xié)議模擬4.2.3 Yahalom 協(xié)議的攻擊模擬運行 AVISPA 安全協(xié)議自動化驗證工具對 Yahalom.hlpsl 分析驗證,其中Yahalom.hlpsl,是上述的協(xié)議描述文件。通過 OFMC 分析終端對 Yahalom 協(xié)議的分析,得出了此協(xié)議是不安全的結論并給出攻擊的軌跡如圖 4-3 所示:
27圖 4-3 結論及攻擊軌跡攻擊軌跡:1. i -> (b,3): a.x2532. (b,3) -> i: b.{a.x253.Nb(1)}_kbs3. i -> (s,3): b.{a.x253.Nb(1)}_kbs4. (s,3) -> i: {b.Kab(2).x253.Nb(1)}_kas.{a.Kab(2)}_kbs5. i -> (s,7): b.{a.x253.Nb(1)}_kbs6. (s,7) -> i: {b.Kab(3).x253.Nb(1)}_kas.{a.Kab(3)}_kbs攻擊者 Intruder 最先冒充 B 為 I(B),接收原本 A 發(fā)給 B 的消息,導致 B 接收不到需要消息,然后攻擊者又冒充 B 把從 A 獲得的消息發(fā)送給 S。在整個過程
【參考文獻】:
期刊論文
[1]安全協(xié)議形式化分析的研究和實現(xiàn)[J]. 徐夢茗,肖聰,李斌,杜彪. 信息安全與通信保密. 2008(08)
[2]Efficient Protocol-Proving Algorithm Based on Improved Authentication Tests[J]. 李謝華,楊樹堂,李建華,諸鴻文. Journal of Shanghai Jiaotong University. 2007(01)
[3]安全協(xié)議和網(wǎng)絡攻擊分析[J]. 徐夢茗,肖聰,唐六華,黃金濤. 信息安全與通信保密. 2007(02)
[4]串空間理論在網(wǎng)絡安全協(xié)議形式化分析中應用[J]. 孫海波,林東岱,黃寄洪. 大連理工大學學報. 2003(S1)
[5]安全協(xié)議形式化分析理論與方法研究綜述[J]. 馮登國,范紅. 中國科學院研究生院學報. 2003(04)
[6]基于串空間的安全協(xié)議形式化驗證模型及算法[J]. 周宏斌,黃連生,桑田. 計算機研究與發(fā)展. 2003(02)
[7]認證協(xié)議的一些新攻擊方法[J]. 王貴林,卿斯?jié)h,周展飛. 軟件學報. 2001(06)
博士論文
[1]安全協(xié)議代數(shù)證明方法研究[D]. 李援.合肥工業(yè)大學 2007
碩士論文
[1]密碼協(xié)議符號分析方法的計算可靠性研究[D]. 朱玉娜.解放軍信息工程大學 2008
[2]無線傳感器網(wǎng)絡安全定向擴散路由協(xié)議研究[D]. 趙浩浩.武漢理工大學 2008
本文編號:3042608
【文章來源】:吉林大學吉林省 211工程院校 985工程院校 教育部直屬院校
【文章頁數(shù)】:47 頁
【學位級別】:碩士
【部分圖文】:
丫ahalom協(xié)議交互過程圖
26圖 4-2 Yahalom 協(xié)議的協(xié)議模擬4.2.3 Yahalom 協(xié)議的攻擊模擬運行 AVISPA 安全協(xié)議自動化驗證工具對 Yahalom.hlpsl 分析驗證,其中Yahalom.hlpsl,是上述的協(xié)議描述文件。通過 OFMC 分析終端對 Yahalom 協(xié)議的分析,得出了此協(xié)議是不安全的結論并給出攻擊的軌跡如圖 4-3 所示:
27圖 4-3 結論及攻擊軌跡攻擊軌跡:1. i -> (b,3): a.x2532. (b,3) -> i: b.{a.x253.Nb(1)}_kbs3. i -> (s,3): b.{a.x253.Nb(1)}_kbs4. (s,3) -> i: {b.Kab(2).x253.Nb(1)}_kas.{a.Kab(2)}_kbs5. i -> (s,7): b.{a.x253.Nb(1)}_kbs6. (s,7) -> i: {b.Kab(3).x253.Nb(1)}_kas.{a.Kab(3)}_kbs攻擊者 Intruder 最先冒充 B 為 I(B),接收原本 A 發(fā)給 B 的消息,導致 B 接收不到需要消息,然后攻擊者又冒充 B 把從 A 獲得的消息發(fā)送給 S。在整個過程
【參考文獻】:
期刊論文
[1]安全協(xié)議形式化分析的研究和實現(xiàn)[J]. 徐夢茗,肖聰,李斌,杜彪. 信息安全與通信保密. 2008(08)
[2]Efficient Protocol-Proving Algorithm Based on Improved Authentication Tests[J]. 李謝華,楊樹堂,李建華,諸鴻文. Journal of Shanghai Jiaotong University. 2007(01)
[3]安全協(xié)議和網(wǎng)絡攻擊分析[J]. 徐夢茗,肖聰,唐六華,黃金濤. 信息安全與通信保密. 2007(02)
[4]串空間理論在網(wǎng)絡安全協(xié)議形式化分析中應用[J]. 孫海波,林東岱,黃寄洪. 大連理工大學學報. 2003(S1)
[5]安全協(xié)議形式化分析理論與方法研究綜述[J]. 馮登國,范紅. 中國科學院研究生院學報. 2003(04)
[6]基于串空間的安全協(xié)議形式化驗證模型及算法[J]. 周宏斌,黃連生,桑田. 計算機研究與發(fā)展. 2003(02)
[7]認證協(xié)議的一些新攻擊方法[J]. 王貴林,卿斯?jié)h,周展飛. 軟件學報. 2001(06)
博士論文
[1]安全協(xié)議代數(shù)證明方法研究[D]. 李援.合肥工業(yè)大學 2007
碩士論文
[1]密碼協(xié)議符號分析方法的計算可靠性研究[D]. 朱玉娜.解放軍信息工程大學 2008
[2]無線傳感器網(wǎng)絡安全定向擴散路由協(xié)議研究[D]. 趙浩浩.武漢理工大學 2008
本文編號:3042608
本文鏈接:http://sikaile.net/guanlilunwen/ydhl/3042608.html
最近更新
教材專著