Abstract: A secure electronic transaction formal model was given, which technical method of analyzing correlative security protocols automatically. showed the theoretic basis and The model was based on term rewriting, which described the three main process of electric transaction by symbols and rules, and satisfied the bidirectional authentication of the security mechanism. It showed some properties of the new model, proved the integrity and consistency by termination and confluece of rewriting system, and validated the authentication and non-repudiation of origin in the analyzing of security.