A Research On Analysis And Implementation Of Security Protocol With Counterexamples

As the Internet is more and more widely used in people's life,network security is becoming more and more important.As an important part of information security,the analysis of security protocol is of vital importance.At present,there are many methods to analyze security protocols.As a formal method,model checking is widely used to analyze security protocols.Based on the counterexamples generated by the model checker,this thesis analyzes the security protocol and finds the attack path of the protocol.Compared with other formal methods,model checking has many advantages.Model checking is a highly automatic technology,which makes the analysis of system easier.When the model violates the system specification,the model checker will generate a path from the initial state of the system to the violation state,that is,the counterexample.However,the counterexamples generated by model checker show high similarity,which makes the analysis of counterexamples difficult.In the process of model checker detecting protocol model,the modeling of protocol is particularly important.This thesis models NSPK protocol with promela modeling language,and analyzes the security properties that the protocol model needs to meet.Several counterexamples are found after we analyze the protocol model with model checker SPIN.In order to solve the problem of data similarity among many counterexamples generated by model detector,this thesis uses the equivalence class of counterexamples to simplify multiple counterexamples.This method ensures that the equivalence class of every counterexample contains only one counterexample,so each counterexample in the reduced counterexample set represents a different counterexample path.Our method reduces the number of counterexamples and improves the efficiency of the system.The set of the counterexamples is the base of analyzing multiple counterexample.Researchers often use single counterexample to analyze security protocol.But single counterexample contains too little information to find system errors correctly.In order to solve this problem,this thesis analyzes the security protocol with multiple counterexample.Multiple counterexample contains much more information than single counterexample,thus the system errors can be located much faster.We use the Tarantulastatistical method to calculate the frequency of statements in the counterexample and the anomaly value of the statements.Finally,we find the counterexample which may contain the error of the protocol model and find the attack path of the security protocol according to the counterexample.Compared with the original model checker SPIN,the method in this thesis adds counterexamples reduction and counterexamples analysis.Taking NSPK protocol as an example,this method reduces 1809 counterexamples generated by SPIN to 13,and increases the system running time from 0.67 seconds to0.31 seconds.Finally,according to the analysis results of the counterexample,we find that there is a vulnerability in the protocol without adding the identifier of both sides of the protocol communication.