數位內容公平交易協定之正規驗證

Formal Verification of a Fair: Exchange Electronic Commerce Protocol for Digital Content Transactions

10.6382/JIM.200901.0018

林熙禎(Shi-Jen Lin)；鍾佑祥(Yo-Shang Chung)

線上交易協定 ； 正規驗證 ； 公平交易 ； 電子現金 ； FDR ； e-commerce protocol ； formal verification ； fair exchange ； electronic cash ； FDR

資訊管理學報

16卷_S期（2009 / 01 / 01）

153 - 164

繁體中文

電子商務日漸普及，藉由網路進行電子交易亦為一種熱門新興的購物模式。但由於此交易模式尚未成熟，雙方皆憂慮在虛幻的網路中損失自身權益，因此交易公平性之疑慮成為電子商務發展瓶頸。近代學者提出許多公平交易相關協定，並以協定分析方式列舉情境來證明協定滿足公平特性。然而，情境模擬的方式無法提供嚴謹之驗證，仍可能有百密一疏的例外情況發生。因此本研究提供一個嚴謹且兼具效率的方式，使用正規驗證(Formal Verification)中模型檢測(Model Checking)，運用CSP (Communicating Sequential Processes)語言，針對欲檢驗的協定及公平特性進行建模(Modeling)，再搭配FDR (Failures-Divergence Refinement)以有限狀態自動機結構(Finite Automata-like Structure)的概念做狀態集合的檢驗，偵測協定中的缺失，並檢驗協定是否完全滿足公平交易特性。

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 immature enough to convince the participants that they won't ever suffer the loss of money or interests through the virtual 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 can detect the failures of protocol and make sure if the protocol satisfied the fairness exactly.

1. Formal Systems (Europe) Ltd,"Failures-Divergence Refinement: FDR2 User Manual", 2005.
2. 孫鴻業，「美線上內容服務營收僅緩步成長 網路安全性為障礙」，FIND網路脈動，2006，http://www.find.org.tw/find/home.aspx?page
3. Anderson, B.B.,Hansen, James V.,Lowry, Paul Benjamin,Summers, Scott L.(2006).The application of model checing for securing e-commerce model checking is an effective component for performing online transactions that build customer trust and confidence.Communications of the ACM,49(6),97-101.
4. Gartner, F.C.,Pagnia, H.,Vogt, H.(1999).Approaching a formal definition of fairness in electronic commerce.Proceedings of the International Workshop on Electronic Commerce,Lausanne, Switzerland:
5. Grau, Jeffrey(2006).eMarketer ReportseMarketer Reports,未出版
6. Kim, I.G.,Choi, J.Y.(2005).Model Checking of RADIUS Protocol inWireless Networks.IEICE Trans. Commun,E88-B(1),397-398.
7. Lin, S.J.,Liu, D.C.(2007).A Fair-Exchange and Customer-Anonymity Electronic Commerce Protocol for Digital Content Transactions.Lecture Notes in Computer Science,4882,321-326.
8. Lowe, G.(1996).Breaking and fixing the Needham-Schroeder public-key protocol using FDR.Proc. TACAS
9. Muller-Olm, Markus,Schmidt, David,Steffen, Bernhard(1999).Model-Checking a Tutorial Introduction.SAS'99
10. Ray, Indrakshi,Ray, Indrajit(2000).Failure Analysis of an E-commerce Protocol Using Model Checking.Proceedings of the Second International Workshop on Advanced Issues of E-Commerce and Web-based Information Systems,Milpitas, CA:
11. Wang, F.(2004).Formal Verification of Timed Systems: A Survey and Perspective.Proceedings of the IEEE,92(8),1283-1307.