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

• 作者: 罗军舟 黎波涛
• 来源期刊: 软件学报
• 学科: 工学
• 关键词: 不可否认 时限性 SVO逻辑 形式化分析
• 年，卷（期）: 2006,（7）
• 所属期刊栏目: 算法设计与分析
• 页码范围: 1510-1516
• 页数: 7页
• 分类号: TP393
• 字数: 5721字
• 语种: 中文

摘要

虽然SVO逻辑由于其简单性在对不可否认协议的形式化分析中得到了广泛的应用,但它在时间描述能力上的不足使得它无法分析不可否认协议的时限性.通过向SVO逻辑添加一种简单的时间表达和分析方法扩展了SVO逻辑,并使用扩展后的逻辑对Zhou和Gollmann于1996年提出的一个公平不可否认协议及其一个改进协议进行了分析.分析结果表明,原协议不具有时限性,而改进协议具有时限性,因此也说明了扩展后的新逻辑能够分析不可否认协议的时限性.另外,新逻辑还能用来分析一般密码协议中的时间相关性质.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	罗军舟	东南大学计算机科学与工程系	165	4086	26.0	60.0
2	黎波涛	东南大学计算机科学与工程系	5	79	4.0	5.0