數位內容公平交易協定之正規驗證; Formal Verification of a Fair-exchange Electronic Commerce Protocol for Digital Content Transactions

NCU Institutional Repository > 管理學院 > 資訊管理研究所 > 博碩士論文 > Item 987654321/13416

jsp.display-item.identifier=請使用永久網址來引用或連結此文件: http://ir.lib.ncu.edu.tw/handle/987654321/13416

题名:	數位內容公平交易協定之正規驗證;Formal Verification of a Fair-exchange Electronic Commerce Protocol for Digital Content Transactions
作者:	鍾佑祥;Yo-Shung Chung
贡献者:	資訊管理研究所
关键词:	線上交易協定;正規驗證;公平交易;電子現金;FDR;electronic cash;FDR;e-commerce protocol;formal verification;fair exchange
日期:	2008-07-04
上传时间:	2009-09-22 15:31:19 (UTC+8)
出版者:	國立中央大學圖書館
摘要:	電子商務日漸普及，藉由網路進行電子交易亦為一種熱門新興的購物模式。但由於此交易模式尚未成熟，雙方皆憂慮在虛無的網路中損失自身權益，因此交易公平性之疑慮成為電子商務發展瓶頸。近代學者提出許多公平交易相關協定，並以協定分析方式列舉情境來證明協定滿足公平特性。然而，情境模擬的方式無法提供嚴謹之驗證，仍可能有百密一疏的例外情況發生。因此本文使用嚴謹且兼具效率的正規驗證（formal verification）方式，使用模型檢測（model checking），運用CSP（Communicating Sequential Processes）語言，針對欲檢驗的協定及公平特性進行建模（modeling），再搭配FDR（Failures-Divergence Refinement）以有限狀態自動機結構（finite automata-like structure）的概念做狀態集合的檢驗，檢驗協定是否完全滿足金錢原子性（money atomicity）、貨品原子性（goods atomicity）、有效接收性（validated receipt）與有效傳送性（validated sending）四種公平交易特性。最後佐以網路斷線、交易成員系統故障等不可靠環境，並加入自動逾時機制予以補強後重新驗證，進行更周全的公平性分析。 Due to the growing popularity of e-commerce, electronic transactions through the Internet become one of the popular new shopping models. However, this model is not mature enough to convince the participants that they won’t ever suffer the loss of money or interests through Internet dealing, so the fairness become the sticking point of e-commerce. Actually, many researchers propose some fair-exchange protocol lately, but they prove the fairness of their protocols by simulation and test including a few inevitable exceptions which can’t provide a rigorous proof. Therefore, we provide a strict but efficient method by the model checking of formal verification. First, we model the protocol and the desired fair properties by CSP (Communicating Sequential Processes). Second, we verify the variety of all the states by FDR (Failures-Divergence Refinement) based on the finite state machine concept. Then we analyze the security of e-commerce protocols in failure environments using the model checking approach to make sure if the protocol satisfied the four fairness properties included money atomicity, goods atomicity, validated receipt and validated sending exactly.
显示于类别:	[資訊管理研究所] 博碩士論文

文件中的档案:

档案	大小	格式	浏览次数

在NCUIR中所有的数据项都受到原著作权保护.

社群 sharing

数据加载中.....