基于ATL的公平交换协议的形式化验证

• 作者: 李群 陈清亮
• 来源期刊: 计算机工程与应用
• 学科: 工学
• 关键词: 形式化验证 交替时态逻辑(ATL) MOCHA工具 公平交换协议
• 年，卷（期）: 2015,（19）
• 所属期刊栏目: 理论研究、研发设计
• 页码范围: 32-36
• 页数: 5页
• 分类号: TP301.2
• 字数: 6359字
• 语种: 中文
• DOI: 10.3778/j.issn.1002-8331.1410-0375

摘要

如何对电子商务协议进行分析与验证一直是研究的热点，基于ATL（交替时态逻辑）对电子商务协议中的公平交换协议（Fair Exchange Protocols）进行形式化分析与验证，并选取了其中的一个电子合同签署协议进行形式化验证。用ATL语言来形式化描述公平交换协议，并使用ATS（Alternating Transition Systems，交替转移系统）来为公平交换协议进行形式化建模，再用形式化验证工具MOCHA对公平交换协议的公平性（Fairness）、及时性（Timeli-ness）和不可滥用性（Abuse-Freeness）进行有效的验证；对验证结果进行分析与讨论，发现了该协议不满足公平性和不可滥用性，不符合设计的要求。

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	陈清亮	暨南大学计算机科学系	10	50	5.0	7.0
2	李群	暨南大学计算机科学系	2	1	1.0	1.0