The Research Of System, Rules And Checking Of Protocol Based On TLA

Aiming to ensure the software system's credibility and safety radically, many computer scientists, including A. PnDeli who is a gainer of Turing Award, believe it is a important way to construct safety software with validating and analyzing the system by formal methods. Model checking technology is one of validating ways.Formal methods use mathematic and logic method to describe and validate the system. Its description includes two aspects. One, which is also called modeling, is the description of systematic behavior. It describes the system and behavior mode through the model with systematic structure. The other one, which is also called specification, is systematic property. It shows the property which the system has, such as safety property, liveness property and so on. These properties can be described by one or several specifications which include proposition logic, liner logic, algebra, course algebra, special process language, subset of process language and so on.Temporal Logic of Actions (TLA) is brought forward by Leslie Lamport. And its syntax and complete formal semantics are summarized in about a page. TLA is extremely powerful, both in principle and in practice. And TLA+ is a specification language based on TLA, TLC is checking tool which is developed by Compaq Corporation and Microsoft Corporation.In the research, we carry on from three directions, the first direction is conducts the thorough research to theory of TLA, and want to get ahead in theories by hard work; The second direction is carries on the formal specification and checking of the reality system; The third direction is carries on the formal specification and checking of network protocol. Through, all has diligently obtained certain understanding in three directions, but also has many research works to need to continue and to strengthen.We do the works as follows:Firstly, in researching of concurrent system based on TLA, the question of states transition and the properties is a research branch. Always we check the properties of the concurrent system after system transfer. But we thought add the property into the transition system this time, that is to say the system has the property before transfer, and so the system has some properties from beginning to the end. For this purpose we bring forwards some concepts, such as transition condition, controllable action, controllable state, and controllable transition system, in addition we give the theorems and prove them. Then formalizing Internet banking based on TLA+ and checking it using TLC. The results show the theories are appropriate.These definitions need to be proved. We specify several concurrent systems, such as the clock system, the elevator system, Needham-Schroeder protocol and check these systems. The results show the theories are appropriate.Secondly, safety property is a important property of transition system, and we put forward safety transition system based on controlled transition system. When we specified the Internet banking system, we find that 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 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 conformation, 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.Thirdly, specifying and checking systems, its main purpose was carries on the liveness properties . Leslie Lamport has put forward liveness rules based on the TLA, but we found in some systems such as multi-clients in network, multi-users under a count in Internet banking the Leslie Lamport's liveness rules could not use.Based on Lamport's liveness rules , we put forward multi-actor liveness rules under weak and strong fairness and prove them, the example of multi-user's mutually exclusive action of drawing out in Internet bank based TLA+ to check the rules, and then we put forward multi-actor property liveness rules in safety transition system and use the example of multi-user's mutually exclusive action of drawing out in safety Internet bank based TLA+ to check the rules.Finally, based on TLA the AVISPA stands for automated validation of Internet security protocols and Applications and the AVISPA Project is funded by the European Union. The AVISPA project aims at developing a push-button and industrial-strength technology for the analysis of large-scale Internet security- sensitive protocols and applications. System models are written in the high level protocol specification language (HLPSL). We specified the Kerberos protocol four steps model and six step models based on HLPSL, and through the checking we found the model was unsafe under certain condition, and the attack steps was given by the tool.Another checking tool TLC2.0 was developed by Compaq and Microsoft Corporation in 2003, the tool use the TLA+ description language. We specified Neeham-Sehroeder protocol based on TLA+, and through the TLC checking we found the protocol could be broken in by hacker under certain condition.We compared the TLA+ language with the HLPSL language, and found on the one hand, the TLA+ language need write more code than the HLPSL language and is better on system specification, that is to say we should know fairly well with TLA+ in heart, on the other the HLPSL is more powerful than the TLA+ language in protocol checking because: many function has been written by HLPSL, and so we would do more work to research and compare these famous examination tool SPIN, SMV and so on.