電子商務日漸普及，藉由網路進行電子交易亦為一種熱門新興的購物模式。但由於此交易模式尚未成熟，雙方皆憂慮在虛無的網路中損失自身權益，因此交易公平性之疑慮成為電子商務發展瓶頸。近代學者提出許多公平交易相關協定，並以協定分析方式列舉情境來證明協定滿足公平特性。然而，情境模擬的方式無法提供嚴謹之驗證，仍可能有百密一疏的例外情況發生。
因此本文使用嚴謹且兼具效率的正規驗證（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.

中文參考文獻
1. 林水順、莊英慎，電子商務－企業電子化觀點，高立圖書，民94。
2. 高志中，「以DR Signature配合隨機式RSA部分盲簽章所建構之數位內容多受款者付款機制」，國立中央大學資訊管理研究所，碩士論文，民95。
3. 施凱耀，「網格計算中以代理人為基礎之公平交易機制」，國立中央大學資訊管理研究所，碩士論文，民96。
英文參考文獻
4. Adi, K., Debbabi, M., & Mejri, M. (2003). A new logic for electronic commerce protocols. Theoretical Computer Science, 291(3), 223-283.
5. Anderson, B. B., Hansen, J. V., Lowry, P. B., & Summers, S. L. (2006). The application of model checking for securing e-commerce transactions. Communications of the ACM, 49(6), 97-101.
6. Anderson, B. B., Hansen, J. V., Lowry, P. B., & Summers, S. L. (2006). Standards and verification for fair-exchange and atomicity in e-commerce transactions. Information Sciences, 176(8), 1045-1066.
7. Burch, J. R., Clarke, E. M., McMillan, K. L., Dill, D. L., & Hwang, L. J. (1990). Symbolic model checking: 10 20 states and beyond. Logic in Computer Science, 1990.LICS''90, Proceedings., Fifth Annual IEEE Symposium on e, , 428-439.
8. Clarke, E. M., & Wing, J. M. (1996). Formal methods: State of the art and future directions. ACM Computing Surveys (CSUR), 28(4), 626-643.
9. Gartner, F. C., Pagnia, H., & Vogt, H. (1999). Approaching a formal definition of fairness in electronic commerce. Proceedings of the 18th IEEE Symposium on Reliable Distributed Systems (Workshop on Electronic Commerce), , 354-359.
10. Goldsmith, M. (2005). FDR2 user''s manual version 2.82. Formal Systems (Europe) Ltd.
11. Heintze, N., Tygar, J. D., Wing, J., & Wong, H. C. (1996). Model checking electronic commerce protocols. Proceedings of the 2nd Conference on Proceedings of the Second USENIX Workshop on Electronic Commerce-Volume 2 Table of Contents, , 10-10.
12. Kim, I. G., & Choi, J. Y. (2004). Formal verification of PAP and EAP-MD5 protocols in wireless networks: FDR model checking. Advanced Information Networking and Applications, 2004.AINA 2004.18th International Conference on, 2
13. Lin, S., & Liu, D. (2007). A fair-exchange and customer-anonymity electronic commerce protocol for digital content transactions. LECTURE NOTES IN COMPUTER SCIENCE, 4882, 321.
14. Lowe, G. (1996). Breaking and fixing the needham-schroeder public-key protocol using FDR. Software - Concepts and Tools, 17(3), 93-102.
15. Müller-Olm, M., Schmidt, D. A., & Steffen, B. (1999). Model-checking: A tutorial introduction. Proceedings of the 6th International Symposium on Static Analysis, , 330-354.
16. Ranganathan, C., & Ganapathy, S. (2002). Key dimensions of business-to-consumer web sites. Information & Management, 39(6), 457-465.
17. Ray, I. (2000). Failure analysis of an e-commerce protocol using model checking. Advanced Issues of E-Commerce and Web-Based Information Systems, 2000.WECWIS 2000.Second International Workshop on, , 176-183.
18. Ray, I., & Ray, I. (2000). An optimistic fair exchange E-commerce protocol with automated dispute resolution. Proceedings of the 1st International Conference on Electronic Commerce and Web Technologies,
19. Tsiakis, T., & Sthephanides, G. (2005). The concept of security and trust in electronic payments. Computers & Security, 24(1), 10-15.
20. Vogt, H., Gärtner, F. C., & Pagnia, H. (2003). Supporting fair exchange in mobile environments. Mobile Networks and Applications, 8(2), 127-136.
21. Wang, F. (2004). Formal verification of timed systems: A survey and perspective. Proceedings of the IEEE, 92(8), 1283-1305.
網頁資料
22. Computer Industry Almanac Inc, “Worldwide Internet Users Top 1.2 Billion in 2006,” February 12, 2007. http://www.c-i-a.com/pr0207.htm
23. Jeffrey Grau, “Online Privacy and Security: The Fear Factor,” eMarketer Reports, April 2006. http://www.emarketer.com/Report.aspx?privacy_retail_apr06
24. Linda Rosencrance, “E-commerce fraud rises to $2.8 billion,” TECHWORLD, November 11, 2005. http://www.techworld.com/security/news/index.cfm?NewsID=4773&inkc=0
25. 中國投資諮詢網，「2008年中國電子支付市場分析及投資諮詢報告」，2008年1月。http://www.econet.com.cn/reports/2006391dianzizhifu.htm
26. 孫鴻業，「美線上內容服務營收僅緩步成長 網路安全性為障礙」，FIND 網路脈動，2006年3月。http://www.find.org.tw/find/home.aspx?page=news&id=4195
27. 財團法人台灣網路資訊中心（TWNIC），「2008年台灣寬頻網路使用調查」，2008年2月。http://www.twnic.net.tw/download/200307/0801a.doc
28. 財團法人資訊工業策進會產業支援處，「2007 數位內容產業年鑑」，2007年。http://www.digitalcontent.org.tw/2007/index.htm
29. 張玉霜，「2005年美國消費者線上交易總額突破800億美元」，FIND 網路脈動，2005年12月。http://www.find.org.tw/find/home.aspx?page=news&id=4079
30. 資策會市場情報中心（MIC），「2007台灣電子商店發展趨勢」，2007年10月。http://mic.iii.org.tw/index.asp