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

Formal analysis of non-repudiation protocols with SVO logic

作　　者：黎波涛[1] 罗军舟[1] 

机构地区：[1]东南大学计算机科学与工程系,南京210096

出　　处：《东南大学学报（自然科学版）》2005年第5期688-691,共4页Journal of Southeast University：Natural Science Edition

基　　金：江苏省"网络与信息安全"重点实验室计划资助项目(BM20033201);江苏省高技术研究资助项目(BG2004036)

摘　　要：使用SVO逻辑对Zhou-Gollmann的公平不可否认协议的一个改进协议进行了形式化分析.在分析该协议的过程中,分析了使用SVO逻辑分析不可否认协议时存在的一些问题,这是分析过程无法发现Zhou-Gollmann不可否认协议的原因.这些问题包括协议目标的确定,协议时限性的描述与分析,协议初始假设集的确定等.分析协议时,不仅需要证明协议的最终目标,还需要证明中间目标.通过对SVO逻辑的语法进行扩展,使其具有显式的时间描述能力,从而能够分析不可否认协议的时限性.A new improvement of Zhou-Gollmann＇s fair non-repudiation protocol is analyzed with SVO logic. Some problems in the analysis of non-repudiation protocols using SVO logic, which are the causes why the flaw of Zhou-Gollmann＇s fair non-repudiation cannot be discovered, are discussed. These problems include determination of protocol goals, analysis of timeliness property of protocols and premise set establishment. In the analysis, both the final goals and the intermediary goals need to be proved. By extending the syntax of SVO logic, a time description method is added into it and, thus the timeliness of non-repudiation protocols can be analyzed.

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

分 类 号：TP393[自动化与计算机技术—计算机应用技术]