Verification of network security protocols

During recent years there has been considerable interest and growth in computer networks and distributed systems. Computer networks employ encryption for several purposes, including private communication, message authentication and digital signatures. The correctness and security of these applications depend not only on the strength of the cryptographic algorithms but also on the protocols for key management. In this paper, we analyse the behaviour of a "generic" key distribution protocol using a model checker based on temporal logic. The protocol typifies several protocols that have been recently proposed to achieve an authenticated communication in a network environment. The protocol is first specified using a state-machine-based language. Then some important properties of the protocol are verified. Such analysis technique is useful in a wide range of applications. In particular, we feel that the model checker helps to bring the automatic verification of finite systems closer to a practical proposition.