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

以作者查詢圖書館館藏

、以作者查詢臺灣博碩士

、以作者查詢全國書目

、勘誤回報

、線上人數：28

、訪客IP：18.191.132.194

姓名

鍾佑祥(Yo-Shung Chung) 查詢紙本館藏

畢業系所

資訊管理學系

論文名稱

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

相關論文

★ 網路合作式協同教學設計平台－以國中九年一貫課程為例	★ 內容管理機制於常用問答集(FAQ)之應用
★ 行動多重代理人技術於排課系統之應用	★ 存取控制機制與國內資安規範之研究
★ 信用卡系統導入NFC手機交易機制探討	★ App應用在電子商務的推薦服務-以P公司為例
★ 建置服務導向系統改善生產之流程-以W公司PMS系統為例	★ NFC行動支付之TSM平台規劃與導入
★ 關鍵字行銷在半導體通路商運用-以G公司為例	★ 探討國內田徑競賽資訊系統－以103年全國大專田徑公開賽資訊系統為例
★ 航空地勤機坪作業盤櫃追蹤管理系統導入成效評估—以F公司為例	★ 導入資訊安全管理制度之資安管理成熟度研究－以B個案公司為例
★ 資料探勘技術在電影推薦上的應用研究-以F線上影音平台為例	★ BI視覺化工具運用於資安日誌分析—以S公司為例
★ 特權帳號登入行為即時分析系統之實證研究	★ 郵件系統異常使用行為偵測與處理-以T公司為例

檔案

[Endnote RIS 格式]

[Bibtex 格式]

[相關文章]

[文章引用]

[完整記錄]

[館藏目錄]

[檢視]

[下載]

本電子論文使用權限為同意立即開放。
已達開放權限電子全文僅授權使用者為學術研究之目的，進行個人非營利性質之檢索、閱讀、列印。
請遵守中華民國著作權法之相關規定，切勿任意重製、散佈、改作、轉貼、播送，以免觸法。

摘要(中)

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

關鍵字(中)

★ 線上交易協定
★ 正規驗證
★ 公平交易
★ 電子現金
★ FDR

關鍵字(英)

★ electronic cash
★ FDR
★ e-commerce protocol
★ formal verification
★ fair exchange

論文目次

第一章緒論 1
1.1 研究背景 1
1.2 研究動機 2
1.3 研究目的 3
1.4 研究方法 4
1.5 論文架構 5
第二章文獻探討 6
2.1 正規驗證（formal verification） 6
2.2 公平交易 9
2.3 驗證之協定 10
2.4 小結 15
第三章　CSP建模與FDR驗證 16
3.1 以CSP進行協定建模 16
3.2 以CSP進行特性建模 26
3.3 以FDR進行模型檢測 36
3.4 小結 42
第四章　不可靠環境下之建模與驗證 43
4.1 通訊管道故障 43
4.2 交易成員之系統故障 45
4.3 協定公平性分析與改善 47
4.4 小結 57
第五章結論與未來研究方向 58
5.1 結論與貢獻 58
5.2 未來研究方向 59
參考文獻 61
中文參考文獻 61
英文參考文獻 61
網頁資料 63

參考文獻

中文參考文獻
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

指導教授

林熙禎(Shi-Jen Lin)

審核日期

2008-7-17

推文