From f659cce88945c78f9727b715f409559c22f884cd Mon Sep 17 00:00:00 2001
From: ccremers <ccremers@4f7d145f-a0d4-0310-ae10-d96cc04433c1>
Date: Tue, 8 Aug 2006 13:18:09 +0000
Subject: [PATCH] - Improved multi-protocol attack script.

---
 gui/mpa.py | 67 ++++++++++++++++++++++++++++++++++++++----------------
 1 file changed, 47 insertions(+), 20 deletions(-)

diff --git a/gui/mpa.py b/gui/mpa.py
index 6add6cd..6ddecab 100755
--- a/gui/mpa.py
+++ b/gui/mpa.py
@@ -44,35 +44,62 @@ def getCorrectIsolatedClaims(protocolset):
                     correctclaims.append((protocol,claim.id))
     return (goodprotocols,correctclaims)
 
+def verifyMPAlist(mpalist,claimid):
+    """
+    Verify the existence of an attack in this context
+
+    If an attack is found, we return False, otherwise True. This is
+    needed for the iteration later.
+    """
+    # This should be a more restricted verification
+    s = MyScyther(mpalist,claimid)
+    claim = s.getClaim(claimid)
+    if claim:
+        if not claim.okay:
+            # This is an MPA attack!
+            print "I've found a multi-protocol attack on claim %s in the context %s." % (claimid,str(mpalist))
+            return False
+    else:
+        return True
+
+def constructMPAlist(protocolset,claimid,mpalist,length,start,callback):
+    """
+    Append a list of parallel protocols, without duplicates,
+    such that the added part is lexicographically ordered (from
+    index 'start' in the protocol list)
+    For each possible list, the function callback is called. If the
+    callback returns true, iteration proceeds (returning true in the
+    end), otherwise it aborts and returns false.
+    """
+    if len(mpalist) < length:
+        # list is not long enough yet
+        for pn in range(start,len(protocolset)):
+            p = protocolset[pn]
+            if p not in mpalist:
+                if not constructMPAlist(protocolset,claimid,mpalist + [p],length,pn+1,callback):
+                    return False
+        return True
+    else:
+        # list is long enough: callback
+        return callback(mpalist,claimid)
+    
 def findMPA(protocolset,protocol,claimid,maxcount=3):
     """
     The protocol claim is assumed to be correct. When does it break?
     """
+
+    # First we examine 2-protocol attacks, and then increase the
+    # number of parallel protocols if we don't find any attacks on the
+    # claim.
     count = 2
     if len(protocolset) < maxcount:
+        # we cannot have more protocols in parallel than there are
+        # protocols.
         maxcount = len(protocolset)
 
-    def verifyMPAlist(mpalist):
-        # This should be a more restricted verification
-        s = MyScyther(mpalist,claimid)
-        cl = s.getClaim(claimid)
-        if cl:
-            if not cl.okay:
-                # This is an MPA attack!
-                print "I've found a multi-protocol attack on claim %s in the context %s." % (claimid,str(mpalist))
-                return mpalist
-
-    def constructMPAlist(mpalist,start,callback):
-        if len(mpalist) < count:
-            for pn in range(start,len(protocolset)):
-                p = protocolset[pn]
-                if p not in mpalist:
-                    constructMPAlist(mpalist + [p],pn+1,callback)
-        else:
-            callback(mpalist)
-
+    # the actual incremental search loop
     while count <= maxcount:
-        constructMPAlist([protocol],0,verifyMPAlist)
+        constructMPAlist(protocolset,claimid,[protocol],count,0,verifyMPAlist)
         count += 1
     return None