hashfunction  hashed;
hashfunction sharedkey;
usertype Message;
usertype SessionKey;

protocol MutualAuthentication(Monitor,CloudServer)
{
	role Monitor {

		fresh MonitorValue  : Nonce;
		var CloudServerValue : Nonce;

		fresh MonitorInformation : Message;
		var CloudServerInformation: Message;
		fresh sharedkey: SessionKey;


		send_1(Monitor,CloudServer,{Monitor,MonitorValue}pk(CloudServer));
		
		recv_2(CloudServer,Monitor, {CloudServerValue,hashed(MonitorValue),
		CloudServer}pk(Monitor));
		
		send_3(Monitor,CloudServer,{CloudServerValue, MonitorInformation} sharedkey );
		
		recv_4(CloudServer,Monitor,{MonitorValue,CloudServerInformation} sharedkey);
		
		claim_Monitor1(Monitor,Niagree);
		claim_Monitor2(Monitor,Nisynch);
		claim_Monitor3(Monitor,  Secret, CloudServerInformation);
		claim_Monitor4(Monitor,Alive);

	}	
	
	role CloudServer {

		var MonitorValue: Nonce;
		fresh CloudServerValue: Nonce;

		fresh CloudServerInformation: Message;
		var MonitorInformation: Message;
		var sharedkey: SessionKey;

		recv_1(Monitor,CloudServer,{Monitor,MonitorValue}pk(CloudServer));
		send_2(CloudServer,Monitor, {CloudServerValue,hashed(MonitorValue),
		CloudServer}pk(Monitor));
		
		recv_3(Monitor,CloudServer, {CloudServerValue, MonitorInformation} sharedkey );
		
		send_4(CloudServer,Monitor,{MonitorValue,CloudServerInformation} sharedkey);
		
		claim_CloudServer1(CloudServer,Niagree);
		claim_CloudServer2(CloudServer,Nisynch);
		claim_CloudServer3(CloudServer,  Secret, MonitorInformation);
		claim_CloudServer4(CloudServer,Alive);

	}
}