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

目錄
前言
第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