Specifying and checking network protocol based on TLA

Network protocol vulnerability detection is paramount to network security. Formalization provides an important way for vulnerability detection. In this paper, we apply TLA, which is a powerful tool for formal analysis, to analyze network protocols. An approach is proposed that aims to detect vulnerabilities of a protocol effectively with the TLA, with the Kerberos protocol being taken as an example. Firstly, roles for the protocol, especially those related to intruders, are created. Then actions of the roles are specified. Sessions among the roles are built. And environment parameters are set. A prototype program is developed to implement the approach, which covers the model and the detection properties of the protocol. Experiments show that our approach is effective and powerful in specifying and checking a protocol, and it is better than SPIN and SMV.