- Adding CJ modified version of splice protocol

- Adding tmn
- Fixed a modelling error in splice

spdl/SPORE/splice-as-cj.spdl

@@ -0,0 +1,83 @@
+# Clark and Jacob modified Hwang and Chen modified SPLICE/AS
+#
+# Modelled after the description in the SPORE library
+# http://www.lsv.ens-cachan.fr/spore/spliceas3.html
+#
+# Note:
+# The assumptions made here do not comply with those in SPORE 
+# SPORE assumes that the agents do not know the pk function, but only
+# their own public key values. 
+# This can currently not be modelled.
+
+
+usertype TimeStamp, LifeTime;
+
+const pk: Function;
+secret sk: Function;
+inversekeys (pk,sk);
+const inc,dec: Function;
+inversekeys (inc,dec);
+
+protocol spliceASCJ(I,R,S)
+{
+        role I
+	{
+		const N1,N2: Nonce;
+		const T: TimeStamp;
+		const L: LifeTime;
+
+		send_1(I,S,  I, R, N1 );
+		read_2(S,I,  S, {S, I, N1, R, pk(R)}sk(S) );
+		send_3(I,R,  I, R, {T, L, {I, N2}pk(R)}sk(I) );
+		read_6(R,I,  R, I, {{N2}inc}pk(I) );
+
+		claim_7(I, Secret, N2);
+		claim_9(I, Niagree);
+		claim_10(I, Nisynch);
+	}
+
+	role S
+	{
+		var N1,N3: Nonce;
+
+		read_1(I,S,  I, R, N1 );
+		send_2(S,I,  S, {S, I, N1, R, pk(R)}sk(S) );
+		read_4(R,S, R, I, N3 );
+		send_5(S,R,  S, {S, R, N3, pk(I)}sk(S) );
+	}
+
+	role R
+	{
+		const N3: Nonce;
+		var N2: Nonce;
+		var T: TimeStamp;
+		var L: LifeTime;
+
+		var ni: Nonce;
+		const nr: Nonce;
+
+		read_3(I,R, I, R, {T, L, {I, N2}pk(R)}sk(I) );
+		send_4(R,S, R, I, N3 );
+		read_5(S,R, S, {S, R, N3, pk(I)}sk(S) );
+		send_6(R,I, R, I, {{N2}inc}pk(I) );
+
+		claim_8(R, Secret, N2);
+		claim_11(R, Niagree);
+		claim_12(R, Nisynch);
+	}
+}
+
+const Alice,Bob,Simon,Eve: Agent;
+
+untrusted Eve;
+const ne: Nonce;
+compromised sk(Eve);
+
+run spliceASCJI(Agent,Agent,Agent);
+run spliceASCJR(Agent,Agent,Agent);
+run spliceASCJS(Agent,Agent,Agent);
+
+#run spliceASCJ.I(Alice,Bob,Simon);
+#run spliceASCJ.R(Alice,Bob,Simon);
+#run spliceASCJ.S(Alice,Bob,Simon);
+

spdl/SPORE/splice-as-hc.spdl

@@ -13,7 +13,7 @@ inversekeys (pk,sk);
 const inc,dec: Function;
 inversekeys (inc,dec);
 
-protocol spliceAS(I,R,S)
+protocol spliceASHC(I,R,S)
 {
         role I
 	{
@@ -23,7 +23,7 @@ protocol spliceAS(I,R,S)
 
 		send_1(I,S,  I, R, N1 );
 		read_2(S,I,  S, {S, I, N1, R, pk(R)}sk(S) );
-		send_3(I,R,  I, R, {I, T, L, {N2}pk(R)}sk(R) );
+		send_3(I,R,  I, R, {I, T, L, {N2}pk(R)}sk(I) );
 		read_6(R,I,  R, I, {R, {N2}inc}pk(I) );
 
 		claim_7(I, Secret, N2);
@@ -62,14 +62,18 @@ protocol spliceAS(I,R,S)
 	}
 }
 
-const Al,Bo,Eve: Agent;
+const Alice,Bob,Simon,Eve: Agent;
 
 untrusted Eve;
 const ne: Nonce;
 compromised sk(Eve);
 
