5G网络认证与密钥协商协议的形式化验证与分析

网络攻击的手段层出不穷,如中间人攻击,重放攻击,DoS攻击等,以此获取不当利益.密钥协商协议的设立是为合法用户提供正确认证入口,并拒绝攻击者的非法接入和攻击.密钥协商协议是保护移动通信提高服务质量的第一道安全防线,5G网络密钥协商协议在实际环境中仍然存在安全隐患,其协议本身的安全特性能否满足要求仍未可知,本文提出使用基于概率模型检测的方法,通过对5G网络密钥协商协议的各协议方实体进行建模,建立离散时间马尔科夫链模型,在建模过程中考虑外界的攻击影响,引入攻击率来描述外界的影响程度,通过攻击率对5G网络密钥协商协议的研究进行定量分析,使用概率计算树逻辑对待验属性规约进行编码描述,利用概率模型检测工具PRISM进行实验.实验结果表明:在引入攻击率的5G网络密钥协商协议模型中,5G网络密钥协商协议各协议方实体所受攻击的影响对该协议的时延性,有效性,保密性等属性规约的性能有不同程度的影响,因此,研究外界网络攻击对协议的安全性能的影响,对加强协议安全性能及其改进具有一定借鉴意义,并对5G网络密钥协商协议的安全特性的提升和保护用户的经济与信息安全具有很大的意义.