Optimization of anonymous e-cash payment protocol and its formal verification
优化的匿名电子现金支付协议及其形式化验证

In response on the existing problems of anonymous e-cash payment protocol, the paper proposed an optimal protocol, which could meet a variety of security properties. To ensure the realization of its key confidentiality, the agreement and use of the session key were divided into two stages. To realize its non-repudiation, the certificates were used to prove the identities of the transaction entities. To avoid unfairness arisen by the dishonest transaction entities, the transmission of payment receipt was achieved by the trusted party. The proposed protocol used FTP to transmit electronic cashes and payment receipts, which ensured achievement of accountability and fairness, and enhanced the robustness of the protocol. Formal verification results indicate that the optimal protocol satisfies key confidentiality, non-repudiation, accountability, fairness and atomicity.