New Session Key protocol that is much more robust

Scyther Files/SessionKeys.spdl

-
-usertype SessionKey;
-usertype Message;
-
-protocol EncrpytedExchange(Meter,Monitor)
-
-	{
-
-
-	role Meter {
-
-	fresh M: Message;
-	fresh TokenA: SessionKey;
-	var TokenB;
-
-	send_1(Meter,Monitor,{TokenA}k(k));
-	recv_2(Monitor,Meter,{TokenB}k(k));
-	claim(Meter,Running,Monitor,M);
-	send_3(Meter,Monitor,{M}k(k));
-
-	claim_Meter1(Meter, Secret, (k));
-	claim_Meter2(Meter, Secret, M);
-	claim_Meter3(Meter,Niagree);
-	claim_Meter4(Meter,Nisynch);
-
-	}
-
-	role Monitor {
-
-	var M;
-	var TokenA;
-	fresh TokenB: SessionKey;
-
-	recv_1(Meter,Monitor,{TokenA}k(k));
-	send_2(Monitor,Meter,{TokenB}k(k));
-	recv_3(Meter,Monitor,{M}k(k));
-
-	claim_Monitor1(Monitor, Secret, (k));
-	claim_Monitor2(Monitor, Secret, M);
-	claim_Meter3(Monitor,Niagree);
-	claim_Meter4(Monitor,Nisynch);
-
-
-
-	
-	   }
-
-}
+
+hashfunction  hashed;
+hashfunction sharedkey;
+usertype Message;
+usertype SessionKey;
+
+protocol KeyExchange(Monitor,CloudServer)
+{
+	role Monitor
+
+	{
+
+		fresh MonitorValue  : Nonce;
+		var CloudServerValue : Nonce;
+
+		fresh info : 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, {hashed(CloudServerValue), info} sharedkey );
+		
+		claim_Monitor1(Monitor,Niagree);
+		claim_Monitor2(Monitor,Nisynch);
+		claim_Monitor3(Monitor,  Secret, info);
+	
+	}	
+	
+	role CloudServer
+
+	{
+
+		var MonitorValue: Nonce;
+		fresh CloudServerValue: Nonce;
+
+		var info: 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, {hashed(CloudServerValue), info} sharedkey );
+
+		claim_CloudServer1(CloudServer,Niagree);
+		claim_CloudServer2(CloudServer,Nisynch);
+		claim_CloudServer3(CloudServer,  Secret, info);
+
+	}
\ No newline at end of file
+}