序 前言 第1章 緒論 1.1 引言 1.2 投票的分類 1.2.1 按照票的介質進行分類 1.2.2 按照票的類型進行分類 1.2.3 按照票的權重進行分類 1.3 傳統投票模型 1.4 遠程網絡投票模型 1.5 本章小結 參考文獻 第2章 相關的密碼技術 2.1 公鑰密碼體制 2.1.1 RSA公鑰加密體制 2.1.2 E1Gamal公鑰加密體制 2.1.3 Paillier公鑰加密體制 2.1.4 BCP公鑰密碼體制 2.2 秘密共享 2.3 門限公鑰加密 2.3.1 RSA公鑰加密的門限版本 2.3.2 E1Gamal公鑰加密的門限版本 2.3.3 Paillier加密的門限版本 2.4 盲簽名 2.5 同態(tài)加密 2.6 混淆網 2.7 Fiat―Shamir啟發(fā)式 2.8 離散對數相等知識證明 2.9 BCP承諾方案 2.10 分布式明文相等測試 2.11 指定驗證者證明/簽名 2.12 指定驗證者離散對數相等證明 2.13 明文相等證明協議 2.14 指定驗證者再加密證明 2.15 非交互式可否認認證協議 2.15.1 Meng非交互式可否認認證協議 2.15.2 Fan交互式可否認認證協議 2.16 Meng和Wang可否認加密模式 2.17 本章小結 參考文獻 第3章 遠程網絡投票協議 3.1 遠程網絡投票協議安全屬性 3.2 遠程網絡投票協議國內外發(fā)展現狀 3.2.1 無收據性 3.2.2 抗威脅性 3.3 本章小結 參考文獻 第4章 典型遠程網絡投票協議 4.1 DLM投票協議 4.2 F00投票協議 4.3 CGS投票協議 4.4 JCJ投票協議 4.5 Acquisti投票協議 4.6 提出的基于明文相等證明的投票協議 4.7 提出的基于非交互式可否認認證協議的投票協議 4.8 提出的基于可否認加密的投票協議 4.9 本章小結 參考文獻 第5章 基于符號模型的遠程網絡投票協議分析與驗證 5.1 引言 5.2 符號模型分析與驗證遠程網絡投票協議 5.3 本章小結 參考文獻 第6章 手工方式分析與驗證無收據性 6.1 DKR模型及應用 6.1.1 應用PI演算 6.1.2 DKR模型 6.1.3 DKR模型應用 6.2 Jonker-Vink模型及應用 6.2.1 Jonkei-Vink模型 6.2.2 Jonker-Vink模型應用 6.3 Meng模型及應用 6.3.1 Kessler和Neumann邏輯 6.3.2 Meng模型 6.3.3 Meng模型應用 6.4 本章小結 參考文獻 第7章 自動化分析與驗證正確性與抗威脅性 7.1 引言 7.2 一階定理證明器ProVer。if 7.3 Backes模型 7.3.1 遠程網絡投票協議形式化模型 7.3.2 安全屬性形式化定義 7.4 本章小結 參考文獻 第8章 自動化分析與驗證抗拒絕服務攻擊性 8.1 引言 8.2 擴展的應用PI演算 8.2.1 攻擊者上下文 8.2.2 項 8.2.3 擴展后的進程 8.2.4 進程上下文 8.3 定義和符號說明 8.4 自動化證明抗拒絕服務攻擊性方法 8.5 本章小結 參考文獻 第9章 自動化分析與驗證典型遠程網絡投票協議安全性 9.1 正確性與抗威脅性 9.1.1 Meng等投票協議 9.1.2 Meng投票協議 9.1.3 Acquisti投票協議 9.2 抗拒絕服務攻擊性 9.2.1 Meng投票協議 9.2.2 Acquisti投票協議 9.3 本章小結 參考文獻 第10章 基于計算模型的遠程網絡投票協議分析與驗證 10.1 引言 10.2 計算模型分析與驗證遠程網絡投票協議 10.3 本章小結 參考文獻 第11章 Blanchet演算和CryptoVerif 11.1 B1anchet演算 11.2 自動化證明工具CryptoVerif 11.2.1 結構 11.2.2 證明目標 11.2.3 語法 11.3 應用:可否認性模型 11.3.1 提出的可否認性模型 11.3.2 Meng協議可否認性自動化證明 11.3.3 Fan協議可否認性自動化證明 11.4 本章小結 參考文獻 第12章 擴展的Blanchet演算 12.1 擴展的Blanchet演算 12.2 應用:抗拒絕服務攻擊性模型 12.2.1 提出的基于事件的抗拒絕服務攻擊性模型 12.2.2 4步握手協議抗拒絕服務攻擊性自動化證明 12.3 本章小結 參考文獻 第13章 自動化分析與驗證典型遠程網絡投票協議抗威脅性 13.1 引言 13.2 提出的抗威脅性模型 13.3 自動化證明Meng等投票協議抗威脅性 13.3.1 Meng等投票協議 13.3.2 基于擴展的Blanchet演算建模Meng等投票協議 13.3.3 Meng等投票協議抗威脅性自動化證明 13.4 本章小結 參考文獻