《密碼協議分析的邏輯方法》注重由淺入深，適合各層次讀者參閱。全書從基礎理論和基本概念入手，涵蓋了主要的密碼協議分析邏輯以及該領域的一些前沿理論，其中包括作者在密碼協議分析的邏輯方面所做的工作。這些內容對於初學者有著重要的啟發和引導作用，對於研究者具有一定的參考價值，對於密碼協議的分析和設計人員具有重要的指導意義。本書由雷新鋒，薛銳著。

《密碼協議分析的邏輯方法》對密碼協議分析的邏輯方法進行了繫統 詳盡和深入的介紹，全書共四部分，第一部分是理論基礎，第二部分是密 碼協議分析概述，第三部分介紹密碼協議邏輯，第四部分介紹計算可靠的 密碼協議邏輯。 本書的內容包括密碼協議分析相關數理邏輯和現代密碼學理論的基礎 知識、密碼協議分析的主要方法綜述、各種密碼協議邏輯、協議分析實例 以及密碼協議邏輯分析方法的計算可靠性等。內容涵蓋了所有迄今為止重 要的密碼協議分析邏輯繫統，其中包括作者在密碼協議分析方面的工作。 《密碼協議分析的邏輯方法》的讀者對像為信息安全專業高年級本科 生及研究生，也可供從事信息安全專業的教學、科研人員和工程技術人員 參考。本書由雷新鋒，薛銳著。

前言
**部分 理論基礎
第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 密碼協議的表示法
……
第4章 密碼協議分析
第三部分 密碼協議邏輯
第5章 BAN邏輯
第6章 BAN邏輯的擴展
第7章 類BAN邏輯的語義
第8章 BAN邏輯的進一步擴展
第9章 非單調邏輯
**0章 引入時間的協議邏輯
**1章 時間相關密碼協議邏輯及其形式化語義
**2章 協議復合邏輯
第四部分 計算可靠的密碼協議邏輯
**3章 AR邏輯
**4章 對AR邏輯的擴展
**5章 計算可靠的PCL
**6章 IK邏輯
**7章 計算不可區分邏輯
結束語
索引