保护个人的利益——电子商务协议新属性的自动验证  

Automatic Verification of a New Property of E-commerce Protocols:the Protection of Individuals' Interests

作　　者：博诺 黄连生[1] 

机构地区：[1]清华大学计算机系网络技术研究所,北京100084 [2]里昂中央理工大学,法国

出　　处：《计算机工程与应用》2004年第12期153-155,226,共4页Computer Engineering and Applications

摘　　要：电子商务的快速发展加强了电子商务协议的新类型的需求,尤其对各种复杂协议的需求,这使得协议本身安全性的证明变得更为困难。为了证明电子商务协议的可靠性,研究人员已设计了各种方法。为了更加清楚地描述需要证明的电子商务协议的安全目标,研究者们已经提出了几种标志性属性,其中之一是较著名的原子性犤8犦,但这并不能完全描述电子商务协议的全部安全性定义。在犤1犦里,研究员对一项有研究价值的新属性进行了研究,称为“保护个人的利益”,并且提出一个手工验证的模型。该模型虽然有效,但是实用性较差。文章提出了一个基于模型检验这种技术的自动验证方法。The boom of electronic commerce has urged the need for new types of protocols,which have to be more and more sophisticated.In order to prove their reliability,several methods have been designed.Many properties have also been defined to explain what the main goal of an electronic commerce protocol has to be.Among them,the most famous is atomicity.A valuable new property is defined in and a model is designed to prove it(by hand):it is called the pro-tection of individuals' interests.This paper shows a way to check it automatically thanks to a framework based on model checking.

关 键 词：电子商务协议 自动验证 模型检验 

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