Analysis and Checking of Safety Transition System Based on TLA+

With all viruses and computer hackers, online banking security especially the process of payment could not be protected. The majority banks adopt many methods to guarantee the security, but if someone gets the account number and password, he can do anything in Internet and the bank has little way to prevent. So we need greater security in the process of payment. TLA is One kind of logic brought forward by Leslie Lamport[1]. And its syntax and complete formal semantics are summarized in about a page. TLA is extremely powerful, both in principle and in practice. Yet, there have no theory about safety transition system in it. And then we put forward the definitions of safety state, safety transition condition, safety action, safety run, safety transition system and the theorem which proof that every state in safety transition system is safe; then, specify Internet banking using TLA+ which is based on safety transition system. In the specification several accounts and the intruder are in a concurrency system, they communicate through a channel, and the specification is tested by TLC. The results show that the system based on safety transition is more secure.