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.