diff --git a/Scyther Files/MutualAuthentication.spdl b/Scyther Files/MutualAuthentication.spdl new file mode 100644 index 0000000000000000000000000000000000000000..4906eecf2099230071c0400608f03b4afd1179b5 --- /dev/null +++ b/Scyther Files/MutualAuthentication.spdl @@ -0,0 +1,56 @@ + +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); + + } +}