Formalization And Analysis Of TFTP Based On CSP

With the rapid development of computer networks and communication technologies,information configuration and hardware back-up of network devices as well as software back-up and quick recovery of Internetwork Operating System(IOS)have become the basic conditions for the normal operation of modern network systems.Because of the simple design of Trivial File Transfer Protocol(TFTP),the effect of file transfer can be easily realized by code.Most of the underlying implementation of network device configuration and back-up function are based on the TFTP.As a simple file transfer protocol,TFTP allows the client to get a files from remote hosts or put files onto the remote hosts,and it is mainly used for booting the file acquisition when the network devices start the boot.Since the protocol has been put forward,the research work is rarely done on it from the view of the formal methods.Due to the lack of the formalized models,the security of the TFTP is often ignored,and the events that use the protocol for computer virus propagation take place frequently.We establish a formal model for TFTP in Communicating Sequential Processes(CSP)and also analyze its property in this thesis.First,the message data of the communication in the TFTP protocol is modeled,and different models are used for different types of messages.We have three components in our model: server,client and resource.Each of them is modeled as a CSP process and uses a corresponding channel to specify the behavior of receiving and sending messages.At the same time,intruder is added to the model.Intruder is a process that can fake or intercept messages based on known facts.So our system model consists of the above four components.We also describe the properties of the TFTP as a set of specifications and verify these properties by using the model checker PAT.Finally,a case study is given to illustrate the correctness and rationality of our model.The modeling and analysis of the TFPT can help the industry to understand the protocol better,and the verification of its properties can cause more attention to the security of the TFPT.