公平交换协议的信道可信度形式化验证方法

• 作者: 杨晋吉 申涵瑞 陈清亮
• 来源期刊: 小型微型计算机系统
• 学科: 工学
• 关键词: 形式化验证 信道可信度 公平交换协议 概率模型检测 PRISM
• 年，卷（期）: 2018,（2）
• 所属期刊栏目: 计算机网络与信息安全
• 页码范围: 240-244
• 页数: 5页
• 分类号: TP301
• 字数: 5448字
• 语种: 中文
• DOI: 10.3969/j.issn.1000-1220.2018.02.011

摘要

公平交换协议是一种重要的电子商务安全协议,已有的针对公平交换协议进行的形式化验证只能定性分析协议是否满足给定性质,本文提出基于信道可信度的公平交换协议的形式化验证方法,重点对信道问题进行定量分析.以一个电子合同签署协议为例,通过概率模型检测的方法对协议建立离散时间马尔可夫链模型,用概率计算树逻辑对协议属性进行描述,通过PRISM概率模型检测工具对协议进行定量的验证和分析.实验结果表明公平交换协议各实体间信道可信度对协议的公平性、有效性和时限性有不同程度的影响,对相应信道进行控制或改善可以提高协议安全性.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	陈清亮	暨南大学计算机科学系	10	50	5.0	7.0
2	杨晋吉	华南师范大学计算机学院	30	177	8.0	12.0
3	申涵瑞	华南师范大学计算机学院	1	0	0.0	0.0