近年来,网络安全问题日趋严重,针对计算机网络的安全和隐私研究已刻不容缓。为了解决网络协议安全性不足的问题,研究人员设计了各种网络安全协议(以下简称安全协议),以增强网络的安全。但是,很多投入实际应用的安全协议在运行时并不能提供其声明的安全服务。因此,针对安全协议的安全性检测成为安全测试中的重要环节。研究人员在设计或优化安全协议后,需要进一步证明该协议的安全。与非形式化的安全协议验证技术相比,形式化方法能够更全面、深入的检测安全协议和软件中未知的漏洞,它不仅能够证明安全协议的安全性,而且有助于发现针对安全协议的新型攻击手段。但是由于安全协议的复杂性,现有的形式化验证技术并不能自动化证明所有的安全协议,在证明过程中需要专业验证人员辅助计算机完成证明。过高的人力成本和学习成本阻碍了形式化验证技术的进一步发展和运用。本文围绕安全协议的形式化自动验证相关问题,开展了深入的研究。主要研究成果总结如下:1.提出了一种基于强化学习的安全协议形式化自动验证技术,设计并实现了原型系统。本方法突破并解决了传统形式化自动验证中的状态空间爆炸问题。相比于传统的形式化验证工具,该系统可以全自动地搜索正确证明路径,无需任何手工辅助。研究成果可以挖掘给定目标的安全协议的所有安全漏洞,确保网络安全协议不会被攻击者攻破。据笔者所知,该系统是首个使用动态策略全自动形式化验证安全协议的工作。实验结果表明,该系统实现了安全协议的通用和全自动形式化验证,远优于现有的形式化验证工具。2.提出了一种面向可追责协议的形式化研究方法,设计并实现了原型系统。针对可追责协议的安全属性本文提出了形式化定义。基于该定义,提出并实现了针对可追责协议的形式化建模与验证方法。该方法扩展了应用pi演算语言,通过使用新定义的语法,用户只需要对正常参与方的操作流程进行手动建模,工具可根据用户建立的模型将相应的异常参与方操作自动转换为协议验证工具ProVerif可验证的模型语言。另外,本文提出了一套自动转换协议模型并生成安全目标的方法。该方法极大降低了形式化建模和验证协议的复杂性。实验结果表明,该方法可适用于两个典型的可追责协议的形式化研究,通过本方法,成功发现了不可否认协议的设计缺陷。3.提出了一种面向5G-AKA协议的形式化研究方法。该方法采用多重集合复写规则对5G-AKA协议进行建模。协议模型基于协议规范中的四方消息交互模型。攻击者能力比现有工作定义的攻击者能力要更全面。安全属性包含私密性、认证的相关属性以及隐私性。然后,使用通用全自动形式化验证系统验证形式化模型。实验结果表明,5G-AKA协议模型中的所有安全属性都成立。另外,使用前文定义的可追责属性针对5G-AKA协议进行了形式化分析,发现协议并未设计追责的流程,存在设计缺陷。针对此缺陷,对5G-AKA协议提出了改进措施,并使用通用全自动形式化验证系统对改进后的协议进行了验证,验证结果表明,修改后的协议保证了追责的公平性和完整性。