- Improved the arguments adapting to the input stuff (e.g. number of

protocols)
- Improved many protocols by adding agreement claims.

spdl/andrew-ban.spdl

@@ -14,6 +14,7 @@ protocol andrewBan(I,R)
 		send_3(I,R, {nr}k(I,R) );
 		read_4(R,I, {kir,nr2,ni}k(I,R) );
 		claim_5(I,Nisynch);
+		claim_5b(I,Niagree);
 		claim_6(I,Secret, kir);
 		claim_7(I,Secret, k(I,R));
 	}	
@@ -29,6 +30,7 @@ protocol andrewBan(I,R)
 		read_3(I,R, {nr}k(I,R) );
 		send_4(R,I, {kir,nr2,ni}k(I,R) );
 		claim_8(R,Nisynch);
+		claim_8b(R,Niagree);
 		claim_9(R,Secret, kir);
 		claim_10(R,Secret, k(I,R));
 	}

spdl/andrew-lowe-ban.spdl

@@ -14,6 +14,7 @@ protocol andrewLoweBan(I,R)
 		send_3(I,R, {ni}kir );
 		read_4(R,I, nr );
 		claim_5(I,Nisynch);
+		claim_5b(I,Niagree);
 		claim_6(I,Secret, kir);
 		claim_7(I,Secret, k(I,R));
 	}	
@@ -29,6 +30,7 @@ protocol andrewLoweBan(I,R)
 		read_3(I,R, {ni}kir );
 		send_4(R,I, nr );
 		claim_8(R,Nisynch);
+		claim_8b(R,Niagree);
 		claim_9(R,Secret, kir);
 		claim_10(R,Secret, k(I,R));
 	}

spdl/bke.spdl

@@ -22,6 +22,7 @@ protocol bke(I,R)
 		read_2 (R,I, { hash(ni),nr,R,kir }pk(I) );
 		send_3 (I,R, { hash(nr) }kir );
 		claim_4 (I, Secret, kir );
+		claim_5 (I, Niagree );
 		claim_6 (I, Nisynch );
 	}
 
@@ -34,8 +35,9 @@ protocol bke(I,R)
 		read_1 (I,R, { ni,I }pk(R) );
 		send_2 (R,I, { hash(ni),nr,R,kir }pk(I) );
 		read_3 (I,R, { hash(nr) }kir );
-		claim_5 (R, Secret, kir );
+		claim_7 (R, Secret, kir );
-		claim_7 (R, Nisynch );
+		claim_8 (R, Niagree );
+		claim_9 (R, Nisynch );
 	}
 }
 

spdl/bkepk.spdl

@@ -23,8 +23,11 @@ protocol bkepk(A,B)
 		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
@@ -36,8 +39,11 @@ protocol bkepk(A,B)
 		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_6 (A, Secret, na );
+
-		claim_7 (A, Secret, nb );
+		claim_8 (A, Secret, na );
+		claim_9 (A, Secret, nb );
+		claim_10 (A, Niagree);
+		claim_11 (A, Nisynch);
 	}
 }
 

spdl/ccitt509-ban.spdl

@@ -19,6 +19,7 @@ protocol ccitt509(I,R)
 		claim_4(I,Secret,yi);
 		claim_5(I,Secret,yr);
 		claim_6(I,Nisynch);
+		claim_7(I,Niagree);
 	}	
 	
 	role R
@@ -32,9 +33,10 @@ protocol ccitt509(I,R)
 		send_2(R,I, R,{nr, I, ni, xr, {yr}pk(I) }sk(R) );
 		read_3(I,R, I,{R,nr}sk(I) );
 
-		claim_7(R,Secret,yi);
+		claim_8(R,Secret,yi);
-		claim_8(R,Secret,yr);
+		claim_9(R,Secret,yr);
-		claim_9(R,Nisynch);
+		claim_10(R,Nisynch);
+		claim_11(R,Niagree);
 	}
 }
 

spdl/gong-nonce-b.spdl

@@ -26,6 +26,7 @@ protocol gongnonceb(I,R,S)
 		claim_6 (I, Secret, ki);
 		claim_7 (I, Secret, kr);
 		claim_8 (I, Nisynch);
+		claim_9 (I, Niagree);
 	}	
 	
 	role R
@@ -39,9 +40,10 @@ protocol gongnonceb(I,R,S)
 		send_3 (R,S, { R,S,R,kr,I }k(R,S), { R,I, ni }f(ki,kr), nr );
 		read_5 (I,R, { I,R,nr }f(ki,kr) );
 
-		claim_9 (R, Secret, ki);
+		claim_10 (R, Secret, ki);
-		claim_10 (R, Secret, kr);
+		claim_11 (R, Secret, kr);
-		claim_11 (R, Nisynch);
+		claim_12 (R, Nisynch);
+		claim_13 (R, Niagree);
 	}
 
 	role S

spdl/kaochow-palm.spdl

@@ -13,6 +13,10 @@ protocol kaochowPalm(I,R,S)
 		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
@@ -26,8 +30,9 @@ protocol kaochowPalm(I,R,S)
 		send_3 (R,I, T, {ni}kir, nr );
 		read_4 (I,R, {nr}kir );
 
-		claim_5 (R, Nisynch);
+		claim_8 (R, Nisynch);
-		claim_6 (R, Secret, kir);
+		claim_9 (R, Niagree);
+		claim_10 (R, Secret, kir);
 	}
 
 	role S

spdl/kaochow.spdl

@@ -13,6 +13,10 @@ protocol kaochow(I,R,S)
 		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 (R, Nisynch);
