Merge branch 'MPA' of ssh://brutus.ethz.ch/~/src/scyther-MPA into MPA

gui/Scyther/Misc.py

@@ -64,7 +64,7 @@ def sorted(li):
     return result
 
 
-# ensurePath: does what os.makedirs should do.
+# ensurePath: wraps os.makedirs
 def ensurePath(pt):
     """
     Make sure the path exists: if not, create the directories one by one
@@ -75,27 +75,9 @@ def ensurePath(pt):
     It ensures this by doing the procedure for "dog", then "dog/cat", etc...
     """
 
-    ptn = os.path.normpath(pt)
-
-    # First we see what needs to exist overall
-    todo = [ptn]
-    tail = "x"
-    while len(tail) > 0:
-        (head,tail) = os.path.split(ptn)
-        if len(head) > 0:
-            todo.append(head)
-            ptn = head
-        else:
-            break
-
-    # Reverse list: path prefixes first
-    todo.reverse()
-
-    # Create bottom-up
-    for pt in todo:
     if not os.path.isdir(pt):
          # Note that os.path.exists(pt) may still hold. In this case the next command will cause an error.
-            os.mkdir(pt)
+         os.makedirs(pt)
 
 
 # path

gui/Scyther/Scyther.py

@@ -263,16 +263,17 @@ class Scyther(object):
 
         uid = m.hexdigest()
 
-        # Split the uid to make (256?) subdirectories
+        # Split the uid to make 256 subdirectories with 256 subdirectories...
         prefixlen = 2
         uid1 = uid[:prefixlen]
-        uid2 = uid[prefixlen:]
+        uid2 = uid[prefixlen:prefixlen+2]
+        uid3 = uid[prefixlen+2:]
 
         # Possibly we could also decide to store input and arguments in the cache to analyze things later
 
-        path = "Cache/%s/" % (uid1)
+        path = "Cache/%s/%s/" % (uid1,uid2)
-        name1 = "%s.out" % (uid2)
+        name1 = "%s.out" % (uid3)
-        name2 = "%s.err" % (uid2)
+        name2 = "%s.err" % (uid3)
 
         fname1 = path + name1
         fname2 = path + name2

gui/test-mpa.py

@@ -455,7 +455,9 @@ def findAllMPA(protocolset,options=[],mpaoptions=[]):
     """
 
     global FOUND
-    global OPTS
+    global OPTS, ARGS
+    global PROTNAMETOFILE
+    global ALLCLAIMS
 
     FOUND = []
 
@@ -490,6 +492,29 @@ def findAllMPA(protocolset,options=[],mpaoptions=[]):
                 print "  %s" % (p)
         print
 
+    # output of all claims (only if latex required)
+    
+    if OPTS.latex:
+        clset = set()
+        for claim in ALLCLAIMS:
+            prot = str(claim.protocol)
+            file = PROTNAMETOFILE[prot]
+            clid = claim.id
+            descr = claim.roledescribe()
+            
+            tup = (file,prot,clid,descr)
+            clset.add(tup)
+
+        fp = open("gen-%s-claims.txt" % (OPTS.latex),"w")
+
+        fp.write("%% OPTS: %s\n" % OPTS)
+        fp.write("%% ARGS: %s\n" % ARGS)
+
+        for (file,prot,clid,descr) in sorted(clset):
+            fp.write("%s; %s; %s; %s\n" % (file,prot,clid,descr))
+
+        fp.close()
+
     # Latex output of protocols with correct claims
     if OPTS.latex:
         pmapclaims = {}
@@ -499,6 +524,10 @@ def findAllMPA(protocolset,options=[],mpaoptions=[]):
             pmapclaims[protocol].add(claimid)
 
         fp = open("gen-%s-correctclaims.tex" % (OPTS.latex),"w")
+
+        fp.write("%% OPTS: %s\n" % OPTS)
+        fp.write("%% ARGS: %s\n" % ARGS)
+
         fp.write("\\begin{tabular}{ll}\n")
         fp.write("Protocol & Claims \\\\\n")
         for protocol in sorted(pmapclaims.keys()):
@@ -559,8 +588,12 @@ def findAllMPA(protocolset,options=[],mpaoptions=[]):
     TODO : Check whether current tests stop after finding *one* MPA attack or whether they find *all*.
 
     """
-    if OPTS.latex:
+    if OPTS.latex and not OPTS.pickle:
         fp = open("gen-%s-mpaattacks.tex" % (OPTS.latex),"w")
+
+        fp.write("%% OPTS: %s\n" % OPTS)
+        fp.write("%% ARGS: %s\n" % ARGS)
+
         fp.write("\\begin{tabular}{lll}\n")
         fp.write("Protocol & Claim & MPA attacks \\\\ \n")
 
@@ -606,6 +639,9 @@ def findAllMPA(protocolset,options=[],mpaoptions=[]):
     print "We scanned %i protocols with options [%s]." % (len(protocolset),options)
     print "We found %i correct claims." % (len(correct))
     print "We then scanned combinations of at most %i protocols with options [%s]." % (OPTS.maxprotocols,alloptions)
+    if OPTS.pickle:
+        print "However, just precomputing now, hence we are not drawing any conclusions."
+    else:
         print "We found %i MPA attacks." % (len(FOUND))
         print "The attacks involve the claims of %i protocols." % (len(mpaprots))
     print "-" * 70
@@ -754,6 +790,7 @@ def fullScan(l, options = [], mpaoptions = []):
     else:
         lres = exploreTree(0, choices, l, options = options, mpaoptions = mpaoptions)
         if len(lres) > 1:
+            if not OPTS.pickle:
                 showDiff(lres)
 
     allprots = set()
@@ -766,6 +803,7 @@ def fullScan(l, options = [], mpaoptions = []):
     for prot in INVOLVED:
         invprots.add(str(prot))
 
+    if not OPTS.pickle:
         print "The bottom line: we found %i protocols with multi-protocol attacks from a set of %i protocols." % (len(attprots),len(allprots))
         print