一种分析和设计认证协议的新逻辑

New Logic for Analyzing and Designing Authentication Protocol

提出一种分析和设计认证协议的新逻辑,可以用来分析认证协议和设计认证协议。通过运用该逻辑,使认证协议的设计和分析可以在同一种逻辑中进行,也消除了用不同的方法来设计和分析认证协议的不一致性。在分析协议时,先用逻辑对协议进行形式化,再用推理规则对协议进行推理。如果不能推理出协议的最终目标,说明协议存在缺陷或者漏洞。在设计协议时,通过运用合成规则使协议设计者可用一种系统化的方法来构造满足需要的协议。用该逻辑对Needham-Schroeder私钥协议进行了分析,指出该协议不能满足协议目标,并重新设计了该协议。

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 protocok authentication protocol is formalized and is reasoned by the logic, There exist bugs or leaks in authen6cation protocol if the logic can not reason the goal of authentication protocol. During designing authemication 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.