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

摘要

随着云计算的发展,由欺诈行为驱动的窃取云资源和云服务的行为日趋严重,导致云资源提供商与用户间出现信任危机.Nayak协议是一种改进的云环境双向认证协议,用于保障用户安全登录云服务器,防止第三方恶意窃取用户信息.采用对称密钥密码体系对Nayak协议进行加密,基于Dolev-Yao攻击者模型,提出四通道并行建模法描述攻击者能力.该建模方法解决了Nayak协议并行运行过程中的模型检测问题以及安全隐患,优化了模型复杂度与存储状态数.运用SPIN模型验证工具分析表明采用对称密钥密码体系对Nayak协议加密不安全.此方法可运用于类似复杂协议形式化分析与验证.%With the development of cloud computing,the behavior of cloud resources and cloud services driven by fraud is becoming more and more serious,leading to cloud trust crisis between resource providers and users.Nayak protocol is an improved mutual authentication protocol in cloud environment,it used to protect the user's security login cloud server and prevent the third-party malicious theft of user information.We use the symmetric key cryptosystem to encrypt the Nayak protocol On the basis of Dolev-Yao attacker model,we propose a four-channel parallel modeling method to describe the attacker's ability.The modeling method solved the problem of model detection and security hidden trouble while Nayak protocol run in parallel,and optimized the model complexity and storage state.We introduced the SPIN model validation tools in this paper.The validation tool analysis shows that the symmetric key cryptography is not secure for Nayak protocol encryption.This method can be applied to formal analysis and verification of similar complex protocols.