diff --git a/spdl/andrew-ban.spdl b/spdl/andrew-ban.spdl index 0c1801d..3524f75 100644 --- a/spdl/andrew-ban.spdl +++ b/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)); } diff --git a/spdl/andrew-lowe-ban.spdl b/spdl/andrew-lowe-ban.spdl index 09abd85..8c292bd 100644 --- a/spdl/andrew-lowe-ban.spdl +++ b/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)); } diff --git a/spdl/bke.spdl b/spdl/bke.spdl index ead3ac2..73d9ac5 100644 --- a/spdl/bke.spdl +++ b/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, Nisynch ); + claim_7 (R, Secret, kir ); + claim_8 (R, Niagree ); + claim_9 (R, Nisynch ); } } diff --git a/spdl/bkepk.spdl b/spdl/bkepk.spdl index a42d57f..cc3f763 100644 --- a/spdl/bkepk.spdl +++ b/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); } } diff --git a/spdl/ccitt509-ban.spdl b/spdl/ccitt509-ban.spdl index 9f9ceda..c4c15d5 100644 --- a/spdl/ccitt509-ban.spdl +++ b/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,yr); - claim_9(R,Nisynch); + claim_8(R,Secret,yi); + claim_9(R,Secret,yr); + claim_10(R,Nisynch); + claim_11(R,Niagree); } } diff --git a/spdl/gong-nonce-b.spdl b/spdl/gong-nonce-b.spdl index fd1576b..e9bb6d2 100644 --- a/spdl/gong-nonce-b.spdl +++ b/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, kr); - claim_11 (R, Nisynch); + claim_10 (R, Secret, ki); + claim_11 (R, Secret, kr); + claim_12 (R, Nisynch); + claim_13 (R, Niagree); } role S diff --git a/spdl/kaochow-palm.spdl b/spdl/kaochow-palm.spdl index 62a0535..559a5e1 100644 --- a/spdl/kaochow-palm.spdl +++ b/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_6 (R, Secret, kir); + claim_8 (R, Nisynch); + claim_9 (R, Niagree); + claim_10 (R, Secret, kir); } role S diff --git a/spdl/kaochow.spdl b/spdl/kaochow.spdl index 8314d7f..8ae1c6e 100644 --- a/spdl/kaochow.spdl +++ b/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_6 (R, Secret, kir); + claim_8 (R, Nisynch); + claim_9 (R, Niagree); + claim_10 (R, Secret, kir); } role S diff --git a/spdl/woolam-cmv.spdl b/spdl/woolam-cmv.spdl index 4eda364..26d53ea 100644 --- a/spdl/woolam-cmv.spdl +++ b/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 diff --git a/spdl/yahalom-lowe.spdl b/spdl/yahalom-lowe.spdl index f49aaed..dc6251b 100644 --- a/spdl/yahalom-lowe.spdl +++ b/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_10(R, Nisynch); + claim_11(R, Secret,kir); + claim_12(R, Nisynch); + claim_13(R, Niagree); } role S diff --git a/spdl/yahalom-paulson.spdl b/spdl/yahalom-paulson.spdl index 866656d..282c02a 100644 --- a/spdl/yahalom-paulson.spdl +++ b/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, Nisynch); + claim_11(R, Secret,kir); + claim_12(R, Nisynch); + claim_13(R, Niagree); } role S diff --git a/test/multiprotocoltest.py b/test/multiprotocoltest.py index 514bbbe..0e1dfa9 100755 --- a/test/multiprotocoltest.py +++ b/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 -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 - - +# Method of bounding will be determined in ScytherEval # Caching of single-protocol results for speed gain. #----------------------------------------------------------------------