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

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