有穷机和逻辑结合的电子商务协议分析方法

• 作者: 侯贵宾 刘文远 司亚利 马生
• 来源期刊: 小型微型计算机系统
• 学科: 工学
• 关键词: 电子商务协议 形式化分析 有穷自动机 逻辑分析
• 年，卷（期）: 2013,（3）
• 所属期刊栏目: 计算机软件与数据库技术
• 页码范围: 492-497
• 页数: 6页
• 分类号: TP391
• 字数: 7667字
• 语种: 中文

摘要

提出一种扩展的有穷自动机模型,并结合卿-周逻辑给出一种新的电子商务协议形式化分析方法,用于分析电子商务协议的可追究性、公平性和时限性.该方法结合了模型检测和逻辑分析两种形式化分析方法的优点,可以准确形象地描述协议的具体运行过程,并且在发生重放攻击时能够正确分析各方的责任.利用该方法对Kim等人提出的改进版ZG协议进行了实例分析,给出了描述该协议运行过程的状态转换图,结合状态转换图对该协议分析得出其满足可追究性、公平性、时限性,并且不存在被重放攻击的可能.最后用时间自动机UPPAAL验证了新方法中有穷自动机模型的准确性和时限性分析的有效性.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	刘文远	燕山大学信息科学与工程学院	154	739	14.0	19.0
2	司亚利	燕山大学里仁学院	22	84	5.0	8.0
3	马生	燕山大学信息科学与工程学院	1	1	1.0	1.0
4	侯贵宾	燕山大学信息科学与工程学院	2	4	1.0	2.0