A New Logic For Analyzing And Designing Security Protocol

Security protocol is a kind of application layer protocol, it packs communication entity, puts on the suit of armour, prevents the attacker from stealing the sensitive data, guarantees the integrality of the communication content. Different application demands have put forward the new request for the design of security protocol, such as group communication, anonymous communication, secure multi-party computation, non-repudiation signature, blind signature, group blind signature, digital cashes and etc., these security technologies must depend on secutity protocol, so the security problem of security protocol is very important.With the development of information technology, the information security becomes the topic that people generally care about. People have already got used to working, communicating, carrying on trade of different goods on the network, so the network security is a current research focus. How to achieve secret communication in the unsafe environment? This problem is solved through security protocol mainly, so security protocol is a key to the network security success or failure.This paper presents current research situation of security protocol analysis and design, and puts forward a new logic of analyzing and designing security protocol, and applies strand space model to prove correctness of the new logic. Finally, the paper illustrates the application of the new logic with several instances. Loosely speaking, the paper has made some achievements below. (1) The paper presents the components of the new logic, including logic symbols, reasoning rules and synthetic rules. Among them the reasoning rules are used for analyzing security protocol, and the synthetic rules are used for designing security protocol.(2)The paper presents a semantics for the new logic. The strand space model is a very important tool of analyzing security protocol, and it has good semantics, but it is difficult to analyze security protocol. The new logic is easy to analyze security protocol, but a semantics for the new logic is not very clear. A strand space semantics for the new logic is presented by combining the new logic withstrand space model, thus proved that the new logic is correct. (3)The new logic can be applied to analyze security protocol. According to sequence of protocol statement, by combining initial conditions with the reasoning rules, the new logic can analyze whether the protocol can reach the goal or not. If the protocol can't reach the goal, the protocol has flaws or leaks. (4)The new logic can be applied to design security protocol. According to the synthetic rules, the goal of protocol can be divided into a lot of sub-goal, then the new logic can check whether each sub-goal is satisfied or not. Repeating this procedure, the design procedure is terminated when all sub-goals are satisfied. Finally, according to synthesize the whole design procedure, the protocol can be described.(5) The new logic brings the procedure of security protocol analysis and design into a frame, so it can get rid of the inconsistency with different methods to analyze and design security protocol.(6) The new logic has simplified the procedure of formalizing the initial conditions and security protocol goal respectively. If security protocol is analyzed and designed with different methods, initial conditions and goal of security protocol must be formalized twice. In the new logic, the initial conditions and goal of security protocol only need be formalized once, thus the new logic can improve work efficiency.Security protocol is the key to information security and network security.In a certain sense, if the security problem of security protocol has been solved, then the problems of the information security and network security are easy to solve. This paper is devoted to solving the security problem of security protocol, it has made some achievements, but there exist some problems, for example, the new logic has not completeness. In a situation that a security protocol has a lot of protocol statement, if the procedure of analyzing and designing security protocol is operated with computer, it is easy to produce combinatorial explosion.