scyther/gui/test-mpa.py

#!/usr/bin/python
"""
	Scyther : An automatic verifier for security protocols.
	Copyright (C) 2007 Cas Cremers

	This program is free software; you can redistribute it and/or
	modify it under the terms of the GNU General Public License
	as published by the Free Software Foundation; either version 2
	of the License, or (at your option) any later version.

	This program is distributed in the hope that it will be useful,
	but WITHOUT ANY WARRANTY; without even the implied warranty of
	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
	GNU General Public License for more details.

	You should have received a copy of the GNU General Public License
	along with this program; if not, write to the Free Software
	Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA  02110-1301, USA.
"""


"""

Example script to show how to perform large-scale tests using the
Scyther Python API (contained in the Scyther subdirectory)

In this example, multi-protocol attack analysis is performed on a small
test set.

Author: Cas Cremers

"""

from Scyther import Scyther
import time
try:
    from progressbar import *
    PROGRESSBAR = True
except ImportError:
    from progressbarDummy import *
    PROGRESSBAR = False
    print """
Missing the progressbar library.

It can be downloaded from:

http://code.google.com/p/python-progressbar/

"""

FOUND = []

def MyScyther(protocollist,filt=None,options=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()

    if options == None:
        # untyped matching
        s.options = "--match=2"
    else:
        s.options = options

    for protocol in protocollist:
        s.addFile(protocol)
    s.verifyOne(filt)
    return s
    

def getCorrectIsolatedClaims(protocolset,options=None):
    """
    Given a set of protocols, determine the correct claims when run in
    isolation.
    Returns a tuple, consisting of
    - a list of compiling protocols
    - a list of tuples (protocol,claimid) wich denote correct claims
    """
    correctclaims = []
    goodprotocols = []

    widgets = ['Scanning for claims that are correct in isolation: ', Percentage(), ' ',
               Bar(marker='#',left='[',right=']')
               ]
    pbar = ProgressBar(widgets=widgets, maxval=len(protocolset))
    pbar.start()
    count = 0
    for protocol in protocolset:
        # verify protocol in isolation
        s = MyScyther([protocol],options=options)
        # investigate the results
        goodprotocols.append(protocol)
        for claim in s.claims:
            if claim.okay:
                correctclaims.append((protocol,claim.id))
        count += 1
        pbar.update(count)
    pbar.finish()
    return (goodprotocols,correctclaims)


def verifyMPAlist(mpalist,claimid,options=None):
    """
    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
    print time.asctime(), mpalist, claimid, options # [DEBUG]
    s = MyScyther(mpalist,claimid,options)
    claim = s.getClaim(claimid)
    if claim:
        if not claim.okay:
            global FOUND

            # This is an MPA attack!
            print "I've found a multi-protocol attack on claim %s in the context %s." % (claimid,str(mpalist))
            FOUND.append((claimid,mpalist))

            return False
    else:
        return True


def constructMPAlist(protocolset,claimid,mpalist,length,start,callback,options=None):
    """
    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,options=options):
                    return False
        return True
    else:
        # list is long enough: callback
        return callback(mpalist,claimid,options)
    

def findMPA(protocolset,protocol,claimid,maxcount=3,options=None):
    """
    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)

    # the actual incremental search loop
    while count <= maxcount:
        constructMPAlist(protocolset,claimid,[protocol],count,0,verifyMPAlist,options)
        count += 1
    return None


def findAllMPA(protocolset,maxcount=3,options=None):
    """
    Given a set of protocols, find multi-protocol attacks
    """

    global FOUND

    FOUND = []

    # Find all correct claims in each protocol
    (protocolset,correct) = getCorrectIsolatedClaims(protocolset,options)
    print "Investigating %i correct claims." % (len(correct))
    # For all these claims...
    widgets = ['Scanning for MPA attacks: ', Percentage(), ' ',
               Bar(marker='#',left='[',right=']')
               ]
    pbar = ProgressBar(widgets=widgets, maxval=len(correct))
    pbar.start()
    count = 0
    for (protocol,claimid) in correct:
        # Try to find multi-protocol attacks
        findMPA(protocolset,protocol,claimid,maxcount,options)
        count += 1
        pbar.update(count)
    pbar.finish()

    """
    The below computation assumes protocol names are unique to files, but if
    they are not, some other errors should have been reported by the Scyther
    backend anyway (conflicting protocol definitions in MPA analysis).
    """
    mpaprots = []
    for (claimid,mpalist) in FOUND:
        pel = claimid.split(",")
        pn = pel[0]
        if pn not in mpaprots:
            mpaprots.append(pn)

    print "-" * 70
    print "Summary:"
    print
    print "We scanned %i protocols with options [%s]." % (len(protocolset),options)
    print "We found %i correct claims." % (len(correct))
    print "We found %i MPA attacks with a maximum of %i protocols." % (len(FOUND),maxcount)
    print "The attacks involve the claims of %i protocols." % (len(mpaprots))
    print "-" * 70


def bigTest():
    """
    Perform the tests as reported in the book.
    """
    import os

    testpath = "Protocols/MultiProtocolAttacks/"
    fl = os.listdir(testpath)
    nl = []
    for fn in fl:
        if fn.endswith(".spdl"):
            nl.append(fn)

    # Report list
    print "Performing multi-protocol analysis for the following protocols:", nl

    # Prepend again the path
    l = []
    for fn in nl:
        l.append(testpath+fn)

    ### Simplified test setup
    #defopts = "--max-runs=3 -T 360"
    #maxcount = 2

    ### Full test setup
    defopts = "--max-runs=4 -T 600"
    maxcount = 3

    # First typed
    print "Scanning without type flaws"
    findAllMPA(l,maxcount=maxcount,options = defopts + " --match=0")
    # Basic type flaws
    print "Scanning for basic type flaws"
    findAllMPA(l,maxcount=maxcount,options = defopts + " --match=1")
    # All type flaws
    print "Scanning for any type flaws"
    findAllMPA(l,maxcount=maxcount,options = defopts + " --match=2")



def simpleTest():
    """
    Simple test case with a few protocols
    """

    l = ['nsl3-broken.spdl','ns3.spdl','nsl3.spdl']
    print "Performing multi-protocol analysis for the following protocols:", l
    print
    findAllMPA(l)
    print
    print "Analysis complete."


def main():
    bigTest()
    #simpleTest()


if __name__ == '__main__':
    main()


# vim: set ts=4 sw=4 et list lcs=tab\:>-: