Vulnerability Mining Of Security Protocol Based On Counterexample

Today,China has entered an era of Internet plus,and all industries have taken the Internet Express.As an important factor related to the security of information circulated through Internet,security protocol is very important.At present,there are many methods to analyze protocols.As a formal method,model checking has been w-idely concerned and recognized.On the basis of previous modeling and verification,this paper extends the counter-example analysis stage.This thesis tries to extract effective information from counterexamples and locate the vulnerabilities by analyzing counterexamples.Model checking has two main advantages.Firstly,model checking is highly automated,which can free researchers from complex search tasks.Secondly,when the system or protocol does not satisfy the agreed properties,the model checker can return a sequence of events at the source level,which is counterexample.Therefore,model checking method has been widely used in protocol verification field.With the increase and improvement of functions,the existing systems and protocols become more and more complex.As a result,the corresponding counterexamples are more and more numerous and the content is more and more complex,so it is more and more difficult to analyze so many counterexamples.In this thesis,a method of eliminating many similar counterexamples is proposed.When using model checker to verify the protocol,we find that there will be a large number of similar counterexamples,which reflect the same security vulnerability,but we only need one of these counterexamples.It will increase the burden of the system and interfere with the process of analyzing counterexamples,if there are too many counterexamples.In this thesis,the node weight method is introduced to eliminate similar counterexamples when counterexamples are generated.In order to ensure the de-similar effect,the elimination process of the post-generation stage of counterexamples is added into the system.This ensures that there are no similar Counterexamples in the set.Counterexamples contain abundant information about vulnerabilities.In order to quickly mine protocol vulnerabilities,we propose a multi-counterexamples based vulnerability mining method.After eliminating similar counterexamples,we need to analyze counterexamples.Because of the long length and mixed content ofcounterexamples,it is difficult to extract effective information of counterexamples.In order to make full use of the information in counterexamples,we use the statistical method turatula and distance measurement technology in the analysis of many counterexamples.Turantula technology can count the frequency of statements in counterexamples,generate a table of suspicions of statements,and analyze these statements in turn from the beginning of the table.In the analysis of each statement,distance measurement technology is used to find the closest successful execution path in the state space to the counterexample.By analyzing and comparing the differences between them,the vulnerabilities are finally located.The modeling,model verification and vulnerability mining of this system are based on Spin and ispin.we integrated these algorithms into our system which improved Spin and ispin Finally,the correctness and efficiency of the system are evaluated by experiments.