Analysis And Studying Of Authentication Protocols

Authentication protocols are the foundation for the security of communication. It is very difficult to design and analysis authentication protocols. These protocols can be flawed in very subtle ways. How to develop authentication protocols so that they are secure? Formal approaches should be taken to the analysis of authentication protocols. Model checking approaches to the analysis of authentication protocols has proved be a very successful formal approach. We adopt NuSMV as the model checker to analysis authentication protocols. NuSMV supports Linear-time Temporal Logic.We will present sufficient conditions on protocols and their environment such that if the protocol is small system secure, then the protocols is secure in the sense that there is no attack on any system. In other words, for such protocols, model checking is complete. We modify some protocols to make them satisfy a number of conditions, and we analysis these protocols upon a small system. Last, we develop a kind possible of method of designing authentication protocols. The method advise us to design a authentication protocol and if the protocol is secure upon an small system, we believe that the authentication protocol is secure. We design test protocols advised the possible method and we use NuSMV to analysis it. Test protocol is secure on a small system.