多方不可否认协议的增广CSP建模与分析
形式化分析是验证不可否认协议安全性的重要方法，然而现有研究大都集中在两方不可协议建模与分析上，对多方不可否认协议安全性验证缺少关注，致使该类协议的安全缺陷无法得到及时检测。本文基于逆向工程的思想，使用前期工作中提出的面向两方不可否认协议分析的增广CSP方法，对典型的Kremer-Markowitch多方不可否认协议的安全性进行了尝试性建模与分析。借助该分析我们成功发现该协议在满足不可否认性和公平性的同时却不具备时限性。这表明在适用于两方不可否认协议安全性验证的同时，增广CSP方法也可作为多方不可否认协议安全性验证的新方法。
形式化分析 多方不可否认 时限性 增广CSP方法
韩志耕 陈耿 罗军舟
南京审计学院 信息科学学院,江苏 南京 211815 东南大学 计算机科学与工程学院,江苏 南京 211189
国内会议
长沙
中文
1-10
2012-11-01（万方平台首次上网日期，不代表论文的发表时间）