第1章 绪论 1
1.1引言 1
1.2投票的分类 2
1.2.1按照票的介质进行分类 2
1.2.2按照票的类型进行分类 3
1.2.3按照票的权重进行分类 4
1.3传统投票模型 4
1.4远程网络投票模型 5
1.5本章小结 6
参考文献 6
第2章 相关的密码技术 9
2.1公钥密码体制 9
2.1.1 RSA公钥加密体制 9
2.1.2 ElGamal公钥加密体制 9
2.1.3 Paillier公钥加密体制 9
2.1.4 BCP公钥密码体制 10
2.2秘密共享 10
2.3门限公钥加密 12
2.3.1 RSA公钥加密的门限版本 12
2.3.2 ElGamal公钥加密的门限版本 13
2.3.3 Paillier加密的门限版本 13
2.4盲签名 14
2.5同态加密 14
2.6混淆网 16
2.7 Fiat-Shamir启发式 18
2.8离散对数相等知识证明 18
2.9 BCP承诺方案 19
2.10分布式明文相等测试 20
2.11指定验证者证明/签名 21
2.12指定验证者离散对数相等证明 23
2.13明文相等证明协议 24
2.14指定验证者再加密证明 26
2.15非交互式可否认认证协议 28
2.15.1 Meng非交互式可否认认证协议 30
2.15.2 Fan交互式可否认认证协议 33
2.16 Meng和Wang可否认加密模式 34
2.17本章小结 38
参考文献 38
第3章 远程网络投票协议 45
3.1远程网络投票协议安全属性 45
3.2远程网络投票协议国内外发展现状 47
3.2.1无收据性 47
3.2.2抗威胁性 56
3.3本章小结 63
参考文献 64
第4章 典型远程网络投票协议 68
4.1 DLM投票协议 68
4.2 FOO投票协议 69
4.3 CGS投票协议 72
4.4 JCJ投票协议 74
4.5 Acquisti投票协议 76
4.6提出的基于明文相等证明的投票协议 81
4.7提出的基于非交互式可否认认证协议的投票协议 90
4.8提出的基于可否认加密的投票协议 94
4.9本章小结 98
参考文献 98
第5章 基于符号模型的远程网络投票协议分析与验证 102
5.1引言 102
5.2符号模型分析与验证远程网络投票协议 103
5.3本章小结 107
参考文献 107
第6章 手工方式分析与验证无收据性 111
6.1 DKR模型及应用 111
6.1.1应用PI演算 111
6.1.2 DKR模型 115
6.1.3 DKR模型应用 116
6.2 Jonker-Vink模型及应用 122
6.2.1 Jonker-Vink模型 122
6.2.2 Jonker-Vink模型应用 123
6.3 Meng模型及应用 127
6.3.1 Kessler和Neumann逻辑 127
6.3.2 Meng模型 132
6.3.3 Meng模型应用 134
6.4本章小结 139
参考文献 139
第7章 自动化分析与验证正确性与抗威胁性 141
7.1引言 141
7.2一阶定理证明器ProVerif 141
7.3 Backes模型 145
7.3.1远程网络投票协议形式化模型 145
7.3.2安全属性形式化定义 146
7.4本章小结 148
参考文献 148
第8章 自动化分析与验证抗拒绝服务攻击性 150
8.1引言 150
8.2扩展的应用PI演算 152
8.2.1攻击者上下文 152
8.2.2项 153
8.2.3扩展后的进程 153
8.2.4进程上下文 154
8.3定义和符号说明 154
8.4自动化证明抗拒绝服务攻击性方法 156
8.5本章小结 158
参考文献 159
第9章 自动化分析与验证典型远程网络投票协议安全性 161
9.1正确性与抗威胁性 161
9.1.1 Meng等投票协议 161
9.1.2 Meng投票协议 179
9.1.3 Acquisti投票协议 197
9.2抗拒绝服务攻击性 215
9.2.1 Meng投票协议 215
9.2.2 Acquisti投票协议 220
9.3本章小结 224
参考文献 225
第10章 基于计算模型的远程网络投票协议分析与验证 227
10.1引言 227
10.2计算模型分析与验证远程网络投票协议 229
10.3本章小结 231
参考文献 232
第11章 Blanchet演算和CryptoVerif 238
11.1 Blanchet演算 238
11.2自动化证明工具CryptoVerif 244
11.2.1结构 244
11.2.2证明目标 249
11.2.3语法 250
11.3应用：可否认性模型 252
11.3.1提出的可否认性模型 252
11.3.2 Meng协议可否认性自动化证明 257
11.3.3 Fan协议可否认性自动化证明 267
11.4本章小结 280
参考文献 280
第12章 扩展的Blanchet演算 282
12.1扩展的Blanchet演算 282
12.2应用：抗拒绝服务攻击性模型 284
12.2.1提出的基于事件的抗拒绝服务攻击性模型 284
12.2.2 4步握手协议抗拒绝服务攻击性自动化证明 286
12.3本章小结 292
参考文献 293
第13章 自动化分析与验证典型远程网络投票协议抗威胁性 294
13.1引言 294
13.2提出的抗威胁性模型 294
13.3自动化证明Meng等投票协议抗威胁性 298
13.3.1 Meng等投票协议 298
13.3.2基于扩展的Blanchet演算建模Meng等投票协议 300
13.3.3 Meng等投票协议抗威胁性自动化证明 307
13.4本章小结 313
参考文献 313