diff --git a/gui/Claim.py b/gui/Claim.py index 641e351..43c4411 100644 --- a/gui/Claim.py +++ b/gui/Claim.py @@ -6,7 +6,7 @@ import Term class Claim(object): def __init__(self): - self.id = None # a unique id string, like 'ns3,r,r3' + self.id = None # a unique id string, consisting of 'protocol,label' self.claimtype = None self.label = None self.shortlabel = None @@ -36,7 +36,7 @@ class Claim(object): self.shortlabel = label # determine id - self.id = "%s,%s,%s" % (self.protocol,self.role,self.shortlabel) + self.id = "%s,%s" % (self.protocol,self.shortlabel) # some additional properties if str(self.claimtype) == 'Reachable': diff --git a/gui/bin/scyther b/gui/bin/scyther index 971ea52..96dad86 100755 Binary files a/gui/bin/scyther and b/gui/bin/scyther differ diff --git a/gui/mpa.py b/gui/mpa.py index 48dc07c..6add6cd 100755 --- a/gui/mpa.py +++ b/gui/mpa.py @@ -8,9 +8,16 @@ Test script to execute multi-protocol attacks on some test set. import Scyther -def MyScyther(protocollist): +def MyScyther(protocollist,filter=None): + """ + Evaluate the composition of the protocols in protocollist. + If there is a filter, i.e. "ns3,I1" then only this specific claim + will be evaluated. + """ s = Scyther.Scyther() - s.options = "-m2" + s.options = "--match=2" + if filter: + s.options += " --filter=%s" % (filter) for protocol in protocollist: s.addFile(protocol) s.verify() @@ -20,48 +27,52 @@ def getCorrectIsolatedClaims(protocolset): """ Given a set of protocols, determine the correct claims when run in isolation. - Returns a list of tuples (protocol,claimid) + Returns a tuple, consisting of + - a list of compiling protocols + - a list of tuples (protocol,claimid) wich denote correct claims """ - correct = [] + correctclaims = [] + goodprotocols = [] 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 + if not s.errors: + goodprotocols.append(protocol) + for claim in s.claims: + if claim.okay: + correctclaims.append((protocol,claim.id)) + return (goodprotocols,correctclaims) def findMPA(protocolset,protocol,claimid,maxcount=3): """ The protocol claim is assumed to be correct. When does it break? """ count = 2 + if len(protocolset) < maxcount: + maxcount = len(protocolset) def verifyMPAlist(mpalist): # This should be a more restricted verification - print "verifying %s" % mpalist - s = MyScyther(mpalist) + s = MyScyther(mpalist,claimid) cl = s.getClaim(claimid) if cl: if not cl.okay: # This is an MPA attack! - print "Attack!" + print "I've found a multi-protocol attack on claim %s in the context %s." % (claimid,str(mpalist)) return mpalist - return None - def constructMPAlist(mpalist,callback): + def constructMPAlist(mpalist,start,callback): if len(mpalist) < count: - for p in protocolset: + for pn in range(start,len(protocolset)): + p = protocolset[pn] if p not in mpalist: - return constructMPAlist(mpalist + [p],callback) + constructMPAlist(mpalist + [p],pn+1,callback) else: - return callback(mpalist) + callback(mpalist) while count <= maxcount: - mpalist = constructMPAlist([protocol],verifyMPAlist) - if mpalist: - return mpalist + constructMPAlist([protocol],0,verifyMPAlist) count += 1 return None @@ -69,7 +80,7 @@ def findAllMPA(protocolset,maxcount=3): """ Given a set of protocols, find multi-protocol attacks """ - correct = getCorrectIsolatedClaims(protocolset) + (protocolset,correct) = getCorrectIsolatedClaims(protocolset) print correct for (protocol,claimid) in correct: mpalist = findMPA(protocolset,protocol,claimid,maxcount=3)