密碼協議分析的邏輯方法檢視原始碼討論檢視歷史

來自 孔夫子網 的圖片

《密碼協議分析的邏輯方法》，雷新鋒薛銳 著，出版社： 科學出版社。

書籍是人類進步的階梯，合理閱讀使一個人完善自身的知識結構，全面提升人文素質，為走向成功奠定堅實的基礎。

內容簡介

對密碼協議分析的邏輯方法進行系統介紹。主要內容包括密碼協議的概念以及密碼協議分析的主要方法綜述，密碼協議邏輯分析方法的理論基礎，各種密碼協議邏輯。這些邏輯涵蓋了當前比較重要的密碼協議分析邏輯，介紹了基於邏輯的計算可靠性的分析方法.重點介紹了作者在密碼協議分析的邏輯方面進行的工作.

目錄

前言

第1部分 理論基礎

第1章 數理邏輯基礎

1.1 基本概念

1.2 命題邏輯

1.2.1 命題邏輯語法

1.2.2 命題邏輯語義

1.2.3 命題邏輯推演系統

1.2.4 命題邏輯的可靠性

1.3 謂詞邏輯

1.3.1 謂詞邏輯語法

1.3.2 謂詞邏輯的語義

1.3.3 謂詞邏輯推演系統

1.3.4 謂詞邏輯的可靠性

1.4 模態邏輯

1.4.1 命題模態邏輯

1.4.2 謂詞模態邏輯

1.4.3 知識邏輯與信念邏輯

1.5 Hoare邏輯

1.6 本章小結

參考文獻

第2章 現代密碼學基礎

2.1 概述

2.1.1 加密方案

2.1.2 對加密方案的攻擊

2.1.3 信息論安全

2.1.4 現代密碼學

2.2 計算複雜性

2.2.1 圖靈機

2.2.2 時間複雜性

2.2.3 P與NP

2.2.4 多項式時間歸約

2.2.5 概率圖靈機與BPP

2.3 計算安全

2.3.1 計算安全的概念

2.3.2 安全假設

2.3.3 幾個安全相關概念

2.4 私鑰加密

2.4.1 私鑰加密方案

2.4.2 私鑰加密方案的CPA安全

2.4.3 私鑰加密方案的CCA安全

2.5 公鑰加密

2.5.1 公鑰加密方案

2.5.2 公鑰加密方案的CPA安全

2.5.3 公鑰加密方案的CCA安全

2.6 數字簽名

2.6.1 數字簽名方案

2.6.2 數字簽名方案的安全性

2.7 安全性證明

2.7.1 概率多項式時間歸約

2.7.2 混合論證

2.7.3 標準模型與隨機應答器模型

2.8 本章小結

參考文獻

第二部分 密碼協議分析概述

第3章 密碼協議

3.1 密碼協議的概念與意義

3.2 密碼協議的屬性與分類

3.3 對密碼協議的攻擊

3.4 密碼協議的表示法

3.5 密碼協議實例

3.6 本章小結

參考文獻

第4章 密碼協議分析

4.1 形式化方法

4.1.1 形式化方法概覽

4.1.2 DY模型

4.1.3 Woo-Lam模型及其擴展

4.2 計算方法

4.2.1 計算方法概覽

4.2.2 BR模型

4.2.3 其他模型

4.3 密碼協議形式化分析的計算可靠性

4.3.1 基於映射的方法

4.3.2 基於模擬的方法

4.3.3 已有形式化方法的計算可靠性

4.3.4 計算方法的直接形式化

4.4 可複合密碼協議分析

4.5 密碼協議邏輯

4.6 本章小結

參考文獻

第三部分 密碼協議邏輯

第5章 BAN邏輯

5.1 BAN邏輯的語法

5.2 推理規則

5.3 協議及其目標的描述

5.3.1 協議理想化

5.3.2 協議註解

5.3.3 認證目標的形式化

5.4 協議分析實例

5.4.1 NSSK協議及其形式化分析

5.4.2 Kerberos協議及其形式化分析

5.5 對BAN邏輯語義的簡單討論

5.6 對BAN邏輯的不同意見

5.6.1 Nessett的評論

5.6.2 Snekkenes的評論

5.7 本章小結

參考文獻

第6章 BAN邏輯的擴展

6.1 GNY邏輯

6.1.1 模型

6.1.2 GNY邏輯的語法

6.1.3 推理規則

6.1.4 協議形式化

6.1.5 協議分析實例

6.2 VO邏輯

6.2.1 語法擴展

6.2.2 公理與規則擴展

6.2.3 通用的形式化目標

6.2.4 通用的形式化假設

6.2.5 STS協議分析

6.3 MB邏輯

6.3.1 公式

6.3.2 推理規則

6.3.3 協議消息理想化

6.3.4 協議分析

6.4 本章小結

參考文獻

第7章 類BAN邏輯的語義

7.1 AT邏輯

7.1.1 AT邏輯對BAN邏輯的改進

7.1.2 語法

