Research On Security Protocol Analysis Technique Based On Extended CSP Model

As a method of formal verification of security protocols, the method based on process algebra has been active recently. The CSP method has proved to be very successful for finding attacks. However, their use in proving protocols had generally been limited, usually restricted by the finiteness of some set of resources. In order to solve the limit, this paper studies the process algbra and CSP model at first, and then extends the CSP model based on data independence. For proving the correctness and validity of the extended CSP model, a verification of protocol and a theory proof are proposed. The main works are listed as follow: By studying the development and application of process algebra, two great breakthroughs in the development are proposed. In order to form the system info of process algebra, the history of development is summarized according to the breakthroughs. By analyzing the CSP model of security protocol, the integrated formalized description and the refine checking goal of security characters are presented. From the point of view of refine checking, the CSP model of security protocol is built that laying a strong emphasis on checking the flaws of security protocol. Based on the research, some shortages of CSP model are summed up. By studying the data independence techniques of Roscoe, some principles for modeling that using the data independence techniques are summed up. Based on the data independence techniques, an extended CSP model and its correctness verification are proposed that laying a strong emphasis on the designing and description of nonce cycling mechanism which composed of Manager process and intruder process. By studying the working principle and refine checking algorithmic of FDR, the working step of checking are presented. The extended CSP model is implemented in CSP_m and the attacks of extended protocol are found by refine checking.