- Added two versions of the kao-chow protocol.

- Improved the testing scripts.

spdl/kaochow-v2.spdl

@@ -0,0 +1,67 @@
+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/kaochow-v3.spdl

@@ -0,0 +1,70 @@
+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/kaochow.spdl

@@ -26,7 +26,7 @@ protocol kaochow(I,R,S)
 		var kir: Sessionkey;
 		var T;
 
-		read_2 (S,R, { T, { I,R,ni,kir }k(R,S) }k(R,S) ); 
+		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 );
 

test/multiprotocoltest.py

@@ -98,13 +98,13 @@ def ScytherEval (plist):
 	sys.stdout.flush()
 	sys.stderr.flush()
 
-	args = scythertest.default_arguments(plist, options.match, options.bounds)
+	args = scythertest.default_arguments(plist, int(options.match), int(options.bounds))
 	n = len(plist)
 	if not (n,args) in ArgumentsList:
 		ArgumentsList.append((n,args))
 		print "Testing",n,"tuples using",args
 
-	return scythertest.default_parsed(plist, options.match, options.bounds)
+	return scythertest.default_parsed(plist, int(options.match), int(options.bounds))
 
 # ScytherEval1
 #
@@ -475,30 +475,29 @@ def banner(str):
 def the_great_houdini(list,width,match):
 	global options
 
+	# Empty list
 	if list == []:
-		list = protocollist.select(int(options.protocols))
-		the_great_houdini(list,width,match)
-		return
-
-	if options.sequence:
+		the_great_houdini(protocollist.select(int(options.protocols)),width,match)
+	# Unfold sequence of tuple widths
+	elif options.sequence:
 		options.sequence = False
 		banner ("Testing multiple tuple widths")
 		for n in range(2,4):
 			banner ("Testing tuple width %i" % n)
 			the_great_houdini(list,n,match)
 		options.sequence = True
-		return 
-
-	if options.allmatch:
+	# Unfold matching methods
+	elif options.allmatch:
 		options.allmatch = False
 		banner ("Testing multiple match methods")
 		for m in range(0,3):
+			options.match = m
 			banner ("Testing match %i" % m)
 			the_great_houdini(list,width,m)
 		options.allmatch = True
-		return
-
-	multiprotocol_test(list,width,match)
+	# Last but not least: test
+	else:
+		multiprotocol_test(list,width,match)
 	
 
 def main():

test/protocollist.py

@@ -1,3 +1,4 @@
+#!/usr/bin/python
 #
 #	protocol list
 #
@@ -22,6 +23,8 @@ def from_literature():
 	"isoiec11770-2-13.spdl",
 	"kaochow-palm.spdl",
 	"kaochow.spdl",
+	"kaochow-v2.spdl",
+	"kaochow-v3.spdl",
 	"ns3.spdl",
 	"nsl3.spdl",
 	"nsl7.spdl",
@@ -81,4 +84,15 @@ def select(type):
 	else:
 		# Otherwise empty list
 		return []
-		
+
+
+
+
+def main():
+	for l in [from_literature(), from_others()]:
+		for p in l:
+			print p
+		print
+
+if __name__ == '__main__':
+	main()

test/scythertest.py

@@ -53,7 +53,7 @@ def default_protocols(plist):
 # 	1: thorough
 #
 def default_arguments(plist,match,bounds):
-	n = len(plist)
+	n = 2 + bounds
 	# These bounds assume at least two protocols, otherwise
 	# stuff breaks.
 	if n < 2: