非否认协议公平性分析的扩展串空间方法

• 作者: 李磊 王育民 陈静
• 来源期刊: 西安交通大学学报
• 关键词: 非否认协议 扩展串空间 协议验证 公平性
• 年，卷（期）: 2010,（6）
• 页码范围: 16-20
• 分类号: TN918
• 语种: 中文

摘要

针对在非否认协议公平性的形式化分析中,如何弱化初始假定和避免状态空间爆炸等问题,提出了扩展串空间方法.通过将签名运算引入串空间理论,从而对串空间理论的项集合进行重新定义,进一步通过对子项关系、攻击者迹和自由加密假定的扩展,并结合丛概念,构成了扩展串空间.分析非否认协议的公平性,首先将协议行为归纳为攻击者串、发送者串、接收者串和可信第3方串,以此构造协议的扩展串空间模型,然后结合协议迹和定理证明验证丛中存在发送者串等价于丛中存在接收者串,从而证明非否认协议公平性.通过扩展串空间方法对Zhou-Gollmann协议公平性的分析,得到了与Kailar逻辑和Lanotte自动验证方法相同的结果.与Kailar逻辑相比,扩展串空间方法仅使用自由加密假定,弱化了初始假定;与Lanotte自动验证方法相比,扩展串空间方法无需使用状态空间搜索,避免了状态空间爆炸问题.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	王育民	西安电子科技大学综合业务网国家重点实验室	244	2283	26.0	36.0
2	陈静	西安交通大学电子与信息工程学院	37	180	6.0	12.0
3	李磊	西安电子科技大学综合业务网国家重点实验室	37	118	6.0	6.0