Abstract: Formal method is an important approach for analyzing network security protocols. Network protocol secu-rity is a research hotspot in information security field. Event logic is a formalism for describing transition between states in a distributed system. It’s common to use event logic to certify the security of network security protocols. Based on event logic, this paper defines strong match and match sessions, and proposes the strong authentication theory by combining event logic axioms and inference rules. Using the strong authentication theory, this paper proves that three-principal Neuman-Stubblebine protocol is not secure because the sender is secure and the receiver isn’t secure. The research results show that the strong authentication theory is applicable to the security certification of similar multi-party security protocols.

Key words: formal method, event logic, strong authentication theory, Neuman-Stubblebine protocol

摘要： 形式化方法是分析网络安全协议的一种重要方法，网络协议安全性也是信息安全领域的研究热点。事件逻辑是一种描述分布式系统中状态迁移的形式化方法，用于证明网络安全协议的安全性。以事件逻辑为基础，定义强匹配及匹配会话，结合事件逻辑公理和推理规则，提出了强认证理论。利用该理论对有3个主体的Neuman-Stubblebine协议进行了研究，分析得出发送者是安全的而接收者是不安全的，从而证明了该协议是不安全的，说明了强认证理论适用于三方的网络安全协议。该理论适用于类似多方网络安全协议的安全性证明。

关键词: 形式化方法, 事件逻辑, 强认证理论, Neuman-Stubblebine协议