+		claim_6 (R, Niagree);
+		claim_7 (R, Secret, kir);
 	}	
 	
 	role R
@@ -26,8 +30,9 @@ protocol kaochow(I,R,S)
 		send_3 (R,I, T, {ni}kir, nr );
 		read_4 (I,R, {nr}kir );
 
-		claim_5 (R, Nisynch);
+		claim_8 (R, Nisynch);
-		claim_6 (R, Secret, kir);
+		claim_9 (R, Niagree);
+		claim_10 (R, Secret, kir);
 	}
 
 	role S

spdl/woolam-cmv.spdl

@@ -34,6 +34,8 @@ protocol woolamcmv(A,B,S)
 		send_7(A,B, { Nb }Kab );	
 
 		claim_8(A,Secret, Kab);
+		claim_9(A,Niagree);
+		claim_10(A,Nisynch);
 	}
 
 	role B
@@ -51,7 +53,9 @@ protocol woolamcmv(A,B,S)
    		send_6(B,A, t2, { Na,Nb }Kab );
 		read_7(A,B, { Nb }Kab );	
 
-		claim_9(B,Secret, Kab);
+		claim_11(B,Secret, Kab);
+		claim_12(B,Niagree);
+		claim_13(B,Nisynch);
 	}
 
 	role S

spdl/yahalom-lowe.spdl

@@ -24,7 +24,10 @@ protocol yahalomlowe(I,R,S)
 		send_1(I,R, I,ni);
 		read_3(S,I, {R,kir,ni,nr}k(I,S) );
 		send_5(I,R, {I,R,S,nr}kir );
+
 		claim_8(I, Secret,kir);
+		claim_9(I, Niagree);
+		claim_10(I, Nisynch);
 	}
 
 	role R
@@ -37,8 +40,9 @@ protocol yahalomlowe(I,R,S)
 		send_2(R,S, {I,ni,nr}k(R,S) );
 		read_4(S,R, {I,kir}k(R,S) );
 		read_5(I,R, {I,R,S,nr}kir );
-		claim_9(R, Secret,kir);
+		claim_11(R, Secret,kir);
-		claim_10(R, Nisynch);
+		claim_12(R, Nisynch);
+		claim_13(R, Niagree);
 	}
 
 	role S

spdl/yahalom-paulson.spdl

@@ -28,6 +28,7 @@ protocol yahalompaulson(I,R,S)
 
 		claim_8(I, Secret,kir);
 		claim_9(I, Nisynch);
+		claim_10(I, Niagree);
 	}
 
 	role R
@@ -40,8 +41,9 @@ protocol yahalompaulson(I,R,S)
 		send_2(R,S, R,nr,{I,ni}k(R,S) );
 		read_4(I,R, {I,R,kir,nr}k(R,S), {nr}kir );
 
-		claim_10(R, Secret,kir);
+		claim_11(R, Secret,kir);
-		claim_11(R, Nisynch);
+		claim_12(R, Nisynch);
+		claim_13(R, Niagree);
 	}
 
 	role S

test/multiprotocoltest.py

@@ -64,6 +64,9 @@ ProtocolToFileMap = {}		# maps protocol names to file names
 ProtocolToStatusMap = {}	# maps protocol names to status: 0 all false, 1 all correct, otherwise (2) mixed
 ProtocolToEffectsMap = {}	# maps protocols that help create multiple flaws, to the protocol names of the flaws they caused
 
+CommandPrefix = "not yet initialised."
+BoundsList = []			# bounds that have been displayed onscreen
+
 # Ugly hack. Works.
 safetxt = " " * 20
 
@@ -125,6 +128,33 @@ def ScytherEval (plist):
 	sys.stdout.flush()
 	sys.stderr.flush()
 
+	n = len(plist)
+	timer = 1
+	maxruns = 2
+	maxlength = 10
+	if options.bounds == 0:
+		timer = n**2
+		maxruns = 2*n
+		maxlength = 2 + maxruns * 3
+	elif options.bounds == 1:
+		timer = n**3
+		maxruns = 3*n
+		maxlength = 2 + maxruns * 4
+	else:
+		print "Don't know bounds method", options.bounds
+		sys.exit()
+
+	ScytherBounds = "--arachne --timer=%i --max-runs=%i --max-length=%i" % (timer, maxruns, maxlength)
+
+	# If these bounds had not been shown before, do so now
+	if not ScytherBounds in BoundsList:
+		BoundsList.append(ScytherBounds)
+		print "\nBounds for", n, "protocols:", ScytherBounds
+
+	# Combine it all
+	ScytherArgs = ScytherDefaults + " " + ScytherMethods + " " + ScytherBounds
+	CommandPrefix = "scyther " + ScytherArgs
+
 	# Combine protocol list to an input
 	input = ""
 	for fn in (IncludeProtocols.split(" ") + plist):
@@ -447,21 +477,7 @@ TupleWidth = str(options.tuplewidth)
 # Match
 ScytherMethods = "--match=" + str(options.match)
 
-# Method of bounding
+# Method of bounding will be determined in ScytherEval
-if options.bounds == 0:
-	ScytherBounds = "--arachne --timer=4 --max-runs=5 --max-length=20"
-elif options.bounds == 1:
-	ScytherBounds = "--arachne --timer=15 --max-runs=6 --max-length=30"
-else:
-	print "Don't know bounds method", options.bounds
-	sys.exit()
-
-
-# Combine it all
-ScytherArgs = ScytherDefaults + " " + ScytherMethods + " " + ScytherBounds
-CommandPrefix = "scyther " + ScytherArgs
-
-
 
 # Caching of single-protocol results for speed gain.
 #----------------------------------------------------------------------