Abstract—Trivial File Transfer Protocol (TFTP) is a simple lockstep file transfer protocol. In this paper we use PAT, a model checker for CSP, to detect errors in the TFTP. We model the protocol and a very general intruder as CSP processes, and use the model checker to test whether the intruder can successfully attack the protocol. We discover many different attacks leading to breaches of security.
Index Terms—Security protocols, PAT, CSP, TFTP, model checking.
Lou Chen is with Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, Shanghai, China (e-mail: 51151500006@stu.ecnu.edu.cn).
[PDF]
Cite:Lou Chen, "Using CSP to Detect Errors in the TFTP," Journal of Advances in Computer Networks vol. 6, no. 1, pp. 24-29, 2018.