| 摘要 | 第4-5页 |
| Abstract | 第5页 |
| 1 绪论 | 第10-18页 |
| 1.1 研究背景及意义 | 第10-11页 |
| 1.2 国内外研究现状 | 第11-16页 |
| 1.3 本文的主要工作 | 第16页 |
| 1.4 文章组织结构 | 第16-18页 |
| 2 移动支付及协议 | 第18-24页 |
| 2.1 移动电子商务概述 | 第18-21页 |
| 2.1.1 移动电子商务的基本概念 | 第18页 |
| 2.1.2 移动电子商务的优势 | 第18-19页 |
| 2.1.3 移动通信场景模型 | 第19-21页 |
| 2.2 移动支付概述 | 第21-22页 |
| 2.2.1 移动支付的分类 | 第21页 |
| 2.2.2 移动支付的角色 | 第21-22页 |
| 2.2.3 移动支付的优势 | 第22页 |
| 2.3 移动支付协议 | 第22-23页 |
| 2.4 本章小结 | 第23-24页 |
| 3 基于时间自动机的移动支付协议的建模 | 第24-32页 |
| 3.1 时间自动机 | 第24-26页 |
| 3.2 移动支付协议的安全性质 | 第26-27页 |
| 3.3 时间自动机描述移动支付协议 | 第27-29页 |
| 3.3.1 系统主体的描述 | 第27-28页 |
| 3.3.2 移动支付通信环境的描述 | 第28页 |
| 3.3.3 主体操作的描述 | 第28-29页 |
| 3.4 移动支付协议的建模 | 第29-31页 |
| 3.5 本章小结 | 第31-32页 |
| 4 基于UPPAAL的移动支付协议PCMS的分析与验证 | 第32-46页 |
| 4.1 模型检测工具UPPAAL | 第32-33页 |
| 4.2 PCMS协议简介 | 第33-37页 |
| 4.2.1 符号说明 | 第33-34页 |
| 4.2.2 PCMS协议描述 | 第34-37页 |
| 4.3 PCMS协议参与者建模 | 第37-42页 |
| 4.3.1 顾客模型 | 第38-39页 |
| 4.3.2 支付网关模型 | 第39-40页 |
| 4.3.3 商家模型 | 第40-41页 |
| 4.3.4 发行方模型 | 第41页 |
| 4.3.5 收款方模型 | 第41-42页 |
| 4.4 PCMS协议模拟 | 第42-43页 |
| 4.5 PCMS协议验证 | 第43-45页 |
| 4.6 本章小结 | 第45-46页 |
| 5 总结与展望 | 第46-48页 |
| 5.1 工作总结 | 第46页 |
| 5.2 工作展望 | 第46-48页 |
| 参考文献 | 第48-51页 |
| 个人简历、在学期间发表的学术论文与研究成果 | 第51-52页 |
| 致谢 | 第52页 |