網(wǎng)絡(luò)安全協(xié)議的形式化分析與驗(yàn)證

定　價(jià)：￥27.00

作　者：	李建華等著
出版社：	機(jī)械工業(yè)出版社
叢編項(xiàng)：
標(biāo)　簽：	信息安全

購(gòu)買(mǎi)這本書(shū)可以去

ISBN：	9787111297260	出版時(shí)間：	2010-04-01	包裝：	平裝
開(kāi)本：	16開(kāi)	頁(yè)數(shù)：	214	字?jǐn)?shù)：

內(nèi)容簡(jiǎn)介

　　《網(wǎng)絡(luò)安全協(xié)議的形式化分析與驗(yàn)證》概述了形式化技術(shù)在網(wǎng)絡(luò)安全協(xié)議分析、驗(yàn)證中的主要應(yīng)用原理及現(xiàn)狀；在此基礎(chǔ)上詳細(xì)地?cái)⑹隽司W(wǎng)絡(luò)安全協(xié)議的形式化分析技術(shù)、形式化設(shè)計(jì)技術(shù);最后重點(diǎn)介紹了目前的形式化分析技術(shù)對(duì)當(dāng)前典型應(yīng)用環(huán)境下復(fù)雜、實(shí)用網(wǎng)絡(luò)安全協(xié)議的分析成果，包括IPSec協(xié)議、SSL協(xié)議、電子商務(wù)協(xié)議、移動(dòng)通信安全協(xié)議及群組通信安全協(xié)議等。信息安全是關(guān)系到國(guó)家安全和經(jīng)濟(jì)發(fā)展的重大戰(zhàn)略問(wèn)題，至關(guān)重要。安全協(xié)議作為實(shí)現(xiàn)信息安全的基礎(chǔ)，其自身的安全性問(wèn)題已成為安全研究的重要內(nèi)容。目前，針對(duì)安全協(xié)議的安全性驗(yàn)證已形成了許多不同的流派、理論和方法。《網(wǎng)絡(luò)安全協(xié)議的形式化分析與驗(yàn)證》理論與應(yīng)用并重，深入淺出地介紹了各類(lèi)形式化分析技術(shù)的基本原理及其在大型復(fù)雜安全協(xié)議分析中的實(shí)際應(yīng)用。《網(wǎng)絡(luò)安全協(xié)議的形式化分析與驗(yàn)證》可作為信息安全專(zhuān)業(yè)高年級(jí)本科生教材，也可作為高等學(xué)校電子信息類(lèi)、計(jì)算機(jī)類(lèi)等相關(guān)專(zhuān)業(yè)的參考書(shū)。

作者簡(jiǎn)介

暫缺《網(wǎng)絡(luò)安全協(xié)議的形式化分析與驗(yàn)證》作者簡(jiǎn)介

圖書(shū)目錄

