移动支付协议PCMS的形式化分析和验证

• 作者: 吴格格 庄雷 张坤丽 王国卿
• 来源期刊: 计算机工程与科学
• 学科: 工学
• 关键词: 移动支付协议 模型检测 时间自动机 UPPAAL
• 年，卷（期）: 2017,（1）
• 所属期刊栏目: 计算机网络与信息安全
• 页码范围: 67-73
• 页数: 7页
• 分类号: TP309
• 字数: 5174字
• 语种: 中文
• DOI: 10.3969/j.issn.1007-130X.2017.01.009

摘要

移动电子商务协议的形式化分析和验证是近年来移动电子商务协议的一个重要研究热点.以一个支付网关为中心的匿名的移动电子商务支付协议PCMS为研究对象,建立了PCMS协议的时间自动机模型,并用计算树逻辑CTL公式描述PCMS协议的部分性质,最后利用模型检测工具UPPAAL对PCMS协议的无死锁、时效性、有效性和钱原子性进行检测验证.验证结果表明,以支付网关为中心的匿名的安全支付协议PCMS满足无死锁、时效性、有效性和钱原子性.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	张坤丽	郑州大学信息工程学院	24	195	9.0	13.0
2	庄雷	郑州大学信息工程学院	92	704	13.0	21.0
3	王国卿	郑州大学信息工程学院	13	54	5.0	7.0
4	吴格格	郑州大学信息工程学院	1	5	1.0	1.0