SAP-AKA二次认证协议的形式化验证与改进

来源：计算机工程杂志2025年第6期北京时间：

作者：彭程炜, 杨晋吉, 杨光

单位：华南师范大学计算机学院，广东 广州 510631

摘要：SAP-AKA协议是根据第3代合作项目(3GPP)标准定义的基于可扩展身份认证(EAP)框架, 为垂直用户提供密钥服务安全的二次认证协议，在5G实际环境中，认证与密钥协商协议受到各种网络攻击的影响，导致非法访问、无法认证以及身份信息泄露，在面临巨大安全挑战下SAP-AKA协议的安全属性能否满足要求仍未知。为此, 采用概率模型检测方法对SAP-AKA协议建立形式化模型，在协议交互状态迁移中引入攻击率，定量分析攻击率对协议的影响程度，使用概率计算树逻辑描述协议属性，并利用概率模型检测工具PRISM对协议的安全属性进行定量形式化分析。实验结果表明，SAP-AKA协议的时延性、认证性和完整性在不同程度上受各实体间攻击率的影响，随着攻击率变大，协议的安全属性不再满足要求。最后根据实验结果分析造成安全缺陷的原因，提出了改进方案并进行形式化验证，协议的安全属性均得到有效提升。

关键词：概率模型检测,认证协议,SAP-AKA协议,形式化验证,PRISM工具

基金资助：广东省自然科学基金(2020A1515010445)