电子商务协议的形式化分析方法

ISCAS OpenIR > 中科院软件所 > 中科院软件所

	电子商务协议的形式化分析方法
	周典萃
专业	计算机应用技术
	1999
学位授予单位	中国科学院软件研究所
学位	博士
学位授予地点	中国科学院软件研究所
关键词	可追究性电子商务公平性形式化方法协议
摘要	近年来，电子商务协议的设计逐渐成为热点，可追究性和公平性是电子商务协议应遵循的两个重要原则，可追究性指电子商务协议必须具备这一机制，它迫使交易双方对自己的行为负有责任。缺乏可追究性，交易双方容易引起争议。公平性指如果交易成功，交易双方应该获得他们要取得的电子货物；或者，如果交易失败，交易双方谁也不能获得要取得的电子货物，过去在认证协议分析方面的经验[11]表明，协议设计是一个极度易出错的工作。因此Rajashekar Kailar提出了一种用于分析电子商务协议可追究性的形式化分析方法[5]。它是目前电子商务协议的主要形式化分析工具。本文分为两部分，前部分指出了Kailar形式化分析方法的三个缺陷：（1）不能分析协议的公平性；（2）列举初始化假设是非形式化的，不当地引入初始化假设会导致协议分析的失败；（3）无法理解包含有签过名的密文的协议语句。后部分进出了一种新的形式化分析方法。和Kailar形式分析方法相比较，新的形式化分析方法主要有三个优点：（1）能有效分析协议的公平性。在进行公平性分析时充分考虑了通信信道的可靠性；（2）初始化拥有集合只依赖于环境，不需要人为地引入初始化假设；（3）增加了密文理解规则，它能有效地分析包含有签过名的加密公式的消息。
其他摘要	The is a growing interest in the design and development of electronic commerce protocols. Accountibility and fairness are the two important rules that electronic commerce protocols must satisfy. Accountability is the ability to hold individuals or organizations accountable for transactions. Without such assurances, electronic transactions can be susceptible to disputes. Fairness means that if the transaction success, both principals of transaction get the items they except, or,in case of failure, neither do. However, protocols design has been extremely error prone by past experience with authentication protocols[11]. Therefore, Rajashekar Kailar has proposed a very important framework[5] for the analysis of electronic commerce protocols that require accountibility. This paper has divided into two parts. In the first part we point out that the framework that Kailar proposed needed to be improved in three aspects. Firstly, the framework cannot analyze fairness of protocols. Second, articulating initial state assumptions is an informal and error-prone step. At last, the messages with encrypted contents in the protocol cannot be interpreted. In the second part we proposed a new framework for the analysis of electronic commerce protocols. Comparing to the framework proposed by Kailar, our framework has three major improvement. Firstly, it can analyze fairness of protocols. In the analysis of fairness, it takes the reliable of commucation channels into consideration. Second, with a new postulate, it can handle the messages with encrypted contents. At last, the way of articulating principal's initial own sets is formal.
页数	33
语种	中文
内容类型	学位论文
URI标识	http://ir.iscas.ac.cn/handle/311060/6336
专题	中科院软件所_中科院软件所
推荐引用方式 GB/T 7714	周典萃. 电子商务协议的形式化分析方法[D]. 中国科学院软件研究所. 中国科学院软件研究所,1999.

条目包含的文件
文件名称/大小	文献类型	版本类型	开放类型	使用许可
LW002866.pdf（1635KB）			限制开放	--	请求全文