The Automatic Verification and Improvement of SET Protocol Model with SMV

In order to make secure transactions over networks, various protocols have been proposed, but there are subtleties involved in original protocol design, some of them have been found after a long time after publication. In this paper, we used model checking method by means of SMV to verify SET protocol in electronic commerce. Model checking combines some of the advantages of both testing and theorem proving. Other advantages include that model checking can start once the first prototype of the model and specification have been finished. The symbolic model checking ware (SMV) was applied for analyzing the authentication, confidentiality and integrity of SET protocol, attacks were found. Then, the influence of attacks was discussed. Finally, the protocol model was optimized. The result of analyzation and checking indicates the importance of dual signature on SET protocol.