- Adding Kao Chow

- Adding Dennig Sacco
- Updated not modelled file to include DH, GJM and Gong

spdl/SPORE/NotModelled.txt

@@ -4,3 +4,15 @@ The following protocols have not been modelled for use in Scyther:
 This protocol only consists of one message and corresponding database actions.
 The description given in SPORE is unsuitable for formalisation.
 
+- Diffie Helman http://www.lsv.ens-cachan.fr/spore/diffieHelman.html
+This protocol relies on algebraic properties that can not be modelled in
+scyther.
+
+- GJM http://www.lsv.ens-cachan.fr/spore/gjm.html
+This protocol contains complicated if-then-else constructions that can
+not be modelled in scyther.
+
+- Gong http://www.lsv.ens-cachan.fr/spore/gong.html
+This protocol relies on algebraic properties that can not be modelled in
+scyther.
+

spdl/SPORE/denning-sacco-lowe.spdl

@@ -0,0 +1,80 @@
+# Lowe modified Denning-Sacco shared key
+#
+# Modelled after the description in the SPORE library
+# http://www.lsv.ens-cachan.fr/spore/denningSaccoLowe.html
+#
+# Note:
+# This protocol uses a ticket so scyther will only be able to verify
+# the protocol using the ARACHNE engine (-a) and type 2 matching (-m2)
+#
+# Note:
+# According to SPORE there are no attacks on this protocol, scyther
+# finds one however. This has to be investigated further.
+
+usertype Key;
+usertype Ticket;
+usertype SessionKey;
+usertype TimeStamp;
+secret k: Function;
+usertype PseudoFunction;
+const dec: PseudoFunction;
+
+protocol denningSacco(I,R,S)
+{
+	role I
+	{
+        var W: Ticket;
+		var Kir: SessionKey;
+        var T: TimeStamp;
+        var Nr: Nonce;
+
+		send_1(I,S, I,R );
+		read_2(S,I, {R, Kir, T, W}k(I,S) );
+		send_3(I,R, W);
+        read_4(R,I, {Nr}Kir);
+        send_5(I,R, {{Nr}dec}Kir);
+		claim_6(I,Niagree);
+	}	
+	
+	role R
+	{
+        var Kir: SessionKey;
+        var T: TimeStamp;
+        const Nr: Nonce;
+
+		read_3(I,R, {Kir,I,T}k(R,S));
+        send_4(R,I, {Nr}Kir);
+        read_5(I,R, {{Nr}dec}Kir);
+		claim_8(R,Niagree);
+	}
+	
+    role S
+	{
+        var W: Ticket;
+		const Kir: SessionKey;
+        const T: TimeStamp;
+
+		read_1(I,S, I,R );
+		send_2(S,I, {R, Kir, T, {Kir, I,T}k(R,S)}k(I,S));
+	}	
+}
+
+const Alice,Bob,Simon,Eve: Agent;
+
+untrusted Eve;
+const kee: SessionKey;
+const tee: TimeStamp;
+compromised k(Eve,Simon);
+
+
+
+# General scenario, 2 parallel runs of the protocol
+# Note because the modelchecker does not support tickets this might not
+# be very useful
+
+run denningSacco.I(Agent,Agent,Simon);
+run denningSacco.R(Agent,Agent,Simon);
+run denningSacco.S(Agent,Agent,Simon);
+run denningSacco.I(Agent,Agent,Simon);
+run denningSacco.R(Agent,Agent,Simon);
+run denningSacco.S(Agent,Agent,Simon);

spdl/SPORE/denning-sacco.spdl

@@ -0,0 +1,69 @@
+# Denning-Sacco shared key
+#
+# Modelled after the description in the SPORE library
+# http://www.lsv.ens-cachan.fr/spore/denningSacco.html
+#
+# Note:
+# This protocol uses a ticket so scyther will only be able to verify
+# the protocol using the ARACHNE engine (-a) and type 2 matching (-m2)
+#
+
+usertype Key;
+usertype Ticket;
+usertype SessionKey;
+usertype TimeStamp;
+secret k: Function;
+
+protocol denningSacco(I,R,S)
+{
+	role I
+	{
+        var W: Ticket;
+		var Kir: SessionKey;
+        var T: TimeStamp;
+
+		send_1(I,S, I,R );
+		read_2(S,I, {R, Kir, T, W}k(I,S) );
+		send_3(I,R, W);
+		claim_4(I,Nisynch);
+	}	
+	
+	role R
+	{
+        var Kir: SessionKey;
+        var T: TimeStamp;
+
+		read_3(I,R, {Kir,I,T}k(R,S));
+		claim_8(R,Nisynch);
+	}
+	
+    role S
+	{
+        var W: Ticket;
+		const Kir: SessionKey;
+        const T: TimeStamp;
+
+		read_1(I,S, I,R );
+		send_2(S,I, {R, Kir, T, {Kir, I,T}k(R,S)}k(I,S));
+	}	
+}
+
+const Alice,Bob,Simon,Eve: Agent;
+
+untrusted Eve;
+const kee: SessionKey;
+const tee: TimeStamp;
+compromised k(Eve,Simon);
+
+
+
+# General scenario, 2 parallel runs of the protocol
+# Note because the modelchecker does not support tickets this might not
+# be very useful
+
+run denningSacco.I(Agent,Agent,Simon);
+run denningSacco.R(Agent,Agent,Simon);
+run denningSacco.S(Agent,Agent,Simon);
+run denningSacco.I(Agent,Agent,Simon);
+run denningSacco.R(Agent,Agent,Simon);
+run denningSacco.S(Agent,Agent,Simon);

