公平非否认协议的有限状态分析  

Finite-state Analysis of a Fair Non-repudiation Protocol

作　　者：董荣胜[1] 陈大伟[1] 郭云川[1] 古天龙[1] 

机构地区：[1]桂林电子工业学院计算机系,桂林541004

出　　处：《计算机科学》2005年第8期83-86,共4页Computer Science

基　　金：广西自然科学基金(编号:桂科自0229051)

摘　　要：本文针对公平非否认协议给出了一种基于有限状态自动机的分析模型,并使用SPIN模型检测工具,对Zhou-Gollmann非否认协议进行了分析,结果发现该协议不满足公平性和机密性,为此对该协议进行了改进。A model based on finite state automaton is proposed for a fair non-repudiation protocol. The Zhou-Gollmann fair non-repudiation protocol is analyzed with using model checker SPIN. The results show that the protocol isn＇t satisfied with fairness and confidentiality. Finally, some improvements are given for this protocol.

关 键 词：模型检测 SPIN 非否认性 公平性 机密性 有限状态自动机 非否认协议 状态分析 检测工具 模型 

分 类 号：TP301.1[自动化与计算机技术—计算机系统结构] TP393.08[自动化与计算机技术—计算机科学与技术]