From 2b53516542ac96c6904785a4ccb9d9c76dd6eb79 Mon Sep 17 00:00:00 2001 From: ccremers Date: Thu, 18 Nov 2004 15:50:54 +0000 Subject: [PATCH] - Major improvements (o.a. in progress bars etc) --- spdl/carkey-ni2.spdl | 10 ++--- spdl/multiprotocoltest.py | 77 +++++++++++++++++++++++++++++++++------ 2 files changed, 71 insertions(+), 16 deletions(-) diff --git a/spdl/carkey-ni2.spdl b/spdl/carkey-ni2.spdl index 5c7802a..49bbe95 100644 --- a/spdl/carkey-ni2.spdl +++ b/spdl/carkey-ni2.spdl @@ -2,7 +2,7 @@ const pk: Function; secret sk: Function; inversekeys (pk,sk); -protocol carkeyni(I,R) +protocol carkeyni2(I,R) { role I { @@ -28,7 +28,7 @@ untrusted Eve; const nc: Nonce; compromised sk(Eve); -run carkeyni.I(Agent,Agent); -run carkeyni.R(Agent,Agent); -run carkeyni.I(Agent,Agent); -run carkeyni.R(Agent,Agent); +run carkeyni2.I(Agent,Agent); +run carkeyni2.R(Agent,Agent); +run carkeyni2.I(Agent,Agent); +run carkeyni2.R(Agent,Agent); diff --git a/spdl/multiprotocoltest.py b/spdl/multiprotocoltest.py index 41794ad..a2b9823 100755 --- a/spdl/multiprotocoltest.py +++ b/spdl/multiprotocoltest.py @@ -19,7 +19,7 @@ TupleProgram = "./tuples.py" ScytherProgram = "../src/scyther" ScytherDefaults = "--summary" -ScytherMethods = "-m1 -a" +ScytherMethods = "-m0 -a" ScytherBounds = "-r4 -l40" ReportInterval = 10 @@ -29,6 +29,13 @@ CommandPrefix = ScytherProgram + " " + ScytherArgs ProtocolClaims = {} +SkipList = [ + 'gong-nonce.spdl', + 'gong-nonce-b.spdl', + 'splice-as-hc.spdl', + 'kaochow-palm.spdl' + ] + # *********************** # LIBS # *********************** @@ -47,7 +54,7 @@ def ScytherEval (plist): results = {} for line in lines: data = line.split() - if data[0] == 'claim': + if len(data) > 6 and data[0] == 'claim': claim = " ".join(data[1:4]) tag = data[6] value = -1 @@ -70,6 +77,43 @@ def ScytherEval1 (protocol): +# Show progress of i (0..n) +# +LastProgress = {} +ProgressBarWidth = 50 + +def ShowProgress (i,n,txt): + factor = int((ProgressBarWidth * i) / n) + showme = 0 + if LastProgress.has_key(n): + if LastProgress[n]<>(factor,txt): + showme = 1 + else: + showme = 1 + if showme == 1: + bar = "\r[" + i = 0 + while i < ProgressBarWidth: + if i <= factor: + bar = bar + "*" + else: + bar = bar + "." + i = i+1 + bar = bar + "] " + txt + sys.stdout.write(bar) + sys.stdout.flush() + LastProgress[n] = (factor, txt) + +def ClearProgress (n,txt): + bar = " " * (1 + ProgressBarWidth + 2 + len(txt)) + sys.stdout.write("\r" + bar + "\r") + sys.stdout.flush() + + + + + + # *********************** # MAIN CODE @@ -97,8 +141,8 @@ while loop: if line != '': # not the end of the input cleanline = string.strip(line) - if cleanline != '': - # not a blank line + if cleanline != '' and cleanline not in SkipList: + # not a blank line, not forbidden Protocol.append(cleanline) ProtocolCount = ProtocolCount + 1 outp.write(line) @@ -106,7 +150,6 @@ while loop: # end of the input loop = 0 outp.close() -print "Evaluating tuples of", TupleWidth, "for", ProtocolCount, "protocols." # Caching of single-protocol results for speed gain. #---------------------------------------------------------------------- @@ -114,11 +157,15 @@ print "Evaluating tuples of", TupleWidth, "for", ProtocolCount, "protocols." # The script first computes the singular results for all the protocols # and stores this in an array, or something like that. +print "Evaluating tuples of", TupleWidth, "for", ProtocolCount, "protocols, using the command '" + CommandPrefix + "'" i = 0 +safetxt = ' ' while i < ProtocolCount: + ShowProgress (i, ProtocolCount,Protocol[i]+safetxt) ScytherEval1 ( Protocol[i] ) i = i + 1 -print "Evaluated single results." +ClearProgress(ProtocolCount, safetxt) +print "Evaluated single results, proceeding to test tuples." # Computation of combined list. #---------------------------------------------------------------------- @@ -129,12 +176,17 @@ print "Evaluated single results." lstatus=os.system(TupleProgram + ' ' + TupleWidth + ' <' + TempFileList + ' >' + TempFileTuples) +inp = open(TempFileTuples, 'r') +TupleCount = 0 +for x in inp: + TupleCount = TupleCount + 1 +inp.close() + # Testing of protocol tuples #---------------------------------------------------------------------- # # We take the list of tuples and test each combination. -print inp = open(TempFileTuples, 'r') processed = 0 newattacks = 0 @@ -143,6 +195,10 @@ for tline in inp: # Get the next tuple # protocols = tline.split() + ShowProgress (processed, TupleCount, " ".join(protocols) + safetxt) + # + # Process it + # results = ScytherEval ( protocols ) # # Now we have the results for this combination. @@ -154,15 +210,14 @@ for tline in inp: # an attack) if ProtocolClaims[claim] == 1: # Wooh! It was correct before + ClearProgress (TupleCount, safetxt) newattacks = newattacks + 1 - print claim + print "We found a new flaw:", claim # Next! processed = processed + 1 - if (processed % ReportInterval) == 0: - print "Checked", processed, "sofar." -print +ClearProgress (TupleCount, safetxt) print "Processed", processed,"tuple combinations in total." inp.close()