Formal Analysis And Research On Mutual Authentication Protocol For Cloud User

With the rapid development of information networks,cloud service has already come into people's life.However,most users believe cloud computing system cannot protect their private information and data security,so they are not willing to use it.Cloud security protocol is a tool,which can guarantee the safety of cloud communication environment.Because of facing the secure challenges,cloud security protocol should be complicatedly designed.Nayak protocol is a password authentication scheme,which is based on the bidirectional authentication and session key agreement in the cloud environment.This scheme does not depend on the digital certification,instead it is through the simple sharing and easy password to authenticate and exchange for secret key.Whereas,because Nayak protocol generally set easy password,so it is vulnerable to attack from dictionary,intermediate,and internal personal.This paper selects Nayak protocol as the research objective,then uses formal methods to solve problems that Nayak protocol has.(1)To analyze and verify the Nayak protocol,the model checking technology is applied.Firstly,the symmetric key cryptography is adopted to encrypting the Nayak protocol.Then a four-channel parallel modeling method is set up to clarify attackers' abilities based on the Dolev-Yao attacker model.Finally,the SPIN model verification tool is applied to check the symmetric key cryptosystem out whether or not the threats will destroy the Nayak protocol encryption.(2)Nayak protocol's defects and security problems is analyzed systematically,and the time stamp technology is set up with private key signature.Throughout the double encryption method extensively applied by adding the time stamp during the message routing period and changing the encryption,the the communication security of both sides can be guaranteed.The four-channel parallel modeling method is adopted to build the Nayak protocol,while verifying the protocol's security with spin.(3)There are three strategies that can optimize the Nayak protocol model,such as type checking,syntax reordering and static analysis.These optimized strategies can achieve state space reduction and storage space compression to help Nayak protocol obtain the optimal security.(4)This paper comes up with a four channel parallel modeling method,which can solve the problem of repeated sub message items,and multi round protocol parallelism,and reduces either the amount of state migration produced by cross operation or the complexity of the model.This modeling method is universal,and it also can be applied to formal analysis and verification of similar complex protocols.