一种面向5G专网鉴权协议的形式化分析方案

摘要：

文章提出一种面向5G专网鉴权协议EAP-TLS的细粒度形式化建模与验证方案.方案以TS 33.501文档为依据,首先构建基于Diffie-Hellman模式的协议交互模型;然后扩展Dolev-Yao攻击者模型,提出了两种参与方受控场景和混合信道模型;最后使用验证工具SmartVerif验证保密性、认证性、隐私性3类安全属性.实验结果表明,协议在保密性和认证性方面存在3类安全隐患.文章分析了出现安全隐患的根本原因并提出了修订方案,修订后的协议可以满足文章定义的全部安全属性.

关键词：5G专网;EAP-TLS认证协议;Dolev-Yao攻击者模型;形式化方法

分类号：TP309(计算技术、计算机技术)

资助基金：国家自然科学基金[61972369;国家重点研发计划[2018YFB2100301

在线出版日期：2021-09-28（万方平台首次上网日期，不代表论文的发表时间）

页数：共7页

页码：1-7