安全協(xié)議操作語(yǔ)義與驗證簡(jiǎn)介，目錄書(shū)摘

安全工程師用高強度的密碼算法設計出一個(gè)協(xié)議后，并不能保證通信協(xié)議的安全性。傳統的安全分析依賴(lài)于設計者的經(jīng)驗和手工分析，這種做法在實(shí)踐中已經(jīng)被證明很難完全檢測出系統的各種隱藏漏洞。協(xié)議運行環(huán)境的改變、安全假設的改變，都可能導致新的攻擊。

本書(shū)涵蓋從安全協(xié)議驗證的基礎理論到代碼的實(shí)現，不僅為協(xié)議構建了牢固的數學(xué)形式化基礎，進(jìn)而精確地定義了協(xié)議的運行規范和安全屬性，還設計了高效的驗證算法。

安全協(xié)議作為信息安全的重要基礎之一，其安全屬性能否達到設計者的初始目標成為一個(gè)重要研究?jì)热?，關(guān)系到依賴(lài)于協(xié)議的上層應用系統的安全性。本書(shū)的內容主要涵蓋兩部分：用形式化的語(yǔ)義定義協(xié)議的執行規格和安全屬性，精確表示安全協(xié)議的安全屬性；綜合運用各種形式化方法設計一個(gè)高效的驗證算法，在可接受的時(shí)間內驗證安全屬性。本書(shū)還探討了多協(xié)議安全分析，比較分析了各種驗證理論和發(fā)展趨勢。

Cas Cremers 牛津大學(xué)信息安全領(lǐng)域正教授。2006 年獲得荷蘭艾恩德霍芬技術(shù)大學(xué)博士學(xué)位；2006 年至 2013 年，在瑞士蘇黎世聯(lián)邦理工學(xué)院任博士后和高級研究員；2013年開(kāi)始在牛津大學(xué)任教，于2015 年成為正教授。近期他加入了位于德國的CISPA-Helmholtz中心。他擅長(cháng)各種形式化理論和系統安全驗證與加固，獨立或與其他研究者一起開(kāi)發(fā)了一系列協(xié)議驗證系統，在國際上享有盛譽(yù)。Sjouke Mauw 博士，工作于盧森堡大學(xué)計算機科學(xué)與通信研究所。曾與人一起創(chuàng )建了荷蘭埃因霍溫理工大學(xué)的計算機安全研究小組，關(guān)注安全協(xié)議的形式化建模與安全屬性分析。

目    錄
第1章  背景介紹 1
1．1  歷史背景 1
1．2  基于黑盒的安全協(xié)議分析 3
1．3  目的與方法 5
1．4  概要 5
1．4．1  協(xié)議分析模型 6
1．4．2  模型的應用 6
第2章  預備知識 7
2．1  集合與關(guān)系 7
2．2  巴科斯范式 8
2．3  符號變遷系統 8
第3章  操作語(yǔ)義 10
3．1  問(wèn)題域分析 10
3．2  安全協(xié)議規范 13
3．2．1  角色項 14
3．2．2  協(xié)議規范 16
3．2．3  事件次序 18
3．3  協(xié)議執行描繪 20
3．3．1  回合 20
3．3．2  匹配 21
3．3．3  回合事件 23
3．3．4  威脅模型 24
3．4  操作語(yǔ)義 25
3．5  協(xié)議規范實(shí)例 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  認證繼承關(guān)系 41
4．5  對NS協(xié)議的攻擊和改進(jìn) 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  搜索空間遍歷實(shí)例 66
5．4  使用模式精煉驗證安全屬性 70
5．5  啟發(fā)式算法和參數選擇 71
5．5．1  啟發(fā)式算法 71
5．5．2  選擇一個(gè)合適的回合數 74
5．5．3  性能 75
5．6  驗證單射性 76
5．6．1  單射同步一致性 76
5．6．2  LOOP循環(huán)屬性 79
5．6．3  模型假設 82
5．7  更多Scyther分析系統的特性 82
5．8  思考題 84
第6章  多協(xié)議攻擊 85
6．1  多協(xié)議攻擊概述 86
6．2  實(shí)驗 86
6．3  測試結果 87
6．3．1  嚴格類(lèi)型匹配：無(wú)類(lèi)型缺陷 89
6．3．2  簡(jiǎn)單類(lèi)型匹配：基本類(lèi)型缺陷 90
6．3．3  無(wú)類(lèi)型匹配：所有類(lèi)型缺陷 90
6．3．4  攻擊例子 90
6．4  攻擊場(chǎng)景 92
6．4．1  協(xié)議更新 92
6．4．2  歧義性身份驗證 94
6．5  預防多協(xié)議攻擊 96
6．6  總結 97
6．7  思考題 97
第7章  基于NSL擴展的多方認證 98
7．1  一個(gè)多方身份認證協(xié)議 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  類(lèi)型缺陷攻擊 108
7．2．9  消息最小化 108
7．3  模式變體 109
7．4  弱多方認證協(xié)議 111
7．5  思考題 112
第8章  歷史背景和進(jìn)階閱讀 114
8．1  歷史背景 114
8．1．1  模型 114
8．1．2  早期分析工具 114
8．1．3  邏輯 114
8．1．4  驗證工具 115
8．1．5  多協(xié)議攻擊 117
8．1．6  復雜度分析 117
8．1．7  符號化模型和計算模型之間的差異 117
8．1．8  消除安全分析和代碼實(shí)現之間的差異 118
8．2  可選方法 119
8．2．1  建?？蚣?119
8．2．2  安全屬性 120
8．2．3  驗證工具 122
參考文獻 125