Research On Formal Verification Methods Of Security Protocols

Working as a kind of kernel technology for the secure network communication, the security protocols are the foundation in building up a safe internet environment. Therefore, the correctness and security of protocols play a crucial role in network environment. However, it remains to be solved on the security and design of the protocols to better meet the demands of the safety. A formalized method, thereafter, has been proved to be effective in analyzing and testing verification of the protocols, which so far has become a focus in the field of formal study.Although the formal method has succeeded in finding flaws and attacks of many security protocols, it still suffers from lots of problems, such as the faultiness of the formal method itself, which can not suit the verification of some security protocols. On the other hand, some others can only presume the insecurity of cryptographic protocols rather than the credible verification of security objectives.In terms of the causes and attacking methods accordingly, there are 7 types of deficiencies, i.e. protocol deficiency, password/key deficiency, outdated information deficiency, internal protocol deficiency, parallel communication deficiency, code system deficiency and other deficiencies. In the meanwhile, 6 types of attacks in security protocols have been classified: information-reissuing attacking, presuming attacking, code-analyzing attacking, parallel communication attacking, type deficiency attacking and binding attacking.BAN logic, the foundation of the logic analysis, put forward by Burrow, Abadi and Needham, forms the landmark in analyzing security protocols. However, the narrow definition of symbol muster proves that there are some deficiencies which can not be analyzed, for the reasoning method of BAN logic is as a matter of fact abstracted from the real protocol analysis method and the symbol cluster of the logic process is abstracted from the real protocols. For example, it can not analyze the protocol deficiency by time synchronization, or it can not analyze the protocol with special password conversion method, etc. Besides, many illogic initial presumptions exist in BAN logic, which limits seriously the method into practice. Take the presumption that the news can not be forged as an example. Finally, some other deficiencies exist in BAN logic: non- standard idealized process deficiency, reasoning rule deficiency, lacking-in-clear- semantic deficiency, lacking-in-environment-model deficiency and lacking-in-effective-exploring -attacking deficiency, etcAs an important logic in studying and analyzing electronic business protocols, Kailar logic has flaws as follows: 1) Kailar logic can only study the pursuitability rather than the impartiality of the protocol; 2) As some presumptions will be introduced before the reasoning of Kailar logic, which is a non-standard process, improper introduction of presumption, therefore, will lead to the failure of protocol analysis; 3) The applicable range could be restricted when Kailar logic can only explain those signatory explicit information.To sum up, a new logic of security protocol analysis---CPL, that is, Cryptographic Protocols Logic---has been designed, which can not only analyze but also design the security protocols. Thus, the new logic integrates the analysis and design into one logic frame, avoiding the potential disagreement owing to the different methods in analyzing and designing, simplifying the steps of initialized conditions and objectives in the formalized process of analyzing and designing security protocol, improving the efficiency of the analyzing and designing. CPL gives the primary symbols, reasoning and composition rules, among of which, the two rules can be used in analyzing and designing respectively in security protocols. The analysis process of the security protocols can test the safety of the protocol by way of the reasoning rules and initialized conditions and executive steps in analyzing the security of the protocols. The design process can design the security protocols by way of the composition rules and initialized conditions and objectives in protocol operation. Two kinds of protocols, i.e. password protocols and identification protocols have been illustrated on the basis of the new logic.