形式化方法是分析网络安全协议的一种重要方法,也是信息安全领域的研究热点。形式化方法基于严格的数学概念和逻辑方法,对协议进行描述,在描述过程中可发现协议安全属性的不明确或不完整,有效地降低分析过程复杂度,使协议的安全分析简单、规范、实用。定理证明是形式化方法的一种,目的是证明无穷并发状态下网络安全协议是安全的。事件逻辑是在并发与分布式系统下描述协议和算法的逻辑,是定理证明中一种非常重要的逻辑方法。本文以事件逻辑为基础,对其进行扩展,提出强认证理论。针对Needham-Schroeder(NS)协议和Neuman-Stubblebine协议进行形式化描述及认证性证明。论文主要工作包括:1、基于事件逻辑,对安全协议的七种动作(生成挑战数、发送消息、接收消息、加密、解密、签名和验证)进行形式化描述,同时给出协议中密钥、挑战数和协议消息的形式化描述。定义强匹配及匹配会话,结合事件逻辑公理和推理规则,提出强认证理论。2、对两个主体的NS协议进行研究,针对协议漏洞,对其增加时间戳,避免了重放攻击,运用事件逻辑对改进后的协议进行形式化描述,通过对发送者和接收者的认证证明,说明强认证理论适用于两方的网络安全协议;对三个主体的Neuman-Stubblebine协议进行研究,运用事件逻辑对协议基本序列进行合法定义,证明发送者是安全的而接收者是不安全的,不能达到双向身份认证,说明强认证理论也适用于三方的网络安全协议。3、通过以上分析,认证协议可以通过只对协议诚实主体动作的推理来证明其认证性,事件逻辑适用于多个主体的网络安全协议认证性分析。