Analysis And Improvement Of Protocol Vulnerability Based On Multiple Counterexamples

Model checking is a powerful method for verifying software and hardware systems.It first uses formal language to describe the system to be tested and the specifications that the system needs to meet,and then uses algorithms such as DFS(Depth First Search)to traverse the state space of the system model to find out those that do not meet the specifications and return counterexamples to guide system modification.However,the existing model checkers are all based on single counterexample,which often require multiple human interventions to complete the verification process when verifying the system.On the other hand,with the explosive growth of the number of users of various applications and platforms in the mobile Internet era,it is more and more common for people to authorize their information on a certain platform to third-party applications.As an open authorization protocol,the OAuth 2.0(Open Authorization)protocol is used by many domestic and foreign companies and applications such as We Chat,Google,Facebook,etc.as their information authorization solution.However,there is not much research on the security of the OAuth 2.0 protocol,and there are problems such as inaccurate modeling and low analysis efficiency.This thesis uses multiple counterexamples method to improves the well-known model checking tool SPIN(Simple Promela Interpreter),and uses the model learning method and the improved SPIN to analyze and research the OAuth 2.0 protocol.Specifically,the main work is as follows:(1)This thesis improves the model checker SPIN.SPIN is a model checking tool based on single counterexample.When SPIN is used for protocol verification,if a counterexample is found,it will automatically stop.It is necessary to manually modify the error that caused this counterexample and then re-verify the system to generate the next counterexample.This process is cumbersome.This thesis proposes a modification method to the SPIN verification process so that it can search for all counterexamples with only one verification.Aiming at the problem that there may be similar counterexamples in these counterexamples,this thesis draws on the measurement method of string similarity to reduce and eliminate similar counterexamples.This work simplifies the verification process of SPIN,improves its work efficiency,and has a positive effect on the analysis of other protocols and programs.(2)This thesis Uses the model learning method to model the OAuth 2.0 protocol.Modeling is the first step of the model checking method,and the accuracy of modeling directly affects the verification results.Compared with traditional manual analysis and modeling,model learning is a more efficient modeling method,which has the advantages of high degree of automation and accurate modeling.This thesis introduces the model learning method into the modeling process of OAuth 2.0 protocol for the first time and establishes the model of the protocol.(3)This thesis uses SPIN based on multiple counterexamples to verify the OAuth2.0 protocol.The verification result found that there is a vulnerability in this protocol.The attacker can obtain access token without the user's authorization,and then steal the user's protected resources.Aiming at this vulnerability,this thesis proposes an improved method to the OAuth 2.0 protocol flows.This method ensures security by adding authorization server identity information to the redirection address.Finally,the effectiveness of the improved method is verified through experiments.