From 4047f922c0045c0ff0e0cc7a9fc8028864059943 Mon Sep 17 00:00:00 2001
From: Matthew Hutchings <mwh1g17@soton.ac.uk>
Date: Thu, 11 Jun 2020 13:28:13 +0100
Subject: [PATCH] Reorganised Project Protocols
Added a example protocols folder for example/learning protocols not featured in the final implementation
---
.../EncryptedExchange.spdl | 78 +++++++++----------
.../{ => Example Protocols}/HelloWorld.spdl | 0
.../{ => Example Protocols}/KeyExchange.spdl | 0
.../MutualAuthentication.spdl | 0
.../MutualAuthenticationBroken.spdl | 0
.../SendAndConfirm.spdl | 0
.../{ => Example Protocols}/SessionKeys.spdl | 0
.../ImplicitKeyAuthentication.spdl.txt | 49 ++++++++++++
Scyther Files/MessageEncryption.spdl.txt | 31 ++++++++
Scyther Files/MutualAuthentication.spdl.txt | 57 ++++++++++++++
Scyther Files/Production Protocols/.gitkeep | 0
Scyther Files/SessionKeys.spdl.txt | 49 ++++++++++++
12 files changed, 225 insertions(+), 39 deletions(-)
rename Scyther Files/{ => Example Protocols}/EncryptedExchange.spdl (92%)
rename Scyther Files/{ => Example Protocols}/HelloWorld.spdl (100%)
rename Scyther Files/{ => Example Protocols}/KeyExchange.spdl (100%)
rename Scyther Files/{ => Example Protocols}/MutualAuthentication.spdl (100%)
rename Scyther Files/{ => Example Protocols}/MutualAuthenticationBroken.spdl (100%)
rename Scyther Files/{ => Example Protocols}/SendAndConfirm.spdl (100%)
rename Scyther Files/{ => Example Protocols}/SessionKeys.spdl (100%)
create mode 100644 Scyther Files/ImplicitKeyAuthentication.spdl.txt
create mode 100644 Scyther Files/MessageEncryption.spdl.txt
create mode 100644 Scyther Files/MutualAuthentication.spdl.txt
delete mode 100644 Scyther Files/Production Protocols/.gitkeep
create mode 100644 Scyther Files/SessionKeys.spdl.txt
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 1207838..6661458 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 0000000..4e0a655
--- /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 0000000..cdb06a1
--- /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 0000000..ddb305a
--- /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 e69de29..0000000
diff --git a/Scyther Files/SessionKeys.spdl.txt b/Scyther Files/SessionKeys.spdl.txt
new file mode 100644
index 0000000..f470264
--- /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
--
GitLab