基于认证测试方法的EAP-AKA协议分析

EAP-AKA(Extensible Authentication Protocol-Authentication and Key Agreement)是WLAN的认证和密钥分配协议;认证测试是一种以串空间理论为基础的安全协议分析验证方法。运用认证测试方法对EAP-AKA协议的双向身份认证过程进行了分析证明,结果说明EAP-AKA能够保证移动终端和认证服务器之间的双向认证。     

Needham-Schroeder 协议的认证测试方法形式化分析

在安全协议的形式化分析方法中,串空间模型和基于串空间模型的认证测试方法是比较常用的验证方法。针对Needham- Schroeder协议存在中间人攻击的缺陷,提出对协议的改进并采用认证测试方法,验证了改进的协议可以满足协议的安全目标。     

增强EAP-AKA协议安全性的改进方案

针对EAP-AKA协议中存在的安全问题,提出了改进方案。通过在3G和WLAN接入网络间增设共享密钥实现了两者间的相互认证,并用串空间模型和认证测试方法进行了形式化分析,通过加密传输NAI实现了对IMSI的加密保护,通过引入密钥更新机制实现了对用户和3G网络间的共享密钥的安全更新。     

EAP-AKA协议的改进与分析

EAP-AKA协议是3G-WLAN互联的认证与密钥协商协议,通过对EAP-AKA协议的安全性分析,提出了一种改进方案,并对其安全性进行了分析。     

WiMAX中EAP-AKA认证协议与安全性能分析

WiMAX以其极高的接入速率成为当前无线宽带接入技术研究的热点,EAP-AKA是其对应的鉴权和密钥管理协议,本文分析了EAP-AKA协议的认证流程和安全性能,指出了其安全缺陷.     

安全协议认证的形式化方法研究

安全协议认证是网络安全领域中重大课题之一。形式化方法多种多样。该文首先论述了模型检测技术及其在安全协议验证中的应用,然后介绍了各种定理证明方法和定理证明工具,接着讨论其它形式化验证方法,最后论述形式化方法的一些研究方向。     

改进身份认证协议的形式化描述与验证

以前用着色Petri网验证协议,大多只验证了其正确性,采用着色Petri网对自行设计的基于PKI的动态身份认证系统的安全性进行了描述和验证;一般在使用传统1-可达性分析方法分析复杂身份认证协议时,会存在状态空间爆炸的问题,为了有效地解决该问题,提出了一种用1-可迭性分析方法和向回分析方法相结合的策略,对该身份认证协议进行了分析,从而验证了该身份认证协议是安全的.     

一种用户身份认证系统的形式化描述

身份认证系统用于解决访问者的物理身份和数字身份的一致性问题,给其他系统提供权限管理的依据.运用形式化方法,针对一个用户身份认证系统,使用Z语言对其进行形式化描述.在形式化过程中,对该系统用户身份记录定义了读、添加、更新、删除四种操作,对该系统用户身份认证定义了登录、退出二种操作.对于每种操作,还定义了具体的操作步骤、操作需要的前提条件和提示信息.身份认证是整个信息安全体系的基础,并越来越受到重视,因此研究身份认证系统的形式化具有一定的现实意义.     

公钥密码体制下认证协议的形式化分析方法研究

本文通过对形式化方法中最广泛使用的类BAN逻辑进行研究发现，此方法更侧重于对称密码体制下认证协议的分析，而在分析基于公钥体制的认证协议时，该方法有很大的局限性。因此，文中针对公角密码的特点对类BAN逻辑进行了扩展。扩展后的逻辑方法能够更好地应用于分析公钥认证协议。     

基于身份密码学的EAP-AKA方案

针对3GPP R8版本中的EPS-WLAN互联网络,分析EPS-WLAN互联网络接入认证协议EAP-AKA的安全性,指出其存在的安全隐患以及对于特定攻击存在的脆弱性。在EAP协议的基础上,引入基于身份的加密和密钥协商的要素,提出基于身份密码学的改进方案。通过性能和安全性分析,证明该协议能够在不增加协议步骤和系统负担的条件下,克服EAP-AKA协议的安全隐患,提高协议的安全性。     

802.11i双向认证协议的模型检查

确保安全协议的正确性对于保证Internet上安全敏感的业务非常重要。采用形式化方法建模和验证安全协议可以检测到传统测试手段难以发现的错误。模型检查作为形式化验证方法的一种,有着自动化和提供反例等诸多优点。使用模型检查工具SPIN对802.11i双向认证协议EAP-TLS进行验证,提取出包含协议设计重要细节的形式化模型,对协议安全属性采用线性时态逻辑抽象,并验证协议模型是否满足安全属性。提出了一种使用PROMELA建模认证协议的方法。     

无人机无线通信协议的形式化认证分析与验证

针对无人机组与地面控制站之间进行无线通信时的身份认证问题,首先分析无线通信协议的工作流程及其形式化表示,然后对网络系统中的诚实主体和攻击者进行形式化建模,其中推导了协议安全属性的LTL公式,通过建立密钥机制,实现控制站与无人机节点以及各个无人机节点之间的身份认证;运用模型检测工具SPIN验证无线通信协议的一致性,其中提出一种改进的知识项获取方法,加快攻击者需掌握知识集的求取过程;验证结果表明该无人机无线通信协议具有中间人攻击漏洞。     

基于 EAP-AKA 协议的安全性分析和改进

近几年来,以3G 网络和 WLAN 为主要代表的无线网络技术取得了重大突破,3G网络能够在广域的范围内提供比较好的漫游服务,但其传输的数据速率以及网络带宽较小,而WLAN 能够提供较高的数据传输速率而且价格较低,但其网络范围较小,因此,3G 网络和WLAN 两者融合具有很好的互补性,这是实现高速接入的一种比较高效的模式。因此3GPP 组织针对3G 网络与 WLAN 融合提出了一套互联方案,并为其设计了可扩展认证和密钥协商协议（EAP-AKA）。但是经过大量的的实践和研究发现,EAP-AKA 协议存在一些安全缺陷,文章通过对 EAP-AKA 的协议过程和安全性进行分析,针对其安全缺陷,特别是用户身份会暴露而导致由于身份泄露引起的跟踪攻击,缺乏对无线局域网（WLAN）接入网络的认证以及明文传输会话密钥而导致 WLAN 失去通信过程中的机密性和完整性等,提出了一种通过对 WLAN 接入网络增设公钥以及采用匿名技术的改进方案,分别完成了对无线局域网接入网络的认证,避免了用户身份信息的暴露以及加密传输会话密钥,保证了为用户提供安全的网络服务。     

EAP-AKA协议的分析和改进*

3G与WLAN互连是当前研究的一个热点。EAPAKA是其对应的认证与密钥分配协议。详细分析EAP-AKA协议的流程和安全性,并针对其中的安全缺陷,提出一种改进的方案,同时对改进方案的安全性也进行了分析。     

安全协议中的形式化验证技术

伴随着网络和通信的迅速发展，安全已经成为一个备受关注的问题，为确保不同系统的安全，出现了许多的安全协议。文中描述了安全协议验证的形式化需求，并且详细阐述了目前流行的几种形式化的验证技术及各自的优缺点，探讨了形式化验证技术所面临的挑战，指出目前在这方面所做的工作以及有待发展的方向。