-run spliceAS.I(Agent,Agent,Agent);
+#run spliceASHC.I(Alice,Bob,Simon);
-run spliceAS.R(Agent,Agent,Agent);
+#run spliceASHC.R(Alice,Bob,Simon);
-run spliceAS.S(Agent,Agent,Agent);
+#run spliceASHC.S(Alice,Bob,Simon);
+
+run spliceASHC.I(Agent,Agent,Agent);
+run spliceASHC.R(Agent,Agent,Agent);
+run spliceASHC.S(Agent,Agent,Agent);
 
 

spdl/SPORE/splice-as.spdl

@@ -3,6 +3,11 @@
 # Modelled after the description in the SPORE library
 # http://www.lsv.ens-cachan.fr/spore/spliceas.html
 #
+# Note:
+# The assumptions made here do not comply with those in SPORE 
+# SPORE assumes that the agents do not know the pk function, but only
+# their own public key values. 
+# This can currently not be modelled.
 
 
 usertype TimeStamp, LifeTime;
@@ -23,7 +28,7 @@ protocol spliceAS(I,R,S)
 
 		send_1(I,S,  I, R, N1 );
 		read_2(S,I,  S, {S, I, N1, pk(R)}sk(S) );
-		send_3(I,R,  I, R, {I, T, L, {N2}pk(R)}sk(R) );
+		send_3(I,R,  I, R, {I, T, L, {N2}pk(R)}sk(I) );
 		read_6(R,I,  R, I, {R, {N2}inc}pk(I) );
 
 		claim_7(I, Secret, N2);
@@ -62,7 +67,7 @@ protocol spliceAS(I,R,S)
 	}
 }
 
-const Al,Bo,Eve: Agent;
+const Alice,Bob,Simon,Eve: Agent;
 
 untrusted Eve;
 const ne: Nonce;
@@ -72,4 +77,7 @@ run spliceAS.I(Agent,Agent,Agent);
 run spliceAS.R(Agent,Agent,Agent);
 run spliceAS.S(Agent,Agent,Agent);
 
+#run spliceAS.I(Alice,Bob,Simon);
+#run spliceAS.R(Alice,Bob,Simon);
+#run spliceAS.S(Alice,Bob,Simon);
 

spdl/SPORE/tmn.spdl

@@ -0,0 +1,65 @@
+# TMN
+#
+# Modelled after the description in the SPORE library
+# http://www.lsv.ens-cachan.fr/spore/tmn.html
+#
+
+usertype Key;
+
+const pk: Function;
+secret sk: Function;
+inversekeys(pk,sk);
+
+protocol tmn(I,R,S)
+{
+	role I
+	{
+		const Ki: Key;
+		var Kr: Key;
+
+		send_1(I,S, R,{Ki}pk(S) );
+		read_4(S,I, R,{Kr}Ki );
+
+		claim_I1(I,Secret,Ki);
+		claim_I2(I,Secret,Kr);
+	}	
+	
+	role R
+	{
+		const Kr: Key;
+
+		read_2(S,R, I );
+		send_3(R,S, I, { Kr }pk(S) );
+
+		claim_R1(R,Secret,Kr);
+	}
+
+	role S
+	{
+		var Ki,Kr: Key;
+
+		read_1(I,S, R,{Ki}pk(S) );
+		send_2(S,R, I );
+		read_3(R,S, I, { Kr }pk(S) );
+		send_4(S,I, R,{Kr}Ki );
+	}
+}
+
+const Alice,Bob,Eve,Simon: Agent;
+const Ke: Key;
+
+
+untrusted Eve;
+compromised sk(Eve);
+
+# Scenario to recreate an attack in SPORE
+#run tmn.I (Alice,Bob,Simon);
+#run tmn.R (Alice,Bob,Simon);
+#run tmn.S (Alice,Bob,Simon);
+
+run tmn.I (Agent,Agent,Simon);
+run tmn.R (Agent,Agent,Simon);
+run tmn.S (Agent,Agent,Simon);
+
+
+