7.1.3 公理系統

7.1.4 模型

7.1.5 AT邏輯的語義

7.2 SVO邏輯

7.2.1 SVO邏輯語言

7.2.2 公理系統

7.2.3 模型

7.2.4 SVO邏輯的語義

7.2.5 SVO邏輯的可靠性

7.2.6 基於SVO邏輯的協議分析

7.3 本章小結

參考文獻

第8章 BAN邏輯的進一步擴展

8.1 Kailar邏輯

8.1.1 可追責性

8.1.2 分析框架

8.1.3 分析假設

8.1.4 邏輯規則

8.1.5 協議目標

8.1.6 分析實例

8.2 BSW邏輯

8.2.1 模型

8.2.2 BSW邏輯語言

8.2.3 推理規則

8.2.4 定理

8.2.5 合成規則

8.2.6 協議分析與設計的實例

8.3 本章小結

參考文獻

第9章 非單調邏輯

9.1 引言

9.2 Moser邏輯

9.2.1 知道與相信公理

9.2.2 unless謂詞

9.2.3 關於unless的例子

9.3 Rubin邏輯

9.3.1 khat協議

9.3.2 協議描述與分析概述

9.3.3 全局集

9.3.4 本地集

9.3.5 信任矩陣

9.3.6 行為描述

9.3.7 更新函數

9.3.8 推理規則

9.3.9 對khat協議的描述與分析

9.4 本章小結

參考文獻

第10章 引入時間的協議邏輯

10.1 CKT5邏輯

10.1.1 CKT5邏輯術語

10.1.2 安全性定理

10.2 CS邏輯

10.2.1 語法

10.2.2 公理與推理規則

10.2.3 實例分析

10.3 GS邏輯

10.3.1 擴展術語及規則

10.3.2 協議分析實例

10.4 本章小結

參考文獻

第11章 時間相關密碼協議邏輯及其形式化語義

11.1 TCPL的引入

11.2 TCPL的語法

11.3 公理與規則

11.4 TCPL的語義

11.4.1 模型

11.4.2 語義

11.5 TCPL的可靠性

11.6 基於TCPL的密碼協議形式化建模方案

11.6.1 密碼協議建模

11.6.2 安全屬性建模

11.7 基於TCPL的密碼協議分析

11.7.1 定時發布協議

11.7.2 NSPK協議

11.8 進一步討論

11.9 本章小結

參考文獻

第12章 協議複合邏輯

12.1 協議編程語言

12.1.1 PPL的語法

12.1.2 PPL的語義

12.2 協議及其屬性

12.2.1 協議執行模型

12.2.2 協議屬性

12.3 PCL的語法與語義

12.3.1 PCL的語法

12.3.2 PCL的語義

12.4 證明系統

12.5 PCL的可靠性

12.6 協議分析實例

12.6.1 弱認證

12.6.2 強認證性

12.7 協議複合

12.7.1 並行複合

12.7.2 順序複合

12.7.3 協議複合實例

12.8 PCL協議存在的問題

12.9 本章小結

參考文獻

第四部分 計算可靠的密碼協議邏輯

第13章 AR邏輯

13.1 形式化加密與消息等價

13.1.1 形式化消息

13.1.2 消息等價

13.2 加密方案與不可區分性

13.2.1 加密方案的安全性

13.2.2 加密方案安全性的定義

13.3 形式等價的計算可靠性

13.3.1 總體關聯

13.3.2 等價性蘊涵不可區分性

13.4 不完備性

13.5 完備性定理

13.5.1 無混淆加密與認證加密

13.5.2 完備性定理

13.6 本章小結

參考文獻

第14章 對AR邏輯的擴展

14.1 形式化模型

14.1.1 消息

14.1.2 模式

14.1.3 等價

14.2 計算模型

14.3 計算可靠性

14.4 本章小結

參考文獻

第15章 計算可靠的PCL

15.1 協議語法

15.2 邏輯語法

15.3 證明系統

15.4 證明實例

15.5 協議的執行

15.6 計算語義

15.7 本章小結

參考文獻

第16章 IK邏輯

16.1 T系統

16.1.1 語法

16.1.2 T系統的公理

16.1.3 T系統的可靠性

16.2 基於T系統的實例證明

16.3 計算不可區分系統

16.3.1 語法

16.3.2 證明規則

16.4 基於IK邏輯的證明實例

16.5 IK邏輯的可靠性

16.6 本章小結

參考文獻

第17章 計算不可區分邏輯

17.1 應答器系統

17.1.1 應答器系統與敵手

17.1.2 語義

17.1.3 事件

17.2 CIL的語句與基本規則

17.2.1 語句

17.2.2 基本規則

17.3 上下文

17.4 互模擬

17.5 確定性

17.6 CIL的規則與可靠性

17.6.1 上下文與應答器規則

17.6.2 派生規則與外部前提

17.7 概率簽名方案

17.7.1 隨機應答器

17.7.2 形式化證明

17.8 本章小結

參考文獻

結束語

索引