| Summary: | 碩士 === 國立中央大學 === 資訊管理研究所 === 96 === 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.
|
|---|
