diff --git a/Scyther Files/MutualAuthenticationBroken.spdl b/Scyther Files/MutualAuthenticationBroken.spdl new file mode 100644 index 0000000000000000000000000000000000000000..55f5d7d86a213e588e05dbc463ea4bdff130c912 --- /dev/null +++ b/Scyther Files/MutualAuthenticationBroken.spdl @@ -0,0 +1,55 @@ + +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, {info} sharedkey ); + + recv_4(CloudServer,Monitor, {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, {info} sharedkey ); + + send_4(CloudServer,Monitor, {info} sharedkey ); + + claim_CloudServer1(CloudServer,Niagree); + claim_CloudServer2(CloudServer,Nisynch); + claim_CloudServer3(CloudServer, Secret, info); + + } +}