diff --git a/Scyther Files/EncryptedExchange.spdl b/Scyther Files/Example Protocols/EncryptedExchange.spdl similarity index 92% rename from Scyther Files/EncryptedExchange.spdl rename to Scyther Files/Example Protocols/EncryptedExchange.spdl index 120783850095aa39cf36394b5527d706ae104c22..66614586f8fb89188f0c9e6ef35f9d02a0e5ae20 100644 --- a/Scyther Files/EncryptedExchange.spdl +++ b/Scyther Files/Example Protocols/EncryptedExchange.spdl @@ -1,40 +1,40 @@ - - - -protocol EncrpytedExchange(Meter,Monitor) - - { - - role Meter { - - fresh M: Nonce; - var Confirm; - - send_1(Meter,Monitor,{M}k(k)); - recv_2(Monitor,Meter,{Confirm}k(k)); - - claim_Meter1(Meter, Secret, (k)); - claim_Meter2(Meter, Secret, M); - - - - - } - - role Monitor { - - var M; - fresh Confirm: Nonce; - - recv_1(Meter,Monitor,{M}k(k)); - send_2(Monitor,Meter,{Confirm}k(k)); - - claim_Monitor1(Monitor, Secret, (k)); - claim_Monitor2(Monitor, Secret, M); - - - - - } - + + + +protocol EncrpytedExchange(Meter,Monitor) + + { + + role Meter { + + fresh M: Nonce; + var Confirm; + + send_1(Meter,Monitor,{M}k(k)); + recv_2(Monitor,Meter,{Confirm}k(k)); + + claim_Meter1(Meter, Secret, (k)); + claim_Meter2(Meter, Secret, M); + + + + + } + + role Monitor { + + var M; + fresh Confirm: Nonce; + + recv_1(Meter,Monitor,{M}k(k)); + send_2(Monitor,Meter,{Confirm}k(k)); + + claim_Monitor1(Monitor, Secret, (k)); + claim_Monitor2(Monitor, Secret, M); + + + + + } + } \ No newline at end of file diff --git a/Scyther Files/HelloWorld.spdl b/Scyther Files/Example Protocols/HelloWorld.spdl similarity index 100% rename from Scyther Files/HelloWorld.spdl rename to Scyther Files/Example Protocols/HelloWorld.spdl diff --git a/Scyther Files/KeyExchange.spdl b/Scyther Files/Example Protocols/KeyExchange.spdl similarity index 100% rename from Scyther Files/KeyExchange.spdl rename to Scyther Files/Example Protocols/KeyExchange.spdl diff --git a/Scyther Files/MutualAuthentication.spdl b/Scyther Files/Example Protocols/MutualAuthentication.spdl similarity index 100% rename from Scyther Files/MutualAuthentication.spdl rename to Scyther Files/Example Protocols/MutualAuthentication.spdl diff --git a/Scyther Files/MutualAuthenticationBroken.spdl b/Scyther Files/Example Protocols/MutualAuthenticationBroken.spdl similarity index 100% rename from Scyther Files/MutualAuthenticationBroken.spdl rename to Scyther Files/Example Protocols/MutualAuthenticationBroken.spdl diff --git a/Scyther Files/SendAndConfirm.spdl b/Scyther Files/Example Protocols/SendAndConfirm.spdl similarity index 100% rename from Scyther Files/SendAndConfirm.spdl rename to Scyther Files/Example Protocols/SendAndConfirm.spdl diff --git a/Scyther Files/SessionKeys.spdl b/Scyther Files/Example Protocols/SessionKeys.spdl similarity index 100% rename from Scyther Files/SessionKeys.spdl rename to Scyther Files/Example Protocols/SessionKeys.spdl diff --git a/Scyther Files/ImplicitKeyAuthentication.spdl.txt b/Scyther Files/ImplicitKeyAuthentication.spdl.txt new file mode 100644 index 0000000000000000000000000000000000000000..4e0a6556aba3e1161dd28432fbc4f5501ed55682 --- /dev/null +++ b/Scyther Files/ImplicitKeyAuthentication.spdl.txt @@ -0,0 +1,49 @@ +hashfunction hashed; +usertype Message; + +protocol KeyExchange(Monitor,CloudServer) +{ + role Monitor + + { + + fresh MonitorValue : Nonce; + fresh Confirm: Message; + var CloudServerValue : Nonce; + + send_1(Monitor,CloudServer,{Monitor,MonitorValue}pk(CloudServer)); + + recv_2(CloudServer,Monitor, {CloudServerValue,hashed(MonitorValue), + CloudServer}pk(Monitor)); + + send_3(Monitor,CloudServer, hashed(CloudServerValue, Confirm)); + + claim_Monitor1(Monitor,Niagree); + claim_Monitor2(Monitor,Nisynch); + claim_Monitor3(Monitor, Secret, MonitorValue); + claim_Monitor4(Monitor, Secret, CloudServerValue); + + } + + role CloudServer + + { + + var MonitorValue: Nonce; + var Confirm: Message; + fresh CloudServerValue: Nonce; + + recv_1(Monitor,CloudServer,{Monitor,MonitorValue}pk(CloudServer)); + + send_2(CloudServer,Monitor, {CloudServerValue,hashed(MonitorValue), + CloudServer}pk(Monitor)); + + recv_3(Monitor,CloudServer, hashed(CloudServerValue, Confirm)); + + claim_CloudServer1(CloudServer,Niagree); + claim_CloudServer2(CloudServer,Nisynch); + claim_CloudServer3(CloudServer, Secret, MonitorValue); + claim_CloudServer4(CloudServer, Secret, CloudServerValue); + + } +} \ No newline at end of file diff --git a/Scyther Files/MessageEncryption.spdl.txt b/Scyther Files/MessageEncryption.spdl.txt new file mode 100644 index 0000000000000000000000000000000000000000..cdb06a170662c13cb581364a00cd3c3aeabed083 --- /dev/null +++ b/Scyther Files/MessageEncryption.spdl.txt @@ -0,0 +1,31 @@ +protocol smartExchange(Meter,Monitor) + { + + role Meter { + + fresh Message: Nonce; + var Confirm; + + send_1(Meter,Monitor,{Message}k(k)); + + recv_2(Monitor,Meter,{Confirm}k(k)); + + claim_Meter1(Meter, Secret, (k)); + claim_Meter2(Meter, Secret, Message); + + } + + role Monitor { + + var Message; + fresh Confirm: Nonce; + + recv_1(Meter,Monitor,{Message}k(k)); + + send_2(Monitor,Meter,{Confirm}k(k)); + + claim_Monitor1(Monitor, Secret, (k)); + claim_Monitor2(Monitor, Secret, Message); + } + +} \ No newline at end of file diff --git a/Scyther Files/MutualAuthentication.spdl.txt b/Scyther Files/MutualAuthentication.spdl.txt new file mode 100644 index 0000000000000000000000000000000000000000..ddb305af8daadfdc16824c2fbf1f84de4999fb03 --- /dev/null +++ b/Scyther Files/MutualAuthentication.spdl.txt @@ -0,0 +1,57 @@ +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); + + } +} \ No newline at end of file diff --git a/Scyther Files/Production Protocols/.gitkeep b/Scyther Files/Production Protocols/.gitkeep deleted file mode 100644 index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..0000000000000000000000000000000000000000 diff --git a/Scyther Files/SessionKeys.spdl.txt b/Scyther Files/SessionKeys.spdl.txt new file mode 100644 index 0000000000000000000000000000000000000000..f470264c04fb510178e559ff90a7b721d7121f4f --- /dev/null +++ b/Scyther Files/SessionKeys.spdl.txt @@ -0,0 +1,49 @@ +hashfunction hashed; +hashfunction sharedkey; +usertype Message; +usertype SessionKey; + +protocol SessionKeys(Monitor,CloudServer) { + + role Monitor { + + fresh MonitorValue : Nonce; + var CloudServerValue : Nonce; + + fresh info : Message; + var 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); + + claim_Monitor1(Monitor,Alive); + claim_Monitor2(Monitor,Secret, info); + } + + role CloudServer { + + var MonitorValue: Nonce; + fresh CloudServerValue: Nonce; + + var info: Message; + fresh info: Message; + fresh 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); + + claim_CloudServer1(CloudServer,Niagree); + claim_CloudServer2(CloudServer,Nisynch); + claim_CloudServer3(CloudServer,Alive); + claim_CloudServer4(CloudServer,Secret, info); + } +} \ No newline at end of file