Digicash协议原子性的符号模型分析

电子商务协议的安全性和原子性是电子商务研究者和使用者广泛关心的问题,在协议设计完成之后,采取一定的方法对协议进行分析检验以确认协议,是否满足协议是否符合协议设计要求是十分必要的。提出了可以用符号模型检验器(SMV)对电子商务协议进行分析,在对Digicash协议及电子商务原子性进行形式化描述的基础上,用SMV从钱原子性和商品原子性这两个角度对Digicash协议的原子性进行了分析和检验,指出了Digicash协议的缺陷,从而表明了用SMV对电子商务协议分析和验证的可行性。

Symbolic Model Checking Analysis for Atomicity of Digicash Protocol

In electronic commerce field,researchers and users care more about the security and atomicity of electronic commerce protocol.It is necessary that measures verifying the protocol are taken to examine whether all properties are satisfied after the protocol has been designed.A methodology is presented for verifying requirements of electronic commerce protocols by means of SMV.Our work principally focuses on formal representations of protocol specification and atomicity requirements.As case Digicash protocol is studied in two aspects-money and goods atomicity and as a result five attacks upon the protocol are discovered.In addition to some insight to Digicash protocol,this study demonstrates the feasibility of using SMV to analyze electronic commerce protocol