電子商務網(wǎng)絡協(xié)議的形式化分析理論與應用

序
前言
第1章　概論
1.1　信息安全的基本定義
1.2　網(wǎng)絡的安全問題
1.3　網(wǎng)絡安全體系結(jié)構(gòu)
第2章　電子商務協(xié)議的形式化分析理論基礎(chǔ)
2.1　電子商務的定義
2.2　電子商務協(xié)議的安全性
2.2.1　電子商務協(xié)議的安全性
2.2.2　電子商務協(xié)議的設計原則
2.2.3　電子商務協(xié)議的安全分析
2.2.4　電子商務協(xié)議形式化分析方法分類
第3章　電子商務協(xié)議的形式化邏輯分析方法
3.1　BAN邏輯
3.1.1　BAN邏輯公式
3.1.2　BAN邏輯的推理規(guī)則
3.1.3　BAN邏輯的評價
3.2　Kailar邏輯
3.2.1　Kailar邏輯公式
3.2.2　Kailar邏輯的推理規(guī)則
3.3　NDL邏輯
3.3.1　NDL邏輯的語法
3.3.2　NDL邏輯的推理規(guī)則
3.4　卿周邏輯
3.4.1　卿周邏輯的語法
3.4.2　卿周邏輯的推理規(guī)則
第4章 電子商務協(xié)議的通用形式化Petri網(wǎng)模型分析方法
4.1　Petri網(wǎng)概述
4.2　Petri網(wǎng)的定義
4.3　Petri網(wǎng)的應用實例
4.4　Petri網(wǎng)的特性
4.4.1　保守網(wǎng)
4.4.2　有界網(wǎng)
4.4.3　活動性
4.4.4　并發(fā)與沖突
4.5　Petri網(wǎng)的擴充
4.5.1　輸人函數(shù)和輸出函數(shù)的擴充
4.5.2　觸發(fā)條件的擴充
4.5.3　旗標和庫所的擴充（著色Petri網(wǎng)）
4.6　Petri網(wǎng)的替換與合成
4.7　常用的Petri網(wǎng)模型
4.7.1　庫所／變遷網(wǎng)（P／T網(wǎng)）的形式化定義
4.7.2　有色網(wǎng)的形式化定義
4.7.3　常量弧有色網(wǎng)的形式化定義
4.8　Petri網(wǎng)的分析
4.8.1　常量弧網(wǎng)
4.8.2　庫所／變遷網(wǎng)（P／T網(wǎng)）
4.8.3　有色網(wǎng)
第5章 電子商務協(xié)議的形式化有窮自動機模型檢測分析方法
5.1　有窮自動機的定義
5.2　傳輸通道類別
5.3　通道DFA
5.4　協(xié)議實體DFA
5.5　DFA的簡化
5.6　DFA的合成
第6章　基于電子商務安全認證和交易的基本協(xié)議
6.1　安全認證的基本協(xié)議
6.1.1　Needham—Schroeder認證協(xié)議
6.1.2　Kerberos認證協(xié)議
6.1.3　Otwag—Rees認證協(xié)議
6.2　電子交易的基本協(xié)議
6.2.1　網(wǎng)上交易協(xié)議遵循的原則
6.2.2　IBS支付協(xié)議
6.2.3　CMP1及CMP2非否認協(xié)議
　　……
第7章　基于公鑰基礎(chǔ)設施PKI的安全認證協(xié)議
第8章　基于工商管理的安全認證協(xié)議
第9章　安全認證協(xié)議的Petri網(wǎng)模型
第10章　支付協(xié)議的有窮自動機模型
第11章　協(xié)議的有色Petri網(wǎng)模型及分析
參考文獻