运用SPIN对云环境双向认证协议Nayak的安全性验证

随着云计算的发展,由欺诈行为驱动的窃取云资源和云服务的行为日趋严重,导致云资源提供商与用户间出现信任危机。Nayak协议是一种改进的云环境双向认证协议,用于保障用户安全登录云服务器,防止第三方恶意窃取用户信息。采用对称密钥密码体系对Nayak协议进行加密,基于Dolev-Yao攻击者模型,提出四通道并行建模法描述攻击者能力。该建模方法解决了Nayak协议并行运行过程中的模型检测问题以及安全隐患,优化了模型复杂度与存储状态数。运用SPIN模型验证工具分析表明采用对称密钥密码体系对Nayak协议加密不安全。此方法可运用于类似复杂协议形式化分析与验证。

基于时间戳私钥签名技术的Nayak-T协议安全性分析

随着信息网络的快速发展,云服务走进人们视野,云环境下信息安全问题成为人们关注的焦点。Nayak协议是一种云环境下基于口令身份认证,实现双向认证和会话密钥交换的协议。针对Nayak协议存在的中间人攻击,提出改进协议Nayak-T。Nayak-T协议在消息项内增加时间戳并更改加密手段,通过双重加密的手段来保证双方通信安全。利用四通道并行建模法对Nayak-T协议建模,运用SPIN对该协议进行验证,验证结果得出Nayak-T协议安全的结论。模型优化策略分析表明,采用静态分析、类型检查、语法重定序模型优化策略的模型检测效率最佳,可运用于类似复杂协议的形式化分析与验证。