电子合同签订协议的符号模型检验分析  

Symbolic Model Checking Analysis for Electronic Contract Signing Protocol

作　　者：常亮[1] 古天龙[1] 郭云川[1] 

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

出　　处：《计算机工程与应用》2005年第1期161-164,共4页Computer Engineering and Applications

基　　金：广西科学基金资助

摘　　要：与密钥分发和认证协议相比,电子合同签订协议的形式化分析遇到了新的挑战。以Asokan、Shoup和Waidner提出的乐观合同签订协议为例,在对协议进行建模以及对相应的安全性质进行形式化描述的基础上,用符号模型检验器SMV对公平性、适时性和无滥用性进行了分析,检测出了相关的缺陷。表明了用SMV对电子合同签订协议进行符号模型分析的有效性。There exist challenges in applying formal techniques to electronic contract signing protocols,which are not encountered in the analysis of key exchange and authentication protocols.In this paper,the optimistic contract signing protocol is studied as a typical case.The symbolic model and the formal security properties for the protocol are developed.The protocol is verified via SMV,and some flaws are discovered.This work demonstrates the feasibility of using SMV to analyze electronic contract signing protocol.

关 键 词：电子合同签订协议 符号模型检验 公平性 无滥用性 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]