论文部分内容阅读
随着信息网络的快速发展,云服务走进人们的视野,与此同时,因云环境的开放性等特点给云计算的安全带来极大挑战。大多数用户不选择云计算系统,其根本原因就是担心云计算不能保证个人隐私安全和数据安全。云安全协议是保障云环境下通信安全的重要手段,面对云计算所面临的安全性挑战,云安全协议的设计需更加复杂。Nayak协议是一种云环境下基于口令身份认证方案,实现双向认证和会话密钥交换的协议,该协议不依赖数字证书,通过共享简单易于记忆的口令来进行认证与密钥交换,以其简单、高效且易于部署的特点得到了广泛应用。但因方案一般选择易于记忆的口令,导致基于口令的身份认证机制容易受到字典攻击、中间人攻击、内部人员辅助攻击等威胁,这意味着Nayak协议面临着严峻的安全考验。本文以Nayak协议为研究对象,采用形式化方法分析Nayak协议,针对Nayak协议存在的中间人攻击,对协议进行改进。本文的主要工作如下:(1)运用模型检测技术对Nayak协议进行分析与验证。采用对称密钥密码体系对Nayak协议进行加密,基于Dolev-Yao攻击者模型,提出四通道并行建模法描述攻击者能力。运用SPIN模型验证工具,分析结果表明采用对称密钥密码体系对Nayak协议加密不安全。(2)分析Nayak协议所存在的缺陷与安全隐患,提出基于时间戳私钥签名技术的Nayak-T协议。Nayak-T协议在消息项内增加时间戳并更改加密手段,通过双重加密的手段来保证双方通信安全,利用四通道并行建模法对Nayak-T协议建模,运用SPIN对该协议进行验证,验证结果得出Nayak-T协议安全。(3)运用类型检查、语法重定序、静态分析三种优化策略对Nayak-T协议进行模型优化,以达到状态空间消减、存储空间压缩,得到最优安全协议模型。(4)本文提出的四通道并行建模法,可解决重复子消息项以及多轮协议并行的问题,减少进程间交叉运行产生的状态迁移量,降低构建模型复杂度。该建模法具有通用性,可适用于类似复杂协议形式化分析与验证。