From 334317ae28f1fa9618f09d3054a37759a57e54f3 Mon Sep 17 00:00:00 2001
From: mwh1g17 <mwh1g17@soton.ac.uk>
Date: Mon, 30 Mar 2020 13:09:48 +0100
Subject: [PATCH] SessionKeys Protocol
---
Scyther Files/SessionKeys.spdl | 48 ++++++++++++++++++++++++++++++++++
1 file changed, 48 insertions(+)
create mode 100644 Scyther Files/SessionKeys.spdl
diff --git a/Scyther Files/SessionKeys.spdl b/Scyther Files/SessionKeys.spdl
new file mode 100644
index 0000000..65305c8
--- /dev/null
+++ b/Scyther Files/SessionKeys.spdl
@@ -0,0 +1,48 @@
+
+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);
+
+
+
+
+ }
+
+}
\ No newline at end of file
--
GitLab