Improvement and Model Checking of Micro-Payment Protocol Millicent

To solve the defect of the potential security risk caused by emphasizing the efficiency in the traditional mobile micro-payment protocol, according to the security that the mobile electronic business should have, the paper studies the mobile micro-payment protocol Millicent and discovers that it cheats customers. For the sake of the shortage, increasing the confirmation process between Vendor and Custom makes the protocol non-repudiate. Finally, the improved mobile micro-payment protocol Millicent is modeled and is analyzed with the model checking tool SMV. The analysis results show that the improved protocol owns non-repudiation and fairness besides possessing private and authenticating of the former, so it is better.