期刊文献+
任意字段
题名或关键词
题名
关键词
文摘
作者
第一作者
机构
刊名
分类号
参考文献
作者简介
基金资助
栏目信息
共找到3篇文章
< 1 >
每页显示 20 50 100
已选择0条
导出题录 引用分析
参考文献
引证文献
 统计分析
检索结果
已选文献
显示方式：
5G网络鉴权协议的形式化分析与改进
1
作者 伍祥 缪祥华 +1 位作者 张婉君 陈琼 《化工自动化及仪表》 2026年第2期272-278,共7页
由于5G移动通信网络的高速发展,其需要的安全性也在逐步增加,第三代合作伙伴计划(3GPP)已经标准化了用于移动通信的5G AKA(认证和密钥协商)等协议,但是5G AKA协议的安全性没有任何保证。因此,首先针对5G AKA协议、传输信道和攻击者进行... 由于5G移动通信网络的高速发展,其需要的安全性也在逐步增加,第三代合作伙伴计划(3GPP)已经标准化了用于移动通信的5G AKA(认证和密钥协商)等协议,但是5G AKA协议的安全性没有任何保证。因此,首先针对5G AKA协议、传输信道和攻击者进行建模,使用Tamarin工具形式化分析协议中的参数SUPI、SNname和安全锚点密钥KSEAF的Lowe分类法的鉴权性质。根据分析结果,发现从UE实体角度考虑的大部分鉴权性质都不能满足,针对协议存在的安全缺陷和不满足的鉴权性质,提出了两种方法对模型进行改进,一种是引入物理层相关参数计算生成安全密钥,修改原本的MAC认证码生成,将SNname参数增加到MAC的计算中;第2种是在协议结束阶段增加UE和SN实体之间的消息确认,对改进后的协议进行验证和分析,并增加对SUPI和KSEAF单射一致性的验证。改进后的协议大部分鉴权性质都满足。 展开更多
关键词 5G AKA协议 形式化分析 Lowe分类法 鉴权性质 Tamarin工具
在线阅读 下载PDF
基于观察等价性的协议猜测攻击形式化检测方法
2
作者 苗旭阳 顾纯祥 陆思奇 《密码学报》 CSCD 2023年第2期306-319,共14页
由于口令的低熵性,针对基于口令的安全协议存在特有的口令猜测攻击,当前的形式化语义不能较好地刻画攻击者执行口令猜测攻击的条件,对于协议抗猜测攻击能力没有统一的形式化安全属性定义.本文提出了基于观察等价性的协议猜测攻击形式化... 由于口令的低熵性,针对基于口令的安全协议存在特有的口令猜测攻击,当前的形式化语义不能较好地刻画攻击者执行口令猜测攻击的条件,对于协议抗猜测攻击能力没有统一的形式化安全属性定义.本文提出了基于观察等价性的协议猜测攻击形式化检测方法.使用多集重写规则对协议交互流程进行形式化建模,给出了口令初始化、口令猜测行为的标准化规则,修改完善基于口令的对称加密原语,以支持包含基于口令的对称加密的协议验证.理论上将协议口令猜测攻击的形式化分析检测转换为正确猜测和错误猜测下多集重写规则双系统的观察等价性是否成立的判断问题;实现上使用Tamarin形式化分析工具对协议是否存在口令猜测攻击进行自动化分析,首次实现了形式化分析工具对口令猜测攻击路径的自动化生成.使用该方法对EKE、SPAKE等传统口令认证协议和多因子认证协议进行形式化建模和分析,对其中存在口令猜测攻击的协议自动化生成可行的口令猜测攻击路径,验证了方法的正确性和有效性. 展开更多
关键词 形式化分析 观察等价性 口令猜测攻击 tamarin-prover
在线阅读 下载PDF
基于Tamarin Prover的5G EAP-TLS协议的形式化分析 被引量：2
3
作者 马壮壮 杜瑞颖 +1 位作者 陈晶 何琨 《武汉大学学报（理学版）》 CAS CSCD 北大核心 2023年第5期653-664,共12页
为了保证5G专用网络中移动设备的通信安全,第三代合作伙伴计划(3rd generation partnership project,3GPP)提出了5G可扩展认证协议-传输层安全(extensible authentication protocol-transport layer security,EAP-TLS)。然而,现有的针对... 为了保证5G专用网络中移动设备的通信安全,第三代合作伙伴计划(3rd generation partnership project,3GPP)提出了5G可扩展认证协议-传输层安全(extensible authentication protocol-transport layer security,EAP-TLS)。然而,现有的针对于5G EAP-TLS协议的研究工作较少且缺乏系统性。因此,对5G EAP-TLS协议进行详细的描述,并对该协议进行全面的形式化建模。对5G规范中涉及的所有协议实体以及证书分发机制进行建模,同时从5G规约中提取并建模了与5G EAPTLS协议相关的安全目标。提出证据搜索策略引导符号分析工具Tamarin Prover进行自动化证据搜索,解决了Tamarin Prover在验证复杂模型时验证过程无法终止的问题,实现了5G EAP-TLS安全目标的自动化验证。通过分析验证结果,发现了5G EAP-TLS协议能够满足机密性目标,但难以满足一些认证性目标,同时,揭示了协议存在拒绝服务(denial of service,DoS)攻击和用户通信数据泄露的隐患。针对发现的问题,提出了相应的补丁方案,并通过提出的证据搜索策略引导分析工具Tamarin Prover自动化验证了该补丁方案的有效性。 展开更多
关键词 5G专用网络 EAP-TLS协议 形式化分析 Tamarin Prover 自动化验证
原文传递
已选择0条
导出题录 引用分析
参考文献
引证文献
 统计分析
检索结果
已选文献
上一页 1 下一页 到第 页
使用帮助 返回顶部