| 中文摘要 | 第4-5页 |
| 英文摘要 | 第5页 |
| 1 绪 论 | 第8-14页 |
| 1.1 问题的提出及研究意义 | 第8-9页 |
| 1.2 国内外研究现状 | 第9-13页 |
| 1.2.1 密码协议的研究与发展 | 第9-10页 |
| 1.2.2 电子商务及协议的研究状况 | 第10-11页 |
| 1.2.3 形式化分析方法的研究与进展 | 第11-13页 |
| 1.3 本文研究的目的和研究内容 | 第13-14页 |
| 2 安全认证协议和电子交易协议 | 第14-24页 |
| 2.1 认证协议 | 第14-17页 |
| 2.1.1 Needham-Schroeder协议 | 第14-16页 |
| 2.1.2 Otway-Rees协议 | 第16页 |
| 2.1.3 简化的Kerberos协议 | 第16-17页 |
| 2.1.4 Denning-Sacco协议 | 第17页 |
| 2.2 电子商务协议 | 第17-20页 |
| 2.2.1 电子商务协议的设计原则 | 第17-19页 |
| 2.2.2 SSL(安全套接层协议) | 第19-20页 |
| 2.2.3 SET协议 | 第20页 |
| 2.3 安全协议设计和分析的说明 | 第20-24页 |
| 3 安全协议的形式化分析技术 | 第24-30页 |
| 3.1 BAN逻辑 | 第24-27页 |
| 3.1.1 BAN逻辑的表示及含义 | 第24页 |
| 3.1.2 BAN逻辑公式 | 第24-25页 |
| 3.1.3 BAN逻辑的协议分析步骤 | 第25-26页 |
| 3.1.4 BAN逻辑的说明 | 第26-27页 |
| 3.2 Kailar逻辑 | 第27-30页 |
| 3.2.1 Kailar逻辑的表示和含义 | 第27-28页 |
| 3.2.2 Kailar逻辑的推理规则 | 第28页 |
| 3.2.3 Kailar逻辑的说明 | 第28-30页 |
| 4 公钥基础设施PKI的安全认证 | 第30-37页 |
| 4.1 PKI安全体系结构 | 第30-31页 |
| 4.2 安全认证体系结构标准X | 第31-35页 |
| 4.2.1 X.509的简单认证程序 | 第32-33页 |
| 4.2.2 X.509的强认证程序 | 第33页 |
| 4.2.3 X.509的证书内容 | 第33-35页 |
| 4.3 安全认证的目录存取协议LDAP | 第35-37页 |
| 5 某工商年审系统的安全认证协议设计及形式化描述 | 第37-46页 |
| 5.1 认证协议的用户需求 | 第37-38页 |
| 5.2 安全认证协议的功能和机制 | 第38-40页 |
| 5.3 安全认证协议的协议元素 | 第40-42页 |
| 5.4 认证协议的形式化规定 | 第42-43页 |
| 5.5 单向认证协议 | 第43-44页 |
| 5.6 双向认证协议 | 第44-46页 |
| 6 某工商年审系统安全认证协议的验证及应用 | 第46-53页 |
| 6.1 认证协议安全性分析验证及修改 | 第46-51页 |
| 6.1.1 单向认证协议的安全性分析验证及修改 | 第46-48页 |
| 6.1.2 修改后的单向认证协议的安全性分析验证 | 第48-50页 |
| 6.1.3 双向认证协议的安全性分析验证及修改 | 第50-51页 |
| 6.2 某工商年检系统安全认证协议的应用 | 第51-53页 |
| 6.2.1 某工商网上年检系统简要分析 | 第51页 |
| 6.2.2 安全认证协议在某工商年检系统中的应用 | 第51-53页 |
| 7 结 论 | 第53-54页 |
| 致 谢 | 第54-55页 |
| 参考文献 | 第55-57页 |