Abstract: Both the finite state model and the CTL (Computation Tree Logic) formulations were first constructed for the secure e-commerce payment protocol based on four parties (FSE7)in this paper. Then, the symbolic model checking (SMV) was used to analyze and verify the atomicity of the FSET protocol. I}he result of analysis and verification indicafes that the FSET can meet with the money atomicity, the goods atomicity and the certified delivery, as well as the elegy tromc payment security requmements.

Key words: E-commerce payment protocol, Model checking, SMV, Atomicity