New Logic for Analyzing and Designing Authentication Protocol

This paper presents a new logic for analyzing and designing authentication protocol. The logic can be used to analyze authentication protocol and design authentication protocol. Authentication protocol analysis and design are proceeded by the logic. The logic gets rid of non-consistence in different ways to analyze and design authentication protocol. During analyzing authentication protocol,authentication protocol is formalized and is reasoned by the logic. There exist bugs or leaks in authentication protocol if the logic can not reason the goal of authentication protocol. During designing authentication protocol,the protocol designer can use a systematic way to construct requiring protocol by synthetic rules. The paper analyzes Needham-Schroeder protocol and presents that the protocol can not reach protocol goal,and the protocol is redesigned.