论文部分内容阅读
计算机网络正以惊人的速度发展,但是网络安全问题却变得越来越突出,越来越复杂,解决安全问题对许多网络应用来说是首要难题。目前,安全协议是解决网络安全问题最有效的手段之一,需要通过安全协议进行实体之间的认证、在实体之间安全地分配密钥或其他各种秘密、确认发送和接收的消息的非否认性等等。身份认证密钥协商协议是让通信双方确认彼此的身份并共同协商安全的会话密钥,因此,认证密钥协商协议的安全性直接影响到整个通信的安全,这要求认证协议具有抵抗各种攻击的能力。设计和分析认证密钥协商协议是一件具有挑战性的工作,事实表明,许多安全协议经过安全专家认真分析、设计和实现后仍存在漏洞,有些甚至在使用多年后才被发现其存在的漏洞。基于公钥密码体制的认证密钥协商协议已成为当前认证密钥协商协议设计的主流,它在密钥管理和可扩展性方面具有不可替代的优势。以移动通信领域为例,移动通信的安全要求愈来愈高,其安全问题不容忽视。而移动设备计算能力则相对较低,如何降低移动端的计算量是在移动通信中应用认证密钥协商协议时急需解决的问题。当前,一些协议采用哈希函数的方法代替签名机制进行身份认证,通过精巧的设计大大降低了移动设备的计算量。随着认证密钥协商协议的不断发展,安全协议形式化分析方法必须适应安全协议的新变化。本文选取在安全协议形式化分析领域有影响的两种形式化分析方法:SVO逻辑方法和strand space方法作为研究对象,研究内容包括:①对SVO逻辑方法及其分析目标进行扩展和改进;②对strand space理论及其验证模型进行扩展;③研究一个典型的可相互认证协议MA,证明针对MA的Hijacking攻击不成立,并提出针对该协议的未知共享密钥攻击;④提出新的可用于移动通信的相互认证和密钥协商协议MAKAP-3,与国内同类型协议进行比较,指出新协议在计算复杂度和实用性方面所具有的优势,并采用改进的SVO逻辑方法和扩展的strand space方法证明新协议是安全的。