From a6933806f9732ac05427db08b96be17ba1a5dcb3 Mon Sep 17 00:00:00 2001
From: ccremers <ccremers@4f7d145f-a0d4-0310-ae10-d96cc04433c1>
Date: Mon, 7 Aug 2006 18:23:30 +0000
Subject: [PATCH] - MPA analysis script (but it will only work nicely once the
 claim   select functionality is in the Scyther backend)

---
 gui/Scyther.py | 16 ++++++++++
 gui/mpa.py     | 85 ++++++++++++++++++++++++++++++++++++++++++++++++++
 2 files changed, 101 insertions(+)
 create mode 100755 gui/mpa.py

diff --git a/gui/Scyther.py b/gui/Scyther.py
index 10946a8..58b4013 100755
--- a/gui/Scyther.py
+++ b/gui/Scyther.py
@@ -55,6 +55,15 @@ class Scyther(object):
             self.spdl += l
         fp.close()
 
+    def addFile(self,filename):
+        self.inputfile = None
+        if not self.spdl:
+            self.spdl = ""
+        fp = open(filename,"r")
+        for l in fp.readlines():
+            self.spdl += l
+        fp.close()
+
     def verify(self):
 
         # Run Scyther on temp file
@@ -98,6 +107,13 @@ class Scyther(object):
         self.run = True
         return self.claims
 
+    def getClaim(self,claimid):
+        if self.claims:
+            for cl in self.claims:
+                if cl.id == claimid:
+                    return cl
+        return None
+
     def __str__(self):
         if self.run:
             if self.errorcount > 0:
diff --git a/gui/mpa.py b/gui/mpa.py
new file mode 100755
index 0000000..48dc07c
--- /dev/null
+++ b/gui/mpa.py
@@ -0,0 +1,85 @@
+#!/usr/bin/python
+
+"""
+
+Test script to execute multi-protocol attacks on some test set.
+
+"""
+
+import Scyther
+
+def MyScyther(protocollist):
+    s = Scyther.Scyther()
+    s.options = "-m2"
+    for protocol in protocollist:
+        s.addFile(protocol)
+    s.verify()
+    return s
+    
+def getCorrectIsolatedClaims(protocolset):
+    """
+    Given a set of protocols, determine the correct claims when run in
+    isolation.
+    Returns a list of tuples (protocol,claimid)
+    """
+    correct = []
+    for protocol in protocolset:
+        # verify protocol in isolation
+        s = MyScyther([protocol])
+        # investigate the results
+        for claim in s.claims:
+            if claim.okay:
+                correct.append((protocol,claim.id))
+    return correct
+
+def findMPA(protocolset,protocol,claimid,maxcount=3):
+    """
+    The protocol claim is assumed to be correct. When does it break?
+    """
+    count = 2
+
+    def verifyMPAlist(mpalist):
+        # This should be a more restricted verification
+        print "verifying %s" % mpalist
+        s = MyScyther(mpalist)
+        cl = s.getClaim(claimid)
+        if cl:
+            if not cl.okay:
+                # This is an MPA attack!
+                print "Attack!"
+                return mpalist
+        return None
+
+    def constructMPAlist(mpalist,callback):
+        if len(mpalist) < count:
+            for p in protocolset:
+                if p not in mpalist:
+                    return constructMPAlist(mpalist + [p],callback)
+        else:
+            return callback(mpalist)
+
+    while count <= maxcount:
+        mpalist = constructMPAlist([protocol],verifyMPAlist)
+        if mpalist:
+            return mpalist
+        count += 1
+    return None
+
+def findAllMPA(protocolset,maxcount=3):
+    """
+    Given a set of protocols, find multi-protocol attacks
+    """
+    correct = getCorrectIsolatedClaims(protocolset)
+    print correct
+    for (protocol,claimid) in correct:
+        mpalist = findMPA(protocolset,protocol,claimid,maxcount=3)
+        if mpalist:
+            print "Darn, MPA on %s (%s) using %s" % (claimid,protocol,mpalist)
+
+if __name__ == '__main__':
+    list = ['me.spdl','ns3.spdl','nsl3.spdl']
+    findAllMPA(list)
+
+
+
+