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

关键词：nayak协议 模型检测 私钥签名 时间戳 

单位：华东交通大学软件学院; 江西南昌330013; 池州职业技术学院; 安徽池州247100