前言
第1章緒論
1.1 安全協(xié)議概述
1.1.1 安全協(xié)議的基本概念
1.1.2 安全協(xié)議的缺陷分析
1.1.3 安全協(xié)議的攻擊手段
1.1.4 安全協(xié)議形式化方法的必要性
1.2 形式化技術(shù)基礎(chǔ)
1.2.1 模態(tài)邏輯技術(shù)
1.2.2 模型檢測(cè)技術(shù)
1.2.3 定理證明技術(shù)
1.3 形式化方法在安全協(xié)議驗(yàn)證中的應(yīng)用
1.3.1 安全協(xié)議形式化理論發(fā)展現(xiàn)狀
1.3.2 安全協(xié)議形式化方法發(fā)展趨勢(shì)
1.4 本章小結(jié)
1.5 習(xí)題
第2章基于模態(tài)邏輯技術(shù)的安全協(xié)議分析方法
2.1 BAN邏輯
2.1.1 基本術(shù)語(yǔ)
2.1.2 推理規(guī)則
2.1.3 應(yīng)用實(shí)例
2.2 類(lèi)BAN邏輯
2.2.1 GNY邏輯
2.2.2 AT邏輯
2.2.3 SVO邏輯
2.2.4 Kailar邏輯
2.3 Bieber邏輯
2.3.1 歷史模型
2.3.2 KT5邏輯
2.3.3 CKT5通信邏輯
2.3.4 消息的解釋
2.3.5 認(rèn)證與保密
2.4 非單調(diào)邏輯
2.4.1 安全協(xié)議的Nonmonotomic邏輯描述
2.4.2 安全協(xié)議的Nonmonotomic邏輯分析
2.5 本章小結(jié)
2.6 習(xí)題
第3章基于模型檢測(cè)技術(shù)的安全協(xié)議分析方法
3.1 Dolev Yao模型
3.2 通信進(jìn)程方法
3.2.1 CSP的基本概念
3.2.2 CSP的網(wǎng)絡(luò)模型
3.2.3 協(xié)議安全性質(zhì)的CSP描述
3.2.4 CSP協(xié)議分析
3.3 NRL協(xié)議分析器
3.3.1 協(xié)議描述
3.3.2 協(xié)議分析
3.3.3 實(shí)例
3.4 模型檢測(cè)工具M(jìn)ur
3.4.1 Mur系統(tǒng)
3.4.2 Mur協(xié)議分析過(guò)程
3.4.3 Mur協(xié)議分析實(shí)例
3.5 模型檢測(cè)工具ASTRAL
3.6 協(xié)議分析工具BRUTUS
3.6.1 BRUTUS協(xié)議描述模型
3.6.2 BRUTUS協(xié)議屬性邏輯
3.6.3 BRUTUS協(xié)議驗(yàn)證算法
3.6.4.BRUTUS協(xié)議分析實(shí)例
3.7 本章小結(jié)
3.8 習(xí)題
第4章基于定理證明的安全協(xié)議分析方法
4.1 Paulson歸納法
4.1.1 Paulson歸納法簡(jiǎn)介
4.1.2 Paulson歸納法的自動(dòng)化理論
4.1.3 Paulson歸納法協(xié)議分析示例
4.2 Schneider階函數(shù)
4.2.1 階函數(shù)的定義
4.2.2 階函數(shù)定理
4.2.3 協(xié)議分析實(shí)例
4.2.4 基于階函數(shù)的自動(dòng)化驗(yàn)證技術(shù)
4.3 串空間
4.3.1 基本概念
4.3.2 協(xié)議入侵者描述
4.3.3 安全屬性的表示
4.3.4 協(xié)議分析舉例
4.3.5 認(rèn)證測(cè)試方法
4.4 重寫(xiě)逼近法
4.4.1 預(yù)備知識(shí)
4.4.2 逼近技術(shù)
4.4.3 對(duì)NS公鑰協(xié)議的描述與分析
4.5 不變式產(chǎn)生技術(shù)
4.5.1 基本概念
4.5.2 描述攻擊者不可知項(xiàng)集合的不變式
4.5.3 描述攻擊者可知項(xiàng)集合的不變式
4.6 本章小結(jié)
4.7 習(xí)題
第5章安全協(xié)議的形式化設(shè)計(jì)方法
5.1 合成協(xié)議模型及其安全性
5.1.1 HT模型
5.1.2 協(xié)議的組合
5.2 Fail-Stop協(xié)議
5.2.1 Fail-Stop協(xié)議及其分析
5.2.2 復(fù)雜協(xié)議
5.3 BSW簡(jiǎn)單邏輯
5.3.1 模型
5.3.2 邏輯
5.4 本章小結(jié)
5.5 習(xí)題
第6章 Internet密鑰交換協(xié)議及其分析
6.1 Internet密鑰交換協(xié)議概述
6.1.1 階段1主模式交換
6.1.2 階段1野蠻模式交換
6.1.3 階段2快速模式交換
6.2 IKE三協(xié)議的形式化分析
6.2.1 采用NRL協(xié)議分析器進(jìn)行形式化分析
6.2.2 利用擴(kuò)展BSW邏輯分析
6.3 IKEV2協(xié)議概述
6.3.1 IKEV2密鑰交換
6.3.2 密鑰算法協(xié)商
6.3.3 加密密鑰與認(rèn)證密鑰
6.4 IKEV2協(xié)議的形式化分析
6.4.1 擴(kuò)展串空間理論
6.4.2 IKEV2協(xié)議分析
6.5 本章小結(jié)
6.6 習(xí)題
第7章電子商務(wù)安全協(xié)議及其分析
7.1 早期的電子商務(wù)安全協(xié)議
7.1.1 Digicash協(xié)議
7.1.2 First Virtual協(xié)議
7.1.3 Netbill協(xié)議
7.2 SSL協(xié)議及其分析
7.2.1 SSL協(xié)議介紹
7.2.2 SSL協(xié)議的形式化分析
7.3 SET協(xié)議及其分析
7.3.1 SET協(xié)議的流程
7.3.2 雙重簽名技術(shù)
7.3.3 數(shù)字信封v
7.3.4 SEL協(xié)議的形式化分析
7.4 本章小結(jié)
7.5 習(xí)題
第8章移動(dòng)通信安全協(xié)議及其分析
8.1 移動(dòng)通信安全協(xié)議
8.1.1 第1代移動(dòng)通信安全協(xié)議
8.1.2 第2代移動(dòng)通信安全協(xié)議
8.1.3 第3代移動(dòng)通信安全協(xié)議
8.2 AUTLOG認(rèn)證邏輯對(duì)AKA協(xié)議的分析
8.2.1 AUTLOG認(rèn)證邏輯
8.2.2 協(xié)議的形式化描述
8.2.3 假設(shè)前提
8.2.4 協(xié)議目標(biāo)
8.2.5 形式化證明
8.3 利用認(rèn)證測(cè)試方法對(duì)3GPP-AKA，協(xié)議進(jìn)行安全性分析
8.3.1 移動(dòng)用戶與移動(dòng)核心網(wǎng)之間的安全性驗(yàn)證
8.3.2 服務(wù)網(wǎng)絡(luò)基站與移動(dòng)核心網(wǎng)之間的安全性驗(yàn)證
8.3.3 服務(wù)網(wǎng)絡(luò)基站與移動(dòng)用戶之間的安全性驗(yàn)證
8.4 本章小結(jié)
8.5 習(xí)題
第9章群組通信安全協(xié)議及其分析
9.1 群組通信概述
9.2 群組密鑰管理協(xié)議
9.3 密鑰管理方案
9.3.1 集中式密鑰管理方案
9.3.2 分布式密鑰分發(fā)方案
9.3.3 分擔(dān)式密鑰協(xié)商方案
9.4 群組密鑰交換協(xié)議的形式化描述及安全性分析
9.4.1 AT-GDH協(xié)議
9.4.2 AT-GDH2協(xié)議
9.4.3 AT-GDH3協(xié)議
9.5 本章小結(jié)
9.6 習(xí)題
參考文獻(xiàn)
出版說(shuō)明