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

摘要：

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

关键词：不可否认、时限性、SVO逻辑、形式化分析

所属期刊栏目：17

分类号：TP393(计算技术、计算机技术)

资助基金：中国科学院资助项目90412014,90604004;江苏省高技术研究发展计划项目BG2004036;江苏省网络与信息安全重点实验室基金BM2003201

在线出版日期：2006-07-31（万方平台首次上网日期，不代表论文的发表时间）

页数：共7页

页码：1510-1516