安全協議形式化分析與驗證

肖美華

買這商品的人也買了...

相關主題

商品描述

《安全協議形式化分析與驗證》是作者多年從事安全協議形式化分析與驗證相關科研工作的總結,
主要對兩種形式化方法做了歸納:基於SPIN工具的模型檢測和事件邏輯。
《安全協議形式化分析與驗證》主要內容如下:介紹了安全協議形式化分析的研究現狀、主要技術流派,
以及協議描述語言ProDL,闡述了基於算法知識邏輯的網絡安全協議模型檢測分析方法,
用於顯式地刻畫入侵者模型能力;在網絡安全協議驗證模型生成系統中,採用偏序歸約、
語法重定序以及靜態分析等優化策略,有效緩解模型檢測過程中狀態爆炸問題;
對事件邏輯進行擴展,提出一系列規則,對安全協議進行形式化描述,
無需顯性刻畫入侵者模型,只需分析協議動作之間的匹配順序關係即可對協議的安全性進行證明。

目錄大綱

目錄
前言
第1章緒論1
1.1安全協議形式化分析背景1
1.2安全協議形式化分析研究現狀3
參考文獻6

第2章形式化方法基本理論10
2.1形式化方法概述10
2.2模態邏輯11
2.2.1 BAN邏輯11
2.2.2 BAN類邏輯14
2.2.3 Kailar邏輯15
2.3模型檢測15
2.3.1 FDR 16
2.3.2 NRL協議分析器19
2.3.3 Murφ 21
2.3.4 SPIN 23
2.4定理證明26
2.4.1 Paulson歸納法27
2.4.2串空間模型28
2.4.3 Spi演算證明方法29
2.4.4 PCL證明方法30
2.4.5事件邏輯證明方法33
2.5比較與分析35
參考文獻36

第3章安全協議39
3.1安全協議概念39
3.2安全協議分類40
3.2.1 ISO/IEC 11770-2密鑰建立機制6協議40
3.2.2 NSSK協議41
3.2.3 Kerberos認證協議42
3.2.4 ISO/IEC 9798-3協議44
3.2.5 NSPK協議44
3.3協議安全屬性45
3.4協議安全構建方法46
3.4.1 Hash函數48
3.4.2隨機數49
3.4.3時間戳50
3.5協議攻擊者模型及其攻擊類型51
3.5.1 Dolev-Yao攻擊者模型52
3.5.2攻擊類型53
參考文獻53

第4章基於模型檢測的安全協議分析55
4.1安全協議形式化表示55
4.1.1原子消息(基本約定) 55
4.1.2消息55
4.1.3動作56
4.1.4協議57
4.1.5跡57
4.2消息生成規則58
4.3基於算法知識邏輯的協議形式化分析61
4.3.1多智體系統62
4.3.2算法知識邏輯62
4.3.3算法知識邏輯分析協議64
4.4時態邏輯69
4.4.1 Kripke結構70
4.4.2 CTL*、CTL和LTL 70
4.4.3並發系統性質描述72
4.4.4實例73
4.5形式化分析流程74
4.5.1形式化建模75
4.5.2協議安全性質刻畫79
4.5.3形式化驗證79
4.6驗證模型優化策略79
4.6.1靜態分析79
4.6.2語法重定序84
4.6.3偏序歸約84
4.6.4優化策略對比87
4.7與其他方法對比88
4.7.1與認證邏輯對比89
4.7.2與FDR對比91
4.7.3與Murφ對比93
4.7.4與NRL協議分析器對比95
4.7.5與Athena對比97
4.7.6與Isabelle對比100
4.7.7與BRUTUS對比101
參考文獻103

第5章網絡安全協議驗證模型生成系統108
5.1系統概述108
5.1.1系統簡介108
5.1.2系統功能110
5.2系統設計與實現112
5.2.1整體設計112
5.2.2模塊設計112
5.2.3協議描述語言ProDL 124
5.2.4 Needham-Schroeder公開密鑰協議分析與驗證130
5.2.5 BAN-Yahalom三方對稱密鑰認證協議分析與驗證132
5.2.6 CMP1可信第三方電子商務協議分析與驗證133
參考文獻135

第6章基於事件邏輯的安全協議形式化分析137
6.1事件系統137
6.1.1符號說明137
6.1.2消息自動機138
6.1.3語法語義139
6.1.4不可猜測的原子140
6.1.5事件結構140
6.1.6事件類142
6.2事件邏輯公理、推論及性質143
6.2.1事件邏輯公理143
6.2.2事件邏輯推論及性質146
6.3事件邏輯形式化描述協議147
6.4基於事件邏輯的安全協議證明150
6.4. 1推理規則150
6.4.2兩方安全協議證明流程151
6.4.3三方安全協議證明流程153
6.5與其他典型證明方法對比154
6.5.1 PCL 154
6.5.2 BAN類邏輯155
6.5.3串空間理論155
參考文獻156

第7章總結與展望158
7.1研究成果總結158
7.2下一步研究工作159