- Added KSL protocol (modified Kerberos)

- Removed bkepk (duplicate of bke)

spdl/bkepk.spdl

@@ -1,60 +0,0 @@
-/* 
-	Bilateral Key Exchange with Public Key protocol (BKEPK)
-
-	CMV version with explicit secrecy claims.
-*/
-
-usertype Key;
-
-const pk,hash: Function;
-secret sk,unhash: Function;
-
-inversekeys (pk,sk);
-inversekeys (hash,unhash);
-
-protocol bkepk(A,B)
-{
-	role B
-	{
-		const nb: Nonce;
-		var na: Nonce;
-		var kab: Key;
-
-		send_1 (B,A, B,{ nb,B }pk(A) );
-		read_2 (A,B, { hash(nb),na,A,kab }pk(B) );
-		send_3 (B,A, { hash(na) }kab );
-
-		claim_4 (B, Secret, na );
-		claim_5 (B, Secret, nb );
-		claim_6 (B, Niagree );
-		claim_7 (B, Nisynch );
-	}
-
-	role A
-	{
-		var nb: Nonce;
-		const na: Nonce;
-		const kab: Key;
-
-		read_1 (B,A, B,{ nb,B }pk(A) );
-		send_2 (A,B, { hash(nb),na,A,kab }pk(B) );
-		read_3 (B,A, { hash(na) }kab );
-
-		claim_8 (A, Secret, na );
-		claim_9 (A, Secret, nb );
-		claim_10 (A, Niagree);
-		claim_11 (A, Nisynch);
-	}
-}
-
-const Alice,Bob,Eve;
-
-compromised sk(Eve);
-untrusted Eve;
-
-run bkepk.A(Alice,Bob);
-run bkepk.B(Alice,Bob);
-run bkepk.A(Alice,Bob);
-run bkepk.B(Alice,Bob);
-
-

spdl/ksl.spdl

@@ -0,0 +1,83 @@
+/*
+ * KSL from SPORE
+ *
+ * Messages 6-8 are intended for repeated authentication, and there are
+ * known attacks on this. However, we don't model that yet.
+ *
+ * Furthermore, it is interesting to experiment here with key
+ * compromise (of kab), when this is implemented in Scyther.
+ */
+
+usertype Server, SessionKey, GeneralizedTimestamp, Ticket, TicketKey;
+secret k: Function;
+
+const a, b, e: Agent;
+const s: Server;
+
+/* give the intruder something to work with */
+
+const ne: Nonce;
+const kee: SessionKey;
+untrusted e;
+compromised k(e,s);
+
+protocol ksl(A,B,S)
+{
+	role A
+	{
+		const Na, Ma: Nonce;
+		var Nc, Mb: Nonce;
+		var T: Ticket;
+		var Kab: SessionKey;
+		
+		send_1(A,B, Na, A);
+		read_4(B,A, { Na,B,Kab }k(A,S), T, Nc, {Na}Kab );
+		send_5(A,B, { Nc }Kab );
+		
+		send_6(A,B, Ma,T );
+		read_7(B,A, Mb,{Ma}Kab );
+		send_8(A,B, {Mb}Kab );
+
+		claim_A1(A,Secret, Kab);
+		claim_A2(A,Niagree);
+		claim_A3(A,Nisynch);
+	}
+
+	role B
+	{
+		var Na,Ma: Nonce;
+		const Nb,Nc,Mb: Nonce;
+		var Kab: SessionKey;
+		const Kbb: TicketKey;
+		const Tb: GeneralizedTimestamp;
+		var T: Ticket;
+		
+		read_1(A,B, Na, A);
+		send_2(B,S, Na, A, Nb, B );
+		read_3(S,B, { Nb, A, Kab }k(B,S), T );
+		send_4(B,A, T, { Tb, A, Kab }Kbb, Nc, {Na}Kab );
+		read_5(A,B, { Nc }Kab );
+		
+		read_6(A,B, Ma,{ Tb, A, Kab }Kbb );
+		send_7(B,A, Mb,{Ma}Kab );
+		read_8(A,B, {Mb}Kab );
+
+		claim_B1(B,Secret, Kab);
+		claim_B2(B,Niagree);
+		claim_B3(B,Nisynch);
+	}
+
+	role S
+	{
+		var Na, Nb: Nonce;
+		const Kab: SessionKey;
+
+		read_2(B,S, Na, A, Nb, B );
+		send_3(S,B, { Nb, A, Kab }k(B,S), { Na,B,Kab }k(A,S) );
+	}
+}
+
+run ksl.A(a,b,s);
+run ksl.B(a,b,s);
+run ksl.S(a,b,s);
+

test/multiprotocoltest.py

@@ -319,7 +319,7 @@ def RequiresAllProtocols (protocols, claim):
 			simplercase.remove(redundantfile)
 			# now test the validity of the claim
 			simplerresults = ScytherEval (simplercase)
-			if simplerresults[claim] == 0:
+			if claim in simplerresults.keys() and simplerresults[claim] == 0:
 				# Redundant protocol was not necessary for attack!
 				return 0
 	return 1

test/protocollist.py

@@ -13,7 +13,6 @@ def from_literature():
 	list = [ \
 	"andrew-ban.spdl",
 	"andrew-lowe-ban.spdl",
-	"bkepk.spdl",
 	"bke.spdl",
 	"boyd.spdl",
 	"ccitt509-ban.spdl",
@@ -25,6 +24,7 @@ def from_literature():
 	"kaochow.spdl",
 	"kaochow-v2.spdl",
 	"kaochow-v3.spdl",
+	"ksl.spdl",
 	"ns3.spdl",
 	"nsl3.spdl",
 	"nsl7.spdl",