分析和设计安全协议的新逻辑

现有的逻辑,有的只可用于分析安全协议,而有的则只可用于设计安全协议.本文提出一种分析和设计安全协议的新逻辑.该逻辑不但可以用来分析安全协议,而且可以用来设计安全协议.通过运用该逻辑,使安全协议的设计和分析可以在同一种逻辑中进行.同时,该逻辑消除了用不同的方法来设计和分析安全协议的不一致性.在分析协议时,首先用逻辑对协议进行形式化,然后用推理规则对协议进行推理.如果不能推理出协议的最终目标,说明协议存在缺陷或者漏洞.在设计协议时,通过运用合成规则使协议设计者可用一种系统化的方法来构造满足需要的协议.最后,用该逻辑分析Woo-Lam协议,指出该协议不能满足协议目标.我们用该逻辑重新设计了该协议,说明重新设计的协议能够达到协议的目标.

A New Logic for Analysis and Design of the Security Protocol

There exist many logics. Some of them may be only used to analyze security protocols,and the others may be only used to design security protocols. This paper presents a new logic for analysis and design of security protocols. The logic can be used not only to analyze security protocols,but also to design security protocols. Security protocol analysis and design may proceed in the same logic. At the same tlme,the logic may get rid of non-consistence in different ways of analysis and design. During analyzing a security protocol, the security protocol is formalized by the logic and then it is deduced by the reasoning rule. The security protocol is found to have bugs or leaks if the logic can not reason out the protocol goal. During designing a security protocol, the protocol designer may use a systematic way to construct the required protocol. The paper, uses the logic to analyze Woo-Lam protocol and indicates the impossibility to reach the protocol goal. The paper redesigns the Woo-Lam protocol and makes it success.