The Automatic Analysis System For Network Authentication Protocols

The analysis and verification of authenticated protocol is an important field in the security of computer nowadays. The security analysis of protocol includes informal method and formal method, and the formal method is the main way for analysis protocols. We exploited the automatic analysis system for the authentication protocols of network security on the basis of analysis the formal modeling process for many protocols, regarding authenticated protocols of network security as research object and adopting the model checking technique. The main function of the system is that it can automatically model and verify for authenticated protocols. The system includes user's interface module, automatic analysis modeling module and automatic verification module. The user's interface module is responsible for providing a intuitionsitic GUI interface in order that user may input the protocol, which come into the system's acceptable language-PDL; The automatic analysis modeling module has designed the formal analysis arithmetic for authenticated protocols and it can carry out the modeling and property guide for these protocols; The automatic verification module embeds the SPIN and automatically verifies the modeling process and return verification results. The system has finished the automatic modeling and verification for those protocols which belong to the Bilateral Public Key type or the Tripartite Symmetry Key type, and successfully found the flaws of N-S protocol, TMN protocol and Hersinki protocol. Aim at the problem of state exploding, many optimized policies have been adopted in the system, such as atomic and steps, order redirection, cutting down the span of variable and partial specification. The experimental results indicate the system is more effective on condition that optimized policies exist. Furthermore, the innovations of the system represent abstract, efficiency, automatization, expansibility and friendly user interface. The system possesses the better value of application, and it is the effective analysis, evaluation tool for network communication system which is as the core of network authenticated protocols.