不可否认协议时限性的形式化分析

被引:15
作者
黎波涛
罗军舟
机构
[1] 东南大学计算机科学与工程系
关键词
不可否认; 时限性; SVO逻辑; 形式化分析;
D O I
暂无
中图分类号
TP393.04 [];
学科分类号
摘要
虽然SVO逻辑由于其简单性在对不可否认协议的形式化分析中得到了广泛的应用,但它在时间描述能力上的不足使得它无法分析不可否认协议的时限性.通过向SVO逻辑添加一种简单的时间表达和分析方法扩展了SVO逻辑,并使用扩展后的逻辑对Zhou和Gollmann于1996年提出的一个公平不可否认协议及其一个改进协议进行了分析.分析结果表明,原协议不具有时限性,而改进协议具有时限性,因此也说明了扩展后的新逻辑能够分析不可否认协议的时限性.另外,新逻辑还能用来分析一般密码协议中的时间相关性质.
引用
收藏
页码:1510 / 1516
页数:7
相关论文
共 3 条
[1]   一个非否认协议ZG的形式化分析 [J].
范红 ;
冯登国 .
电子学报, 2005, (01) :171-173
[2]   公平的非否认密码协议及其形式分析与应用 [J].
李先贤 ;
怀进鹏 .
软件学报, 2000, (12) :1628-1634
[3]   一种新型的非否认协议 [J].
卿斯汉 .
软件学报, 2000, (10) :1338-1343