安全协议是目前保证信息交互在安全条件下进行的基础。然而,安全协议从设计到部署的过程并不容易,因为安全协议通常会存在缺陷。故需要一套方案来检测安全协议的安全性。目前针对安全协议的安全问题验证,主要有逻辑分析方法、定理证明方法以及形式化验证等方法,其中形式化验证是目前普遍认可的方案。针对5G附着请求流程以及其他几个安全协议,本文使用形式化方法验证其安全性。其中在5G附着请求中失败附着流程可能会产生关联性攻击问题,而在形式化工具ProVerif中无法自动化验证,针对该问题,本文在ProVerif工具的基础上扩展。针对协议中的关联性攻击验证,扩展工具对输入的形式化描述的协议自动构建关联攻击相关属性。与ProVerif工具验证对比,扩展工具实现了自动化构建关联性攻击的相关安全属性,输入文件中无需构建相关属性。实验结果表明,本文的5G附着协议中失败的附着请求安全策略可以抵抗关联性攻击,扩展的工具也能够自动化验证安全协议的关联性攻击问题。本文通过形式化工具ProVerif验证表明本文5G附着请求安全策略是有效的,达到了抗关联性攻击的目的。其中针对安全协议中关联攻击验证问题,对ProVerif工具扩展,扩展后的工具可自动化验证关联性攻击,实验结果也表明该工具能达到此目的。