Formal Analysis and Enhancement on 3GPP AKA protocol with KG Logic

3GPPAKA协议的设计者使用BAN逻辑对协议进行形式化的分析,并生成所有的安全目标已经达到。但是由于BAN逻辑的局限性,设计者并没有找到协议对于重定向攻击和重放攻击的脆弱性。本文给出基于信仰变化的KG逻辑方法,指出脆弱性所在,并对改进后的协议方案进行验证。

基于PCL的3GPP-AKA协议的形式化分析与证明

3GPP-AKA协议在第三代移动通信的安全性方面起着至关重要的作用,它保证了移动用户MS与VLR/HLR之间的双向认证及密钥协商。文中通过协议组合逻辑(PCL)对3GPP-AKA协议进行了形式化分析及安全性证明。分析表明3GPP-AKA协议可以满足它的安全目标,因此该协议可以安全的作为第三代移动通信中的认证和密钥分配协议。

一种改进的高效鲁棒的3GPP AKA协议

针对3G鉴权与密钥协商协议(3GPP AKA)中存在的安全缺陷,结合攻击者可能发起的攻击提出了一种可以防止重定向攻击,利用存在安全漏洞的网络发起的主动攻击,SQN同步缺陷和用户身份信息泄露的改进协议(ER AKA,Efficient and Robust Authentication and Key Agreement),并对其安全性和效率进行了分析,分析表明通过该协议可以以较少的存储资源和计算资源为代价有效的解决上述安全性问题并减少3G系统中安全性处理的信令交互次数。