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

Security analysis of Nayak-T protocol based on time stamp and private key signature

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

With the rapid development of information networks, cloud services step into people＇s vision and the problems of information security in the cloud environment become a focus. Nayak protocol is a password authentication scheme based on the bidirectional authentication and session key agreement in the cloud environment. Targeting at man-in-the-middle attacks existing in Nayak protocol, we put forward an improved Nayak-T protocol. Nayak-T protocol adds in time stamp and changes their encryption ways inside message options to ensure the security of two-way communication through double encryption. We use the four channels parallel modeling method to model Nayak-T protocol and adopt SPIN to verify the security of this protocol. Analysis of modeling optimization strategies proves that the model testing that adopts static analysis, type checking and syntax reordering are most efficient. This method can be applied to the formal analysis and verification of similar complicated protocols.