-
>
全國計算機等級考試最新真考題庫模擬考場及詳解·二級MSOffice高級應用
-
>
決戰行測5000題(言語理解與表達)
-
>
軟件性能測試.分析與調優實踐之路
-
>
第一行代碼Android
-
>
JAVA持續交付
-
>
EXCEL最強教科書(完全版)(全彩印刷)
-
>
深度學習
經典譯叢·網絡空間安全安全協議操作語義與驗證/(瑞士)CAS CREMERS 版權信息
- ISBN:9787121351952
- 條形碼:9787121351952 ; 978-7-121-35195-2
- 裝幀:一般膠版紙
- 冊數:暫無
- 重量:暫無
- 所屬分類:>
經典譯叢·網絡空間安全安全協議操作語義與驗證/(瑞士)CAS CREMERS 本書特色
適讀人群 :本書可作為高等院校信息安全、計算機和通信等專業的教學參考書,也可供從事相關專業的教學、科研和工程技術人員參考。 安全工程師用高強度的密碼算法設計出一個協議后,并不能保證通信協議的安全性。傳統的安全分析依賴于設計者的經驗和手工分析,這種做法在實踐中已經被證明很難完全檢測出系統的各種隱藏漏洞。協議運行環境的改變、安全假設的改變,都可能導致新的攻擊。 本書涵蓋從安全協議驗證的基礎理論到代碼的實現,不僅為協議構建了牢固的數學形式化基礎,進而精確地定義了協議的運行規范和安全屬性,還設計了高效的驗證算法。
經典譯叢·網絡空間安全安全協議操作語義與驗證/(瑞士)CAS CREMERS 內容簡介
安全協議作為信息安全的重要基礎之一,其安全屬性能否達到設計者的初始目標成為一個重要研究內容,關系到依賴于協議的上層應用系統的安全性。本書的內容主要涵蓋兩部分:用形式化的語義定義協議的執行規格和安全屬性,準確表示安全協議的安全屬性;綜合運用各種形式化方法設計一個高效的驗證算法,在可接受的時間內驗證安全屬性。本書還探討了多協議安全分析,比較分析了各種驗證理論和發展趨勢。
經典譯叢·網絡空間安全安全協議操作語義與驗證/(瑞士)CAS CREMERS 目錄
目 錄
第1章 背景介紹 1
1.1 歷史背景 1
1.2 基于黑盒的安全協議分析 3
1.3 目的與方法 5
1.4 概要 5
1.4.1 協議分析模型 6
1.4.2 模型的應用 6
第2章 預備知識 7
2.1 集合與關系 7
2.2 巴科斯范式 8
2.3 符號變遷系統 8
第3章 操作語義 10
3.1 問題域分析 10
3.2 安全協議規范 13
3.2.1 角色項 14
3.2.2 協議規范 16
3.2.3 事件次序 18
3.3 協議執行描繪 20
3.3.1 回合 20
3.3.2 匹配 21
3.3.3 回合事件 23
3.3.4 威脅模型 24
3.4 操作語義 25
3.5 協議規范實例 27
3.6 思考題 28
第4章 安全屬性 29
4.1 安全斷言事件屬性 29
4.2 機密性 30
4.3 認證 32
4.3.1 存活性 32
4.3.2 同步一致性 35
4.3.3 非單射同步一致性 37
4.3.4 單射同步一致性 38
4.3.5 消息一致性 39
4.4 認證繼承關系 41
4.5 對NS協議的攻擊和改進 44
4.6 總結 49
4.7 思考題 50
第5章 驗證 52
5.1 模式 52
5.2 驗證算法 58
5.2.1 良構模式 59
5.2.2 可達模式 59
5.2.3 空模式和冗余模式 60
5.2.4 算法概述 61
5.2.5 模式精煉 62
5.3 搜索空間遍歷實例 66
5.4 使用模式精煉驗證安全屬性 70
5.5 啟發式算法和參數選擇 71
5.5.1 啟發式算法 71
5.5.2 選擇一個合適的回合數 74
5.5.3 性能 75
5.6 驗證單射性 76
5.6.1 單射同步一致性 76
5.6.2 LOOP循環屬性 79
5.6.3 模型假設 82
5.7 更多Scyther分析系統的特性 82
5.8 思考題 84
第6章 多協議攻擊 85
6.1 多協議攻擊概述 86
6.2 實驗 86
6.3 測試結果 87
6.3.1 嚴格類型匹配:無類型缺陷 89
6.3.2 簡單類型匹配:基本類型缺陷 90
6.3.3 無類型匹配:所有類型缺陷 90
6.3.4 攻擊例子 90
6.4 攻擊場景 92
6.4.1 協議更新 92
6.4.2 歧義性身份驗證 94
6.5 預防多協議攻擊 96
6.6 總結 97
6.7 思考題 97
第7章 基于NSL擴展的多方認證 98
7.1 一個多方身份認證協議 98
7.2 安全分析 101
7.2.1 初步檢測 101
7.2.2 正確性證明 102
7.2.3 角色 的隨機數機密性 105
7.2.4 初始化角色 的非單射同步一致性 106
7.2.5 非初始化角色 的隨機數機密性 107
7.2.6 非初始化角色 的非單射同步一致性 107
7.2.7 所有角色的單射同步一致性 108
7.2.8 類型缺陷攻擊 108
7.2.9 消息*小化 108
7.3 模式變體 109
7.4 弱多方認證協議 111
7.5 思考題 112
第8章 歷史背景和進階閱讀 114
8.1 歷史背景 114
8.1.1 模型 114
8.1.2 早期分析工具 114
8.1.3 邏輯 114
8.1.4 驗證工具 115
8.1.5 多協議攻擊 117
8.1.6 復雜度分析 117
8.1.7 符號化模型和計算模型之間的差異 117
8.1.8 消除安全分析和代碼實現之間的差異 118
8.2 可選方法 119
8.2.1 建模框架 119
8.2.2 安全屬性 120
8.2.3 驗證工具 122
參考文獻 125
經典譯叢·網絡空間安全安全協議操作語義與驗證/(瑞士)CAS CREMERS 作者簡介
Cas Cremers 牛津大學信息安全領域正教授。2006 年獲得荷蘭艾恩德霍芬技術大學博士學位;2006 年至 2013 年,在瑞士蘇黎世聯邦理工學院任博士后和高級研究員;2013年開始在牛津大學任教,于2015 年成為正教授。近期他加入了位于德國的CISPA-Helmholtz中心。他擅長各種形式化理論和系統安全驗證與加固,獨立或與其他研究者一起開發了一系列協議驗證系統,在國際上享有盛譽。Sjouke Mauw 博士,工作于盧森堡大學計算機科學與通信研究所。曾與人一起創建了荷蘭埃因霍溫理工大學的計算機安全研究小組,關注安全協議的形式化建模與安全屬性分析。Cas Cremers 牛津大學信息安全領域正教授。2006 年獲得荷蘭艾恩德霍芬科技大學博士學位;2006 年至 2013 年,在瑞士蘇黎世聯邦理工學院任博士后和高級研究員;2013年開始在牛津大學任教,于2015 年成為正教授。近期他加入了位于德國的CISPA-Helmholtz中心。他擅長各種形式化理論和系統安全驗證與加固,獨立或與其他研究者一起開發了一系列協議驗證系統,在國際上享有盛譽。Sjouke Mauw 博士,工作于盧森堡大學計算機科學與通信研究所。曾與人合作創建了荷蘭艾恩德霍芬科技大學的計算機安全研究小組,他關注安全協議的形式化建模與安全屬性分析。
- >
月亮與六便士
- >
【精裝繪本】畫給孩子的中國神話
- >
上帝之肋:男人的真實旅程
- >
朝聞道
- >
羅曼·羅蘭讀書隨筆-精裝
- >
詩經-先民的歌唱
- >
伯納黛特,你要去哪(2021新版)
- >
中國人在烏蘇里邊疆區:歷史與人類學概述