Formally modelling is an efficient way for designing the high confidential computer system. So it is meaningful to formally analyze the e-commerce systems. By timed automata, this article specifies the SNPP, an e-commerce online payment protocol, and analyzes the properties of its implementation model. This work is helpful for designing an e-commerce protocol and a trustworthy e-commerce system.
展开▼
