The Effective Analysis System Of Network Security Protocol

The security of network security protocol is an important basis of network safety. The security analysis and verification of security protocol is one of the most important research subjects and research focus in the field of computer security. Formal method is one of the major approaches to security protocol analysis. At present, the commonly used formal methods include Logic Reasoning, Model Checking, Theorem Proving, and so on. As an automatic technique for analyzing, verifying and improving the software and hardware system's safety and reliability, especially that of the Safety-Critical, Model Checking receives much attention. Focusing on the Formal Analysis of Security Protocol in the leading position, the thesis studies the technique of automatic analysis and verification, basing the research on the technique of model checking. The following are the main results:1. In order to facilitate the computer's automatic analysis of security protocol, the author analyzes and verifies numerous cases of security protocol, and finally sums up the general modeling algorithms of the protocol as well as its storage data structure.2. The semantic description ability of the Protocol Description Language PDL proposed in extending bibliography [1] entitles the protocol with a stronger descriptive ability and makes it more versatile.3. In protocol modeling, the atomic sequence of atomic and d_step is used together with such optimization strategies as Partial Order Reduction, Syntax Reordering and Type Checking to improve the efficiency of verification. This effectively eases the problem of state explosion in model checking.4. The author succeeds in designing an automatic analysis system of network security protocol, called the "The Automatic Analysis System of Security protocol". This system can make an automatic analysis of the Authentication Protocol and that of E-Commerce Protocol with a credible third-party, to check if there are loopholes in the protocol. If such loopholes are found, the system can display graphical path of the attack. This system is highly practical and can be used as effective aiding tools for network safety assessment and security protocol design.