Formal Analysis, Design And Verification On Complex Security Protocols

Security protocol is a very important role in securing network communication, and the formal analysis method for security protocol becomes one of the hottest research topics in security field. Meantime, PKI has been applied in various commercial network environments as a perfect security guarantee, and so many complex security protocols based on PKI application are also on hot way, in which SSL protocol is a most typical one. However, using formal method based on reasoning logic to analyze complex security protocols such as SSL is not so efficient at present. So, the research topic in this paper is to present a new analysis way based on formal method to analyze and design complex security protocols.It's essential that complex security protocols can be obtained through the continues evolution of simple protocols, therefore, the Evolution Model Framework for security protocol based on algebraic specification is presented in this paper, the body of a security protocol can be formalized using this framework and the goal of a security protocol's evolution can be attained by expanding this framework. In this paper, the belief logic system GNY and it's related implementation tool SPEARII are utilized, SSL protocol is a focused instance, then the detailed analysis procedure from initial protocol model to various evolution protocol models is given, later the final evolution protocol model and SSL protocol are contrasted and thus the security analysis conclusion is drawn for SSL. During the analysis procedure two practical security authentication solutions are designed based on evolution protocol models. So, the evolution protocol model is not only useful to analyze complex protocols but also to design protocols. Furthermore, three expanded GNY logic rules are given during above analysis based on GNY, and at the end of this paper, security protocol formal verification based on attack logics is discussed and presented, a development framework of integrating such verification model into automated analysis tools such as SPEARII is shown finally.