摘要
电子商务协议的安全性和原子性是电子商务研究者和使用者广泛关心的问题,采取一定的方法对协议进行分析检验是协议开发过程中一个必要环节。论文在对Netbill协议及其原子性进行形式化描述的基础上,基于符号模型检验器(SMV)从钱原子性和商品原子性两个角度对Netbill协议进行了分析和检验,从而表明了用SMV对电子商务协议分析和验证的可行性。
In e-commerce field,security and atomicity of e-commerce protocols are two important issues.It is a neces-sary step to analyze and verify them in the developing protocol.In this paper,the Netbill protocol and its atomicity are formally represented.Then the atomicity of money and goods is analyzed and verified using symbolic model verifier(SMV).It is shown that SMV is a suitable tool to analyze and verify e-commerce protocols.
出处
《计算机工程与应用》
CSCD
北大核心
2004年第2期57-59,共3页
Computer Engineering and Applications
基金
广西跨世纪人才基金项目
广西科学基金项目(编号:0141046)资助
关键词
电子商务协议
符号模型检验
原子性
Electronic Commerce Protocol,Symbolic Model Checking,Atomicity
