Research And Application Of The SAT-based Formal Analysis Methods For Security Protocols

Security protocols is a kind of communication protocol which provides security services in unsafe public network by means of cryptography technology, whose correctness and security has a crucial role in ensure the network information security. However, the design of security protocols is an extremely complex system engineering, even with the support of the security cryptographic algorithms, there is quite a possibility that some vulnerabilities and defects exit in security protocols. Therefore, the analysis and testing toward the protocols is necessary before it is widely used. Formal analysis can effectively test the security of target protocol, which has been acknowledged as a very reasonable and effective method in security protocol verification and design. Research on the formal analysis of practical security protocols and automatic detection technology has become an extremely important field of information security, which has important theoretical and practical application value.Based on the research and analysis of existing security protocol formal analysis methods, this thesis proposes a new method for security protocol model checking based on Boolean Satisfiability Problem, and taking advantage of it to do safety analysis on the security protocols in actual network environment. Detailed work is summarized as follows:1. A security protocol formal analysis method(SAT-LMC) based on Boolean Satisfiability Problem is proposed. The method uses variables remain and confuses the honest body with the attacker’s ability to get lazy protocol description in the initial state. Compared with the traditional protocol analysis tools, the initial state is greatly reduced, thereby the efficiency has been greatly enhanced; type flaw attack, parallel session attack and other attacks are added to the protocol rewriting rules, and lazy protocol rewrite rules are gain through variable remain and lazy attacker technology. Compared with the traditional protocol analysis tool, the method in this thesis applies term rewriting technique, which convertes protocol formal analysis problem to a protocol insecurity problem; then imports intelligent planning technology to graphics coding the protocol, and ultimately converts the problem to a Boolean satisfiability solving problem. Finally, on account of the existing shortage of the complete search algorithms and local search algorithms in solving Boolean Satisfiability Problem, a compound intermediate solution heuristic algorithm IS-CSAT has been designed. By combining the two algorithms, our algorithm maintains comprehensive serch algorithm completeness and the majority of instances have the local search algorithm efficiency characteristics.2. Based on the SAT-LMC protocol analysis method, the corresponding SAT-LMC Tool is implemented. The solving algorithm of Boolean Satisfiability Problem in the tool not only has the high efficiency of the traditional local search algorithms, but also has the advantages of the traditional global search algorithm, that can get comprehensive answers and can be falsifiable. Compared to traditional protocol formal analysis tools OFMC and SATMC, SAT-LMC Tool has a great speed advantage, higher detection efficiency, and more comprehensive attack detection ability while can detect type flaw attack and parallel session attack.3. The security of the cloud open authorization protocol OAuth2.0 is analyzed with SAT-LMC Tool. The protocol security in four secure channel scenarios are discussed respectively, and the corresponding attack paths under unsafe conditions are enumerated; in addition, taking Sina and Youku for example, implement a user account hijacking attack instance. The experimental result shows that the design and application of SAT-LMC Tool has great significance to the specification of network security environment.