spdl/SPORE/kaochow-v2.spdl

@@ -0,0 +1,77 @@
+# Kao Chow Authentication v.2
+#
+# Modelled after the description in the SPORE library
+# http://www.lsv.ens-cachan.fr/spore/kaoChow2.html
+#
+# Note:
+# This protocol uses a ticket so scyther will only be able to verify
+# the protocol using the ARACHNE engine (-a) and type 2 matching (-m2)
+#
+
+usertype Sessionkey;
+usertype Ticket;
+secret k: Function;
+
+protocol kaochow2(I,R,S)
+{
+	role I
+	{
+		const ni: Nonce;
+		var nr: Nonce;
+		var kir,kt: Sessionkey;
+
+		send_1 (I,S, I,R,ni);
+		read_3 (R,I, R, {I,R,ni,kir,kt}k(I,S), {ni, kir}kt, nr );
+		send_4 (I,R, {nr,kir}kt );
+
+		claim_5 (I, Nisynch);
+		claim_6 (I, Niagree);
+		claim_7 (I, Secret, kir);
+	}	
+	
+	role R
+	{
+		var ni: Nonce;
+		const nr: Nonce;
+		var kir,kt: Sessionkey;
+		var T: Ticket;
+
+		read_2 (S,R, T, { I,R,ni,kir,kt }k(R,S)  ); 
+		send_3 (R,I, R, T, {ni, kir}kt, nr );
+		read_4 (I,R, {nr,kir}kt );
+
+		claim_8 (R, Nisynch);
+		claim_9 (R, Niagree);
+		claim_10 (R, Secret, kir);
+	}
+
+	role S
+	{
+		var ni: Nonce;
+		const kir, kt: Sessionkey;
+
+		read_1 (I,S, I,R,ni);
+		send_2 (S,R, {I,R,ni,kir,kt}k(I,S), { I,R,ni,kir,kt }k(R,S)  ); 
+	}
+}
+
+const Alice,Bob,Simon,Eve: Agent;
+
+untrusted Eve;
+const ne: Nonce;
+const te: Ticket;
+const ke: Sessionkey;
+compromised k(Eve,Eve);
+compromised k(Eve,Alice);
+compromised k(Eve,Bob);
+compromised k(Eve,Simon);
+compromised k(Alice,Eve);
+compromised k(Bob,Eve);
+compromised k(Simon,Eve);
+
+run kaochow2.I(Agent,Agent,Simon);
+run kaochow2.R(Agent,Agent,Simon);
+run kaochow2.S(Agent,Agent,Simon);
+run kaochow2.I(Agent,Agent,Simon);
+run kaochow2.R(Agent,Agent,Simon);
+run kaochow2.S(Agent,Agent,Simon);

spdl/SPORE/kaochow-v3.spdl

