- Beta version works like a charm.

This commit is contained in:
ccremers 2004-11-18 15:06:41 +00:00
parent 96ade10f29
commit a4f9b3c4de

View File

@ -22,6 +22,8 @@ ScytherDefaults = "--summary"
ScytherMethods = "-m1 -a" ScytherMethods = "-m1 -a"
ScytherBounds = "-r4 -l40" ScytherBounds = "-r4 -l40"
ReportInterval = 10
ScytherArgs = ScytherDefaults + " " + ScytherMethods + " " + ScytherBounds ScytherArgs = ScytherDefaults + " " + ScytherMethods + " " + ScytherBounds
CommandPrefix = ScytherProgram + " " + ScytherArgs CommandPrefix = ScytherProgram + " " + ScytherArgs
@ -63,7 +65,8 @@ def ScytherEval (plist):
# #
# The above, but do the preprocessing for a single protocol # The above, but do the preprocessing for a single protocol
def ScytherEval1 (protocol): def ScytherEval1 (protocol):
ProtocolClaims[protocol] = ScytherEval ([protocol]) results = ScytherEval ([protocol])
ProtocolClaims.update (results)
@ -103,6 +106,7 @@ while loop:
# end of the input # end of the input
loop = 0 loop = 0
outp.close() outp.close()
print "Evaluating tuples of", TupleWidth, "for", ProtocolCount, "protocols."
# Caching of single-protocol results for speed gain. # Caching of single-protocol results for speed gain.
#---------------------------------------------------------------------- #----------------------------------------------------------------------
@ -114,8 +118,7 @@ i = 0
while i < ProtocolCount: while i < ProtocolCount:
ScytherEval1 ( Protocol[i] ) ScytherEval1 ( Protocol[i] )
i = i + 1 i = i + 1
print "Evaluated single results."
print ProtocolClaims
# Computation of combined list. # Computation of combined list.
#---------------------------------------------------------------------- #----------------------------------------------------------------------
@ -131,4 +134,35 @@ lstatus=os.system(TupleProgram + ' ' + TupleWidth + ' <' + TempFileList + ' >' +
# #
# We take the list of tuples and test each combination. # We take the list of tuples and test each combination.
print
inp = open(TempFileTuples, 'r')
processed = 0
newattacks = 0
for tline in inp:
#
# Get the next tuple
#
protocols = tline.split()
results = ScytherEval ( protocols )
#
# Now we have the results for this combination.
# Check whether any of these claims is 'newly false'
#
for claim,value in results.items():
if value == 0:
# Apparently this claim is false now (there is
# an attack)
if ProtocolClaims[claim] == 1:
# Wooh! It was correct before
newattacks = newattacks + 1
print claim
# Next!
processed = processed + 1
if (processed % ReportInterval) == 0:
print "Checked", processed, "sofar."
print
print "Processed", processed,"tuple combinations in total."
inp.close()