Research On Reconciling Two Views Of Formal Analysis Methods For Security Protocols

With the development of computer networks and the rise and extensive applications of Electronic Commerce, security requirements of networks become more and more urgent. In the area of network security, all kinds of security services are guaranteed by security protocol, hence, the security of the protocols become very important. In the past twenty years, a lot of security protocols were proposed, but, later researches show that there were many shortcuts in these known security protocols. Therefore, how to design a security protocol, and how to carry out formal analysis to a exited security protocol become two of the most important branches in the research area of security protocol.Security protocol is a process in which two or more participants take a series of steps to achieve a particular security task. Now there are two distinct views in the formal analysis of security protocol: Symbolic view and computational view. The symbolic view generally does not consider the specific cryptographic algorithm, but see the message as symbol having special meaning, then analyze the protocol whether it could achieve the anticipative goal using formal logic and theorem proof. On the other hand, the computational view defines the security of a protocol in the way of probability and time complexity, and the formal proof always prove a mathematic theorem. One commonly use reduction transformations to reduce the security to a hard problem in the computational complexity.Our primary work includes:1) We give a systemic introduction of the relative knowledge in security protocol, includes definition of security protocol, properties and sorts. After analyzing common attack methods on security protocol, we conclude some important principles in design of security protocol.2) We take the BAN logic for instance to introduce the deduction method under the symbolic view. Our work is improving the Yahalom protocol and analyzing the protocol using the BAN logic. Then, we take the works by Bellare and Rogaway for instance to introduce the analysis method which always reduces to a contradiction under the computational view. 3) We introduce a reconciling formal analysis methods proposed by Zhao Huawei and Li Daxing. After that, we discuss the application of timestamps in security protocol. Our work is improving the reconciling methods and adding timestamp semantics to it, so that it can be used to analyze the security protocol with timestamps.4) We introduce Kerberos protocol briefly and take a refinement approach to express messages which contain cryptographic transformations. After that, we analyze the Kerberos protocol completely and correctly with the improved reconciling method.In the end, we summarize the main content and innovation of the thesis, point out the questions and directions which need us to pay more energy to study in this field.