不可否认协议形式化分析的SVO逻辑方法

摘要：

使用SVO逻辑对Zhou-Gollmann的公平不可否认协议的一个改进协议进行了形式化分析.在分析该协议的过程中,分析了使用SVO逻辑分析不可否认协议时存在的一些问题,这是分析过程无法发现Zhou-Gollmann不可否认协议的原因.这些问题包括协议目标的确定,协议时限性的描述与分析,协议初始假设集的确定等.分析协议时,不仅需要证明协议的最终目标,还需要证明中间目标.通过对SVO逻辑的语法进行扩展,使其具有显式的时间描述能力,从而能够分析不可否认协议的时限性.

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

所属期刊栏目：35

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

资助基金：江苏省重点实验室基金BM20033201;江苏省高技术研究发展计划项目BG2004036

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

页数：共4页

页码：688-691