Formalizing and Checking SET Protocol Based on TLA

Leslie Lampor proposed the theory of Temporal Logic of Actions(TLA),which can express model program and logical rules in one language at the same time. Secure Electronic Transaction(SET) is an secure protocol for e-commerce, Based on the open network and paying with credit card. The agreement defines the whole process of the internet transactions. And it has a complete authentication. Based on the TLA, We made a series of operation to the SET, as model analysis, logical description, program description and Detection Analysis. We come to a conclusion that there is an atomicity problem of the value of transactions of the SET transaction process.