@@ -0,0 +1,80 @@
+# Kao Chow Authentication v.3
+#
+# Modelled after the description in the SPORE library
+# http://www.lsv.ens-cachan.fr/spore/kaoChow3.html
+#
+# Note:
+# This protocol uses a ticket so scyther will only be able to verify
+# the protocol using the ARACHNE engine (-a) and type 2 matching (-m2)
+#
+
+usertype Sessionkey;
+usertype Ticket;
+usertype Timestamp;
+secret k: Function;
+
+protocol kaochow3(I,R,S)
+{
+	role I
+	{
+		const ni: Nonce;
+		var nr: Nonce;
+		var kir,kt: Sessionkey;
+		var T2: Ticket;
+
+		send_1 (I,S, I,R,ni);
+		read_3 (R,I, R, {I,R,ni,kir,kt}k(I,S), {ni, kir}kt, nr, T2 );
+		send_4 (I,R, {nr,kir}kt, T2 );
+
+		claim_5 (I, Nisynch);
+		claim_6 (I, Niagree);
+		claim_7 (I, Secret, kir);
+	}	
+	
+	role R
+	{
+		var ni: Nonce;
+		const nr: Nonce;
+		var kir,kt: Sessionkey;
+		var T: Ticket;
+		const tr: Timestamp;
+
+		read_2 (S,R, T, { I,R,ni,kir,kt }k(R,S)  ); 
+		send_3 (R,I, R, T, {ni, kir}kt, nr, {I,R,tr,kir}k(R,S) );
+		read_4 (I,R, {nr,kir}kt, {I,R,tr,kir}k(R,S) );
+
+		claim_8 (R, Nisynch);
+		claim_9 (R, Niagree);
+		claim_10 (R, Secret, kir);
+	}
+
+	role S
+	{
+		var ni: Nonce;
+		const kir, kt: Sessionkey;
+
+		read_1 (I,S, I,R,ni);
+		send_2 (S,R, {I,R,ni,kir,kt}k(I,S), { I,R,ni,kir,kt }k(R,S)  ); 
+	}
+}
+
+const Alice,Bob,Simon,Eve: Agent;
+
+untrusted Eve;
+const ne: Nonce;
+const te: Ticket;
+const ke: Sessionkey;
+compromised k(Eve,Eve);
+compromised k(Eve,Alice);
+compromised k(Eve,Bob);
+compromised k(Eve,Simon);
+compromised k(Alice,Eve);
+compromised k(Bob,Eve);
+compromised k(Simon,Eve);
+
+run kaochow3.I(Agent,Agent,Simon);
+run kaochow3.R(Agent,Agent,Simon);
+run kaochow3.S(Agent,Agent,Simon);
+run kaochow3.I(Agent,Agent,Simon);
+run kaochow3.R(Agent,Agent,Simon);
+run kaochow3.S(Agent,Agent,Simon);

spdl/SPORE/kaochow.spdl

@@ -0,0 +1,77 @@
+# Kao Chow Authentication v.1
+#
+# Modelled after the description in the SPORE library
+# http://www.lsv.ens-cachan.fr/spore/kaoChow1.html
+#
+# Note:
+# This protocol uses a ticket so scyther will only be able to verify
+# the protocol using the ARACHNE engine (-a) and type 2 matching (-m2)
+#
+
+usertype Sessionkey;
+usertype Ticket;
+secret k: Function;
+
+protocol kaochow(I,R,S)
+{
+	role I
+	{
+		const ni: Nonce;
+		var nr: Nonce;
+		var kir: Sessionkey;
+
+		send_1 (I,S, I,R,ni);
+		read_3 (R,I, {I,R,ni,kir}k(I,S), {ni}kir, nr );
+		send_4 (I,R, {nr}kir );
+
+		claim_5 (I, Nisynch);
+		claim_6 (I, Niagree);
+		claim_7 (I, Secret, kir);
+	}	
+	
+	role R
+	{
+		var ni: Nonce;
+		const nr: Nonce;
+		var kir: Sessionkey;
+		var T;
+
+		read_2 (S,R, T, { I,R,ni,kir }k(R,S) ); 
+		send_3 (R,I, T, {ni}kir, nr );
+		read_4 (I,R, {nr}kir );
+
+		claim_8 (R, Nisynch);
+		claim_9 (R, Niagree);
+		claim_10 (R, Secret, kir);
+	}
+
+	role S
+	{
+		var ni: Nonce;
+		const kir: Sessionkey;
+
+		read_1 (I,S, I,R,ni);
+		send_2 (S,R, {I,R,ni,kir}k(I,S), { I,R,ni,kir }k(R,S)  ); 
+	}
+}
+
+const Alice,Bob,Simon,Eve: Agent;
+
+untrusted Eve;
+const ne: Nonce;
+const te: Ticket;
+const ke: Sessionkey;
+compromised k(Eve,Eve);
+compromised k(Eve,Alice);
+compromised k(Eve,Bob);
+compromised k(Eve,Simon);
+compromised k(Alice,Eve);
+compromised k(Bob,Eve);
+compromised k(Simon,Eve);
+
+run kaochow.I(Agent,Agent,Simon);
+run kaochow.R(Agent,Agent,Simon);
+run kaochow.S(Agent,Agent,Simon);
+run kaochow.I(Agent,Agent,Simon);
+run kaochow.R(Agent,Agent,Simon);
+run kaochow.S(Agent,Agent,Simon);