- Added gui.

2006-08-02 12:59:57 +00:00 · 2006-08-02 12:59:57 +00:00 · e1ddf0668b
commit e1ddf0668b
parent 460c087cf2
26 changed files with 2701 additions and 0 deletions
--- a/gui/Attack.py
+++ b/gui/Attack.py
@ -0,0 +1,52 @@
+#
+# Attack
+#
+
+import Trace
+import Term
+#import Classification
+from Misc import *
+
+class Attack(object):
+    def __init__(self):
+        self.broken = []
+        self.match = None
+        self.initialKnowledge = []
+        self.inverseKeys = []
+        self.protocol = None
+        self.semiTrace = Trace.SemiTrace()
+        self.variables = []
+        self.protocoldescr = {}
+        self.id = None
+        self.knowledge = None 
+        self.untrusted = []
+        self.typeflaws = False
+        self.commandline = ''
+        self.scytherDot = None
+        self.claim = None       # refers to parent claim
+    
+    def getInvolvedAgents(self):
+        result = []
+        for run in self.semiTrace.runs:
+            for agent in run.roleAgents.values():
+                result.append(agent)
+        return uniq(result)
+
+    def buildKnowledge(self):
+        if not self.knowledge:
+            self.knowledge = Term.Knowledge(self)
+            self.knowledge.buildKnowledge()
+        
+    def getPrecedingLabelSet(self,event):
+        return self.protocoldescr[str(event.label[0])].getPrecedingLabelSet(event.label)
+        
+    def getPrecedingRoleSet(self,event):
+        return self.protocoldescr[str(event.label[0])].getPrecedingRoleSet(event.label)
+        
+    #def classify(self):
+    #    classification = Classification.Classification(self)
+    #    classification.classifyClaims()
+    #    classification.classifyInitiations()
+    #    classification.classifyComplexity()
+    #    classification.classifyTypeflaws()
+    #    return classification
--- a/gui/Attackimage.py
+++ b/gui/Attackimage.py
@ -0,0 +1,41 @@
+#!/usr/bin/python
+
+#---------------------------------------------------------------------------
+
+""" Import externals """
+import os
+
+#---------------------------------------------------------------------------
+
+""" Import scyther-gui components """
+import Tempfile
+
+#---------------------------------------------------------------------------
+
+class AttackImage:
+    def __init__(self,dotdata):
+        self.dotdata = dotdata
+        self.png = ""
+
+        self.MakeImage()    
+
+    def MakeImage(self):
+        """ Sets png """
+
+        (fd,fpname) = Tempfile.tempcleaned(".dot")
+        fp = os.fdopen(fd, "w")
+        fp.write(self.dotdata)
+        fp.close()
+
+        (fd2,fpname2) = Tempfile.tempcleaned(".png")
+        os.system("dot %s -Tpng >%s" % (fpname, fpname2))
+        self.png = fpname2
+
+        Tempfile.tempcleanearly((fd,fpname))
+
+    def GetImage(self):
+
+        return self.png
+
+#---------------------------------------------------------------------------
+
--- a/gui/Attackwindow.py
+++ b/gui/Attackwindow.py
@ -0,0 +1,169 @@
+#!/usr/bin/python
+
+#---------------------------------------------------------------------------
+
+""" Import externals """
+import wx
+import time
+
+#---------------------------------------------------------------------------
+
+""" Import scyther-gui components """
+import Icon
+
+#---------------------------------------------------------------------------
+
+class AttackDisplay(wx.ScrolledWindow):
+    def __init__(self, daddy, parent, claim,attackid):
+
+        self.win = daddy
+
+        wx.ScrolledWindow.__init__(self,parent,id=-1)
+        # Wait for the attack to be computed
+        while attackid >= len(claim.attacks):
+            time.sleep(1)
+
+        self.Bind(wx.EVT_SIZE, self.OnSize)
+        self.Image = wx.StaticBitmap(self, -1, wx.EmptyBitmap(1,1))
+        self.box = wx.BoxSizer(wx.VERTICAL)
+        self.box.Add(self.Image,1,wx.ALIGN_CENTER)
+        self.hbox = wx.BoxSizer(wx.HORIZONTAL)
+        self.hbox.Add(self.box,1,wx.ALIGN_CENTER)
+        self.SetSizer(self.hbox)
+
+        filename = claim.attacks[attackid].GetImage()
+        self.original = wx.Image(filename,wx.BITMAP_TYPE_PNG)
+
+
+        self.update()
+
+        # TODO self.Bind(wxSizeEvent
+
+    def OnSize(self,event):
+        self.update()
+        event.Skip()
+
+    def update(self):
+
+        self.SetScrollbars(0,0,0,0,0,0)
+
+        bmp = self.original
+        if self.win.fit:
+            W = bmp.GetWidth()
+            H = bmp.GetHeight()
+            (sw,sh) = self.win.GetClientSizeTuple()
+
+            if W > sw:
+                # correct width
+                factor = float(sw) / W
+                W = sw
+                H = H * factor
+            if H > sh:
+                # correct height
+                factor = float(sh) / H
+                H = sh
+                W = W * factor
+
+
+            bmp = self.original.Scale(W,H)
+
+        self.Image.SetBitmap(wx.BitmapFromImage(bmp))
+        #self.box.SetItemMinSize(self.Image.GetContainingSizer())
+        self.box.Layout()
+
+        # wx.StaticBitmap(self, -1, bmp, (0, 0), (bmp.GetWidth(), bmp.GetHeight()))
+        step = 20
+        xn = int(bmp.GetWidth() / step) + 1
+        yn = int(bmp.GetHeight() / step) + 1
+        self.SetScrollbars(step,step,xn,yn,0,0)
+
+        self.Refresh()
+
+
+class AttackWindow(wx.Frame):
+    def __init__(self,cl):
+        super(AttackWindow, self).__init__(None, size=(400,800))
+        self.claim = cl
+        self.fit = False
+        self.CreateInteriorWindowComponents()
+        self.CreateExteriorWindowComponents()
+
+        Icon.ScytherIcon(self)
+        self.SetTitle()
+
+    def SetTitle(self):
+
+        if self.claim.attackcount == 1:
+            tstr = "Attack"
+        else:
+            tstr = "Attacks"
+
+        tstr += " for claim %s" % str(self.claim)
+        super(AttackWindow, self).SetTitle(tstr)
+
+
+    def CreateInteriorWindowComponents(self):
+        ''' Create "interior" window components. In this case it is the
+        attack picture. '''
+
+        self.displays=[]
+        if self.claim.attackcount <= 1:
+            # Just a single window
+            self.tabs = None
+            self.displays.append(AttackDisplay(self,self,self.claim,0))
+        else:
+            # Multiple tabs
+            self.tabs = wx.Notebook(self,-1)
+            for i in range(0,self.claim.attackcount):
+                disp =  AttackDisplay(self,self.tabs,self.claim,i)
+                classname = "Class %i" % ((i+1))
+                self.tabs.AddPage(disp, classname)
+                self.displays.append(disp)
+
+        self.Show(1)
+
+
+    def CreateExteriorWindowComponents(self):
+        ''' Create "exterior" window components, such as menu and status
+        bars '''
+        self.CreateStatusBar()
+        self.SetupToolBar()
+
+    def SetupToolBar(self):
+
+        tb = self.CreateToolBar(wx.TB_HORIZONTAL
+                | wx.NO_BORDER
+                | wx.TB_FLAT
+                | wx.TB_TEXT
+                )
+
+        # Add fit button
+        bmp = wx.ArtProvider_GetBitmap(wx.ART_MISSING_IMAGE,wx.ART_TOOLBAR,(20,20))
+        if not bmp.Ok():
+            bmp = wx.EmptyBitmap(20,20)
+        tb.AddCheckTool(wx.ID_ZOOM_FIT, bmp, bmp, 'Toggle zoom', 'Toggle zoom level')
+        self.Bind(wx.EVT_TOOL, self.OnFit, id=wx.ID_ZOOM_FIT)
+
+        # And shortcut
+        aTable = wx.AcceleratorTable([
+                                      (wx.ACCEL_NORMAL, ord('Z'), wx.ID_ZOOM_FIT)
+                                      ])
+        self.SetAcceleratorTable(aTable)
+
+    def update(self):
+        for t in self.displays:
+            t.update()
+
+    def OnFit(self,event):
+
+        if self.fit:
+            self.fit = False
+        else:
+            self.fit = True
+        self.update()
+
+    def OnRealSize(self):
+
+        self.fit = False
+        self.update()
+
--- a/gui/Claim.py
+++ b/gui/Claim.py
@ -0,0 +1,66 @@
+#
+# Claim
+#
+
+import Term
+
+class Claim(object):
+    def __init__(self):
+        self.claimtype = None
+        self.label = None
+        self.protocol = None
+        self.role = None
+        self.parameter = None
+        self.failed = 0
+        self.count = 0
+        self.states = 0
+        self.complete = False
+        self.timebound = False
+        self.attacks = []
+        self.state = False      # if true, it is a state, not an attack
+
+        # derived info
+        self.foundstates = False
+        self.foundproof = False
+
+    def analyze(self):
+        if str(self.claimtype) == 'Reachable':
+            self.state = True
+        if self.failed > 0:
+            self.foundstates = True
+        if self.complete:
+            self.foundproof = True
+
+    def stateName(self,count=1):
+        if self.state:
+            s = "state"
+        else:
+            s = "attack"
+        if count != 1:
+            s += "s"
+        return s
+
+    def __str__(self):
+        s = "claim "
+        s+= " " + str(self.protocol)
+        s+= " " + str(self.role)
+
+        # We need the rightmost thingy here
+        label = self.label
+        while isinstance(label,Term.TermTuple):
+            label = label[1]
+
+        s+= " " + str(label)
+        s+= " " + str(self.claimtype)
+        if self.parameter:
+            s+= " " + str(self.parameter)
+
+        # determine status
+        s+= " : %i " % (self.failed)
+        s+= self.stateName(self.failed)
+        if self.complete:
+            s+= " (complete)"
+
+        return s
+
+
--- a/gui/Icon.py
+++ b/gui/Icon.py
@ -0,0 +1,23 @@
+#!/usr/bin/python
+
+#---------------------------------------------------------------------------
+
+""" Import externals """
+import wx
+import os.path
+
+#---------------------------------------------------------------------------
+
+""" Import scyther-gui components """
+import Misc
+
+#---------------------------------------------------------------------------
+
+def ScytherIcon(window):
+        """ Set a nice Scyther icon """
+        iconfile = Misc.mypath("scyther-gui-32.ico")
+        if os.path.isfile(iconfile):
+            icon = wx.Icon(iconfile,wx.BITMAP_TYPE_ICO)
+            window.SetIcon(icon)
+
+
--- a/gui/Mainwindow.py
+++ b/gui/Mainwindow.py
@ -0,0 +1,399 @@
+#!/usr/bin/python
+
+#---------------------------------------------------------------------------
+
+""" Import externals """
+import wx
+import os.path
+import sys
+import wx.lib.mixins.listctrl as listmix
+
+#---------------------------------------------------------------------------
+
+""" Import scyther-gui components """
+import Preference
+import Attackwindow
+import Scytherthread
+import Icon
+
+#---------------------------------------------------------------------------
+
+""" Some constants """
+ID_VERIFY = 100
+ID_AUTOVERIFY = 101
+ID_STATESPACE = 102
+ID_CHECK = 103
+
+#---------------------------------------------------------------------------
+
+class MainWindow(wx.Frame):
+
+    def __init__(self, filename=''):
+        super(MainWindow, self).__init__(None, size=(600,800))
+        self.dirname = '.'
+
+        if filename != '' and os.path.isfile(filename):
+            self.filename = filename
+            self.load = True
+        else:
+            self.filename = 'noname.spdl'
+            self.load = False
+
+        Icon.ScytherIcon(self)
+
+        self.CreateInteriorWindowComponents()
+        self.CreateExteriorWindowComponents()
+
+        aTable = wx.AcceleratorTable([
+                                      #(wx.ACCEL_ALT,  ord('X'), exitID),
+                                      (wx.ACCEL_CTRL, ord('W'), wx.ID_EXIT),
+                                      (wx.ACCEL_NORMAL, wx.WXK_F1,
+                                          ID_VERIFY),
+                                      (wx.ACCEL_NORMAL, wx.WXK_F2,
+                                          ID_STATESPACE),
+                                      (wx.ACCEL_NORMAL, wx.WXK_F5, 
+                                          ID_CHECK),
+                                      (wx.ACCEL_NORMAL, wx.WXK_F6,
+                                          ID_AUTOVERIFY),
+                                      ])
+        self.SetAcceleratorTable(aTable)
+
+        self.claimlist = []
+        self.pnglist = []
+
+        #self.SetTitle(self.title) 
+
+    def CreateInteriorWindowComponents(self):
+        ''' Create "interior" window components. In this case it is just a
+            simple multiline text control. '''
+
+        self.splitter = wx.SplitterWindow(self,-1)
+        self.splitter.daddy = self
+
+        # Top: input
+        self.top = wx.Notebook(self.splitter,-1)
+        self.control = wx.TextCtrl(self.top, style=wx.TE_MULTILINE)
+        if self.load:
+            textfile = open(os.path.join(self.dirname, self.filename), 'r')
+            self.control.SetValue(textfile.read())
+            os.chdir(self.dirname)
+            textfile.close()
+        self.top.AddPage(self.control,"Protocol")
+        self.settings = SettingsWindow(self.top,self)
+        self.top.AddPage(self.settings,"Settings")
+
+        # Bottom: output
+        self.bottom = wx.Notebook(self.splitter,-1)
+        self.report = SummaryWindow(self.bottom,self)
+        self.bottom.AddPage(self.report,"Claim summary")
+        self.errors = ErrorWindow(self.bottom,self)
+        self.bottom.AddPage(self.errors,"Detailed output")
+
+        #self.report.SetValue("Welcome.")
+
+        # Combine
+        self.splitter.SetMinimumPaneSize(20)
+        self.splitter.SplitHorizontally(self.top, self.bottom)
+        self.splitter.SetSashPosition(510)
+        self.Show(1)
+
+
+    def CreateExteriorWindowComponents(self):
+        ''' Create "exterior" window components, such as menu and status
+            bar. '''
+        self.CreateMenus()
+        self.CreateStatusBar()
+        self.SetupToolBar()
+        self.SetTitle()
+
+    def SetupToolBar(self):
+
+        tb = self.CreateToolBar(wx.TB_HORIZONTAL
+                | wx.NO_BORDER
+                | wx.TB_FLAT
+                | wx.TB_TEXT
+                )
+
+        bmp = wx.ArtProvider_GetBitmap(wx.ART_EXECUTABLE_FILE,wx.ART_TOOLBAR,(20,20))
+        if not bmp.Ok():
+            bmp = wx.EmptyBitmap(20,20)
+        tb.AddSimpleTool(ID_VERIFY, bmp,"Verify","Verify claims")
+        self.Bind(wx.EVT_TOOL, self.OnVerify, id=ID_VERIFY)
+        tb.AddSimpleTool(ID_STATESPACE, bmp,"Statespace","Generate statespace for all roles")
+        self.Bind(wx.EVT_TOOL, self.OnStatespace, id=ID_STATESPACE)
+        tb.AddSeparator()
+
+        tb.AddSimpleTool(ID_CHECK, bmp,"Check","Check protocol")
+        self.Bind(wx.EVT_TOOL, self.OnCheck, id=ID_CHECK)
+        tb.AddSimpleTool(ID_AUTOVERIFY, bmp,"Default claims","Verify default claims")
+        self.Bind(wx.EVT_TOOL, self.OnAutoVerify, id=ID_AUTOVERIFY)
+
+    def CreateMenu(self, bar, name, list):
+
+        fileMenu = wx.Menu()
+        for id, label, helpText, handler in list:
+            if id == None:
+                fileMenu.AppendSeparator()
+            else:
+                item = fileMenu.Append(id, label, helpText)
+                self.Bind(wx.EVT_MENU, handler, item)
+        bar.Append(fileMenu, name) # Add the fileMenu to the MenuBar
+
+
+    def CreateMenus(self):
+        menuBar = wx.MenuBar()
+        self.CreateMenu(menuBar, '&File', [
+             (wx.ID_OPEN, '&Open', 'Open a new file', self.OnOpen),
+             (wx.ID_SAVE, '&Save', 'Save the current file', self.OnSave),
+             (wx.ID_SAVEAS, 'Save &As', 'Save the file under a different name',
+                self.OnSaveAs),
+             (None, None, None, None),
+             (wx.ID_EXIT, 'E&xit\tCTRL-W', 'Terminate the program',
+                 self.OnExit)])
+        self.CreateMenu(menuBar, '&Verify',
+             [(ID_VERIFY, '&Verify protocol\tF1','Verify the protocol in the buffer using Scyther',
+                 self.OnVerify) ,
+             (ID_STATESPACE, 'Generate &statespace\tF2','TODO' ,
+                 self.OnAutoVerify) ,
+             (None, None, None, None),
+             (ID_CHECK, '&Check protocol\tF5','TODO',
+                 self.OnStatespace) ,
+             (ID_AUTOVERIFY, 'Verify &automatic claims\tF6','TODO',
+                 self.OnCheck)
+             ])
+        self.CreateMenu(menuBar, '&Help',
+            [(wx.ID_ABOUT, '&About', 'Information about this program',
+                self.OnAbout) ])
+        self.SetMenuBar(menuBar)  # Add the menuBar to the Frame
+
+
+    def SetTitle(self):
+        # MainWindow.SetTitle overrides wx.Frame.SetTitle, so we have to
+        # call it using super:
+        super(MainWindow, self).SetTitle('Scyther-gui: %s'%self.filename)
+
+
+    # Helper methods:
+
+    def defaultFileDialogOptions(self):
+        ''' Return a dictionary with file dialog options that can be
+            used in both the save file dialog as well as in the open
+            file dialog. '''
+        return dict(message='Choose a file', defaultDir=self.dirname,
+                    wildcard='*.spdl')
+
+    def askUserForFilename(self, **dialogOptions):
+        dialog = wx.FileDialog(self, **dialogOptions)
+        if dialog.ShowModal() == wx.ID_OK:
+            userProvidedFilename = True
+            self.filename = dialog.GetFilename()
+            self.dirname = dialog.GetDirectory()
+            self.SetTitle() # Update the window title with the new filename
+        else:
+            userProvidedFilename = False
+        dialog.Destroy()
+        return userProvidedFilename
+
+    # Event handlers:
+
+    def OnAbout(self, event):
+        msg = "Scyther GUI\n\nScyther and Scyther GUI\ndeveloped by Cas Cremers"
+        dialog = wx.MessageDialog(self,msg, 'About scyther-gui', wx.OK)
+        dialog.ShowModal()
+        dialog.Destroy()
+
+    def OnExit(self, event):
+        self.Close()  # Close the main window.
+
+    def OnSave(self, event):
+        textfile = open(os.path.join(self.dirname, self.filename), 'w')
+        textfile.write(self.control.GetValue())
+        textfile.close()
+
+    def OnOpen(self, event):
+        if self.askUserForFilename(style=wx.OPEN,
+                                   **self.defaultFileDialogOptions()):
+            textfile = open(os.path.join(self.dirname, self.filename), 'r')
+            self.control.SetValue(textfile.read())
+            textfile.close()
+
+    def OnSaveAs(self, event):
+        if self.askUserForFilename(defaultFile=self.filename, style=wx.SAVE,
+                                   **self.defaultFileDialogOptions()):
+            self.OnSave(event)
+            os.chdir(self.dirname)
+
+    def RunScyther(self, mode):
+        Scytherthread.RunScyther(self,mode)
+
+    def OnVerify(self, event):
+        self.RunScyther("verify")
+
+    def OnAutoVerify(self, event):
+        self.RunScyther("autoverify")
+
+    def OnStatespace(self, event):
+        self.RunScyther("statespace")
+
+    def OnCheck(self, event):
+        self.RunScyther("check")
+
+#---------------------------------------------------------------------------
+
+class SettingsWindow(wx.Panel):
+
+    def __init__(self,parent,daddy):
+        wx.Panel.__init__(self,parent,-1)
+
+        self.win = daddy
+
+
+        # Bound on the number of runs
+        self.maxruns = int(Preference.get('maxruns','5'))
+        r1 = wx.StaticText(self,-1,"Maximum number of runs (0 disables bound)")
+        l1 = wx.SpinCtrl(self, -1, "",size=(150,-1))
+        l1.SetRange(0,100)
+        l1.SetValue(self.maxruns)
+        self.Bind(wx.EVT_SPINCTRL,self.EvtRuns,l1)
+
+        # Matchin options
+        self.match = int(Preference.get('match','0'))
+        claimoptions = ['typed matching','find basic type flaws','find all type flaws']
+        r2 = wx.StaticText(self,-1,"Matching type")
+        l2 = wx.RadioBox(self, -1, "",
+                wx.DefaultPosition,wx.DefaultSize,claimoptions,1,wx.RA_SPECIFY_COLS)
+        l2.SetSelection(self.match)
+        self.Bind(wx.EVT_RADIOBOX,self.EvtMatch,l2)
+
+        ### MISC expert stuff
+
+        self.misc = Preference.get('scytheroptions','')
+        r10 = wx.StaticText(self,-1,"Additional parameters for the Scyther tool")
+        l10 = wx.TextCtrl(self,-1,self.misc,size=(150,-1))
+        self.Bind(wx.EVT_TEXT,self.EvtMisc,l10)
+
+        # Combine
+        space = 10
+        sizer = wx.FlexGridSizer(cols=3, hgap=space,vgap=space)
+        sizer.AddMany([ l1,r1, (0,0),
+                        l2,r2, (0,0),
+                        l10,r10, (0,0),
+                        ])
+        self.SetSizer(sizer)
+        self.SetAutoLayout(True)
+
+    def EvtMatch(self,evt):
+        self.match = evt.GetInt()
+
+    def EvtRuns(self,evt):
+        self.maxruns = evt.GetInt()
+
+    def EvtMisc(self,evt):
+        self.misc = evt.GetString()
+
+    def ScytherArguments(self):
+        """ Note: constructed strings should have a space at the end to
+            correctly separate the options.
+        """
+
+        tstr = ""
+
+        # Number of runs
+        tstr += "--max-runs=%s " % (str(self.maxruns))
+        # Matching type
+        tstr += "--match=%s " % (str(self.match))
+
+        # Verification type
+        if self.mode == "check":
+            tstr += "--check "
+        if self.mode == "autoverify":
+            tstr += "--auto-claims "
+        elif self.mode == "statespace":
+            tstr += "--state-space "
+
+        # Anything else?
+        if self.misc != "":
+            tstr += " " + self.misc + " "
+
+        return tstr
+
+#---------------------------------------------------------------------------
+
+class SummaryWindow(wx.ListCtrl, listmix.ListCtrlAutoWidthMixin):
+
+    def __init__(self,parent,daddy):
+        wx.ListCtrl.__init__(self,parent,-1, style=wx.LC_REPORT
+                | wx.BORDER_NONE
+                | wx.LC_SORT_ASCENDING
+                | wx.LC_SINGLE_SEL
+                )
+        listmix.ListCtrlAutoWidthMixin.__init__(self)
+
+        self.win = daddy
+        self.currentItem = -1
+
+        self.Bind(wx.EVT_LIST_ITEM_SELECTED, self.OnItemSelected)
+
+        self.InsertColumn(0, "Protocol")
+        self.InsertColumn(1, "Role")
+        self.InsertColumn(2, "Claim")
+        self.InsertColumn(3, "Label")
+        self.InsertColumn(4, "Parameters")
+        self.InsertColumn(5, "Status")
+        self.InsertColumn(6, "Attacks")
+        self.InsertColumn(7, "Comments")
+
+    def update(self):
+        self.DeleteAllItems()
+        self.claimlist = self.win.claimlist
+        for key in range(0,len(self.claimlist)):
+            cl = self.claimlist[key]
+            index = self.InsertStringItem(sys.maxint,cl.protocol)
+            self.SetStringItem(index,1,cl.role)
+            self.SetStringItem(index,2,cl.claim)
+            self.SetStringItem(index,3,cl.label)
+            self.SetStringItem(index,4,cl.param)
+            self.SetStringItem(index,5,cl.status)
+            self.SetStringItem(index,6,str(cl.attackcount))
+            self.SetStringItem(index,7,cl.comments)
+            self.SetItemData(index,key)
+
+            if cl.status == "Fail":
+                # Failed :(
+                item = self.GetItem(key)
+                item.SetTextColour(wx.RED)
+                self.SetItem(item)
+            else:
+                # Okay! But with bound?
+                if cl.comments.find("bounds") == -1:
+                    # No bounds, great :)
+                    item = self.GetItem(key)
+                    item.SetTextColour(wx.GREEN)
+                    self.SetItem(item)
+        #for i in range(0,7):
+        #    self.SetColumnWidth(i,wx.LIST_AUTOSIZE)
+
+    def OnItemSelected(self, event):
+        self.currentItem = event.m_itemIndex
+        cl = self.claimlist[self.currentItem]
+        if cl.attackcount > 0:
+            display = Attackwindow.AttackWindow(cl)
+            display.Show(1)
+        self.Refresh()
+        event.Skip()
+
+#---------------------------------------------------------------------------
+
+class ErrorWindow(wx.TextCtrl):
+
+    def __init__(self,parent,daddy):
+        wx.TextCtrl.__init__(self,parent,-1, style=wx.TE_MULTILINE)
+        self.win = daddy
+    
+    def update(self,summary):
+        self.SetValue(summary)
+
+#---------------------------------------------------------------------------
+
+    
+
--- a/gui/Misc.py
+++ b/gui/Misc.py
@ -0,0 +1,45 @@
+#
+# Misc.py
+# Various helper functions
+
+#---------------------------------------------------------------------------
+
+""" Import externals """
+import os.path
+
+#---------------------------------------------------------------------------
+
+def confirm(question):
+    answer = ''
+    while answer not in ('y','n'):
+        print question,
+        answer = raw_input().lower()
+    return answer == 'y'
+
+def exists(func,list):
+    return len(filter(func,list)) > 0    
+
+def forall(func,list):
+    return len(filter(func,list)) == len(list)    
+
+def uniq(li):
+    result = []
+    for elem in li:
+        if (not elem in result):
+            result.append(elem)
+    return result
+
+# Return a sorted copy of a list
+def sorted(li):
+    result = li[:]
+    result.sort()
+    return result
+
+
+# path
+def mypath(file):
+    """ Construct a file path relative to the scyther-gui main directory
+    """
+    basedir = os.path.dirname(__file__)
+    return os.path.join(basedir,file)
+
--- a/gui/Preference.py
+++ b/gui/Preference.py
@ -0,0 +1,132 @@
+#!/usr/bin/python
+
+"""
+    Preferences window and logic for saving and loading such things.
+    Thus, some default things can be set here.
+
+    init    loads stuff
+    save    save the settings after some changes
+    set(k,v)
+    get(k)
+
+    Currently used:
+
+    match
+    maxruns
+    scyther
+    scytheroptions
+"""
+
+#---------------------------------------------------------------------------
+
+""" Import externals """
+
+import wx
+import os.path
+from time import localtime,strftime
+
+#---------------------------------------------------------------------------
+
+""" Import scyther-gui components """
+
+#---------------------------------------------------------------------------
+
+""" Globals """
+
+""" Locations of preferences. The last one is supposedly writable. """
+prefname = "scythergui-config"
+preflocs = ['/usr/local/lib/scyther','~/.scyther']
+
+#---------------------------------------------------------------------------
+
+class Preferences(dict):
+
+    def parse(self,line):
+        line = line.strip()
+
+        """ Skip comments """
+        if not line.startswith("#"):
+            split = line.find("=")
+            if split != -1:
+                key = line[:split].strip()
+                data = line[(split+1):]
+                self[key] = data.decode("string_escape")
+                print "Read %s=%s" % (key,self[key])
+
+    def load(self,file=""):
+        if file == None:
+            self["test1"] = "Dit is met een ' en een \", en dan\nde eerste dinges"
+            self["test2"] = "En dit de tweede"
+        elif file == "":
+            """
+            Test default locations
+            """
+            for f in preflocs:
+                self.load(os.path.join(os.path.expanduser(f),prefname))
+
+        else:
+            """
+            Read this file
+            """
+            if os.path.isfile(file):
+                fp = open(file,"r")
+                for l in fp.readlines():
+                    self.parse(l)
+                fp.close()
+
+    def show(self):
+        print "Preferences:"
+        for k in self.keys():
+            print "%s=%s" % (k, self[k])
+
+    def save(self):
+
+        print "Saving preferences"
+        prefpath = os.path.expanduser(preflocs[-1])
+        if not os.access(prefpath,os.W_OK):
+            os.makedirs(prefpath)
+        savename = os.path.join(prefpath,prefname)
+        fp = open(savename,"w")
+
+        fp.write("# Scyther-gui configuration file.\n#\n")
+        date = strftime("%c",localtime())
+        fp.write("# Last written on %s\n" % (date))
+        fp.write("# Do not edit - any changes will be overwritten by Scyther-gui\n\n")
+
+        l = list(self.keys())
+        l.sort()
+        for k in l:
+            fp.write("%s=%s\n" % (k, self[k].encode("string_escape")))
+
+        fp.close()
+
+def init():
+    """
+        Load the preferences from a file, if possible
+    """
+    global prefs
+
+    prefs = Preferences()
+    prefs.load("")
+
+
+def get(key,alt=None):
+    global prefs
+
+    if prefs.has_key(key):
+        return prefs[key]
+    else:
+        return alt
+
+def set(key,value):
+    global prefs
+
+    prefs[key]=value
+    return
+
+def save():
+    global prefs
+
+    prefs.save()
+
+
--- a/gui/Scyther.py
+++ b/gui/Scyther.py
@ -0,0 +1,112 @@
+#!/usr/bin/python
+#
+# Scyther interface
+#
+
+#---------------------------------------------------------------------------
+
+""" Import externals """
+import os
+import sys
+import StringIO
+import tempfile
+
+#---------------------------------------------------------------------------
+
+""" Import scyther components """
+import XMLReader
+from Misc import *
+
+#---------------------------------------------------------------------------
+
+class Scyther(object):
+    def __init__ ( self):
+        self.program = "scyther"
+        self.options = ""
+        self.spdl = None
+        self.claims = None
+
+    def setInput(self,spdl):
+        self.spdl = spdl
+
+    def setFile(self,filename):
+        self.spdl = ""
+        fp = open(filename,"r")
+        for l in fp.readlines():
+            self.spdl += l
+        fp.close()
+
+    def verify(self):
+
+        if self.spdl:
+            # Write spdl to temp file
+            fp = tempfile.NamedTemporaryFile()
+            fp.write(self.spdl)
+            fp.flush()
+
+            # Run Scyther on temp file
+            self.cmd = "%s %s --dot-output --xml-output --plain '%s'" % (self.program,self.options,fp.name)
+
+            # If we are on windows, we don't get stderr. Maybe we need a
+            # switch to enforce this.
+            if sys.platform.startswith('linux'):
+                cmdline = "%s 2>/dev/null" % (self.cmd)
+            else:
+                # Non-linux does not generate stderr anyway
+                cmdline = "%s" % (self.cmd)
+
+            result = os.popen(cmdline)
+
+            xmlinput = result.read()
+
+
+            fp.close()
+
+            xmlfile = StringIO.StringIO(xmlinput)
+            reader = XMLReader.XMLReader()
+            self.claims = reader.readXML(xmlfile)
+
+
+            # Cleanup
+            del(xmlinput)
+            del(xmlfile)
+            return self.claims
+
+        else:
+            # No input yet!
+            return ""
+
+    def __str__(self):
+        if self.claims:
+            s = ""
+            for cl in self.claims:
+                s += str(cl) + "\n"
+            return s
+        else:
+            return "Scyther has not been run yet."
+
+
+def basictest():
+    # Some basic testing
+    if sys.platform.startswith('win'):
+        print "Dir test"
+        p = os.popen("dir")
+        print p.read()
+        print p.close()
+        confirm("See the dir?")
+   
+    # Scyther
+    x = Scyther()
+
+    if sys.platform.startswith('win'):
+        x.program = "c:\\Scyther.exe"
+        if not os.path.isfile(x.program):
+            print "I can't find the Scyther executable %s" % (x.program)
+
+    x.setFile("ns3.spdl")
+    x.verify()
+
+if __name__ == '__main__':
+    basictest()
+
+
--- a/gui/Scytherthread.py
+++ b/gui/Scytherthread.py
@ -0,0 +1,97 @@
+#!/usr/bin/python
+
+#---------------------------------------------------------------------------
+
+""" Import externals """
+import wx
+import wx.lib.newevent
+import os
+import sys
+import re
+import threading
+import StringIO
+
+#---------------------------------------------------------------------------
+
+""" Import scyther components """
+import XMLReader
+
+""" Import scyther-gui components """
+import Tempfile
+import Claim
+import Preference
+import Scyther
+
+#---------------------------------------------------------------------------
+
+""" Global declaration """
+(UpdateAttackEvent, EVT_UPDATE_ATTACK) = wx.lib.newevent.NewEvent()
+busy = threading.Semaphore()
+
+
+#---------------------------------------------------------------------------
+
+def ScytherPath():
+    """ Retrieve Scyther path, and maybe test whether is is valid? """
+    program = Preference.get('scyther','scyther')
+    program = "\\\\Roivas\\public\\scyther-gui\\Scyther.exe"
+    return program
+
+class ScytherThread(threading.Thread):
+    # Override Thread's __init__ method to accept the parameters needed:
+    def __init__ ( self, win, spdl, details ):
+
+        self.win = win
+        self.spdl = spdl
+        self.details = details
+
+        self.claims = []
+
+        threading.Thread.__init__ ( self )
+
+    def run(self):
+
+        global busy
+
+        evt = UpdateAttackEvent(status="Running Scyther...")
+        wx.PostEvent(self.win, evt)
+
+        self.claimResults()
+
+        evt = UpdateAttackEvent(status="Done.")
+        wx.PostEvent(self.win, evt)
+
+        #self.win.SetCursor(wx.StockCursor(wx.CURSOR_ARROW))
+        busy.release()
+
+    def claimResults(self):
+        """ Convert spdl to result (using Scyther) """
+
+        scyther = Scyther.Scyther()
+        if sys.platform.startswith('win'):
+            scyther.program = "c:\\Scyther.exe"
+            if not os.path.isfile(scyther.program):
+                print "I can't find the Scyther executable %s" % (scyther.program)
+
+        scyther.setInput(self.spdl)
+        self.claims = scyther.verify()
+        self.summary = str(scyther)
+
+        self.win.errors.update(self.summary)
+
+
+def RunScyther(win,mode):
+
+    global busy
+
+    if (busy.acquire(False)):
+
+        # start the thread
+        win.SetCursor(wx.StockCursor(wx.CURSOR_WAIT))
+
+        win.settings.mode = mode
+        t =  ScytherThread(win,win.control.GetValue(),"")
+        t.start()
+        win.threads = [ t ]
+
+
--- a/gui/Tempfile.py
+++ b/gui/Tempfile.py
@ -0,0 +1,41 @@
+#!/usr/bin/python
+
+#---------------------------------------------------------------------------
+
+""" Import externals """
+import os
+import tempfile
+import atexit
+
+#---------------------------------------------------------------------------
+
+""" Local thing (can be done in numerous nicer ways) """
+tempfiles = []
+
+#---------------------------------------------------------------------------
+
+def tempremove(tuple):
+    (fd,fpname) = tuple
+    #os.close(fd)
+    os.remove(fpname)
+
+def cleanupshop():
+    global tempfiles
+
+    for tuple in tempfiles:
+        tempremove(tuple)
+
+def tempcleaned(post=""):
+    global tempfiles
+
+    tuple = tempfile.mkstemp(post,"scyther_")
+    tempfiles.append(tuple)
+    return tuple
+
+def tempcleanearly(tuple):
+    global tempfiles
+
+    tempfiles.remove(tuple)
+    tempremove(tuple)
+
+atexit.register(cleanupshop)
--- a/gui/Term.py
+++ b/gui/Term.py
@ -0,0 +1,204 @@
+#
+# Term
+#
+import Trace
+from Misc import *
+
+class InvalidTerm(TypeError):
+    "Exception used to indicate that a given term is invalid"
+    
+
+class Knowledge(object):
+    def __init__(self,attack):
+        self.attack = attack
+        self.knowledge = []
+
+    def getInverse(self,term):
+        for pair in self.attack.inverseKeys:
+            if term == pair[0]:
+                return pair[1]
+            if term == pair[1]:
+                return pair[0]
+
+    # Get the inverse key
+    def getInverseKey(self,term):
+        # First try to see if the entire term has an inverse
+        result = self.getInverse(term)
+        if result != None:
+            return result
+        
+        # If it is an apply term, try to see if the function has an inverse
+        if isinstance(term,TermApply):
+            result = self.getInverse(term.function)
+            if result != None:
+                return TermApply(result,term.argument)
+            
+        # No inverse found, so term is its own inverse
+        return term
+        
+    # Add a term to the knowledge
+    def add(self,term):
+        if term == None:
+            return
+        added = False
+        for x in term.deriveTerms(self):
+            if not x in self.knowledge:
+                added = True
+                self.knowledge.append(x)
+        
+        # Something new was added, maybe this can help us to decrypt a term
+        # that we could not decrypt before
+        if added:
+            for x in self.knowledge:
+                if isinstance(x,TermEncrypt):
+                    self.add(x)
+            
+    def canDerive(self,term):
+        # We can derive free variables, because we can even choose them
+        if isinstance(term,TermVariable) and term.isFree():
+            return True
+        # We can derive a term if it is in the knowledge
+        # or all terms required to construct it are in the knowledge
+        if exists(lambda x: x == term,self.knowledge):
+            return True
+        constructors = term.constructorTerms()
+   
+        if len(constructors) == 1 and constructors[0] == term:
+            # This is a single term, there is no need to look at constructor
+            # terms as we have already looked at the complete term
+            return False
+            
+        return forall(lambda x: self.canDerive(x),constructors)
+            
+        
+    # Knowledge is the initial knowledge and all messages in sends
+    def buildKnowledge(self):
+        self.knowledge = self.attack.initialKnowledge[:]
+        for run in self.attack.semiTrace.runs:
+            # Intruder actions do not add knowledge processing them
+            # is a waste of time
+            if run.intruder:
+                continue
+            for event in run:
+                if isinstance(event,Trace.EventSend):
+                    self.add(event.message)
+                    self.add(event.fr)
+                    self.add(event.to)
+
+class Term(object):
+    def __init__(self):
+        self.types = None
+        
+    def __str__(self):
+        raise InvalidTerm
+    
+    def constructorTerms(self):
+        raise InvalidTerm
+
+    def deriveTerms(self,knowledge):
+        raise InvalidTerm
+    
+    # Two terms are equal when their string rep is equal
+    def __cmp__(self,other):
+        return cmp(str(self),str(other))
+                
+    
+class TermConstant(Term):   
+    def __init__(self, constant):
+        Term.__init__(self)
+        self.value = str(constant)
+    
+    def deriveTerms(self,knowledge):
+        return [self]
+        
+    def constructorTerms(self):
+        return [self]
+    
+    def __str__(self):
+        return self.value
+
+class TermEncrypt(Term):
+    def __init__(self, value, key):
+        Term.__init__(self)
+        self.value = value
+        self.key = key
+
+    def deriveTerms(self,knowledge):
+        # In order to unpack an encrypted term we have to have the inverse key
+        inverse = knowledge.getInverseKey(self.key)
+        if knowledge.canDerive(inverse):
+            return [self] + [self.value] + self.value.deriveTerms(knowledge)
+        else:
+            return [self]
+        
+    def constructorTerms(self):
+        return [self.value,self.key]
+        
+    def __str__(self):
+        return "{%s}%s" % (self.value, self.key)
+
+class TermApply(Term):
+    def __init__(self, function, argument):
+        Term.__init__(self)
+        self.function = function
+        self.argument = argument
+
+    def constructorTerms(self):
+        return [self.function,self.argument]
+        
+    def deriveTerms(self,knowledge):
+        return [self]
+
+    def __str__(self):
+        return "%s(%s)" % (self.function, self.argument)
+
+class TermVariable(Term):
+    def __init__(self, name, value):
+        Term.__init__(self)
+        self.name = name
+        self.value = value
+
+    def isFree(self):
+        return self.value == None
+    
+    def constructorTerms(self):
+        if self.value != None:
+            return [self.value]
+        else:
+            return [self.name]
+    
+    def deriveTerms(self,knowledge):
+        if self.value != None:
+            return [self,self.value] + self.value.deriveTerms(knowledge)
+        else:
+            return [self,self.name]
+    
+    def __str__(self):
+        if (self.value != None):
+            return str(self.value)
+        else:
+            return str(self.name)
+
+class TermTuple(Term):
+    def __init__(self, op1, op2):
+        Term.__init__(self)
+        self.op1 = op1
+        self.op2 = op2
+
+    def __str__(self):
+        return "%s,%s" % (self.op1,self.op2)
+    
+    def constructorTerms(self):
+        return [self.op1,self.op2]
+        
+    def deriveTerms(self,knowledge):
+        return [self,self.op1,self.op2]+self.op1.deriveTerms(knowledge)+self.op2.deriveTerms(knowledge)
+        
+    def __getitem__(self,index):
+        if index == 0:
+            return self.op1
+        elif index == 1:
+            return self.op2
+        else:
+            return self.op2.__getitem__(index-1)
+
--- a/gui/Trace.py
+++ b/gui/Trace.py
@ -0,0 +1,309 @@
+#
+# Trace
+#
+from Misc import *
+
+class InvalidAction(TypeError):
+    "Exception used to indicate that a given action is invalid"
+    
+class InvalidEvent(TypeError):
+    "Exception used to indicate that a given event is invalid"
+
+class SemiTrace(object):
+    def __init__(self):
+        self.runs = []
+    
+    def totalCount(self):
+        count = 0
+        for run in self.runs:
+            count += len(run.eventList)
+        return count
+            
+    def sortActions(self,actionlist):
+        newlist = actionlist[:]
+        newlist.sort(lambda x,y: self.getOrder(x,y))
+        return newlist
+
+    def getEnabled(self,previous):
+        enabled = []
+        for run in self.runs:
+            for event in run:
+                if event in previous or event in enabled:
+                    continue
+                prec = self.getPrecedingEvents(event,previous)
+                if len(prec) == 0:
+                    enabled.append(event)
+        return enabled
+          
+    # Returns run,index tuples for all connections
+    def getConnections(self,event,removeIntruder=False):
+        if not removeIntruder:
+            return event.follows
+        result = []
+        if event.run.intruder:
+            for before in event.getBefore():
+                result.extend(self.getConnections(before,removeIntruder))
+
+        for x in event.follows:
+            fol = self.getEvent(x)
+            # If this is an intruder action descend into it
+            if fol.run.intruder:
+                result.extend(self.getConnections(fol,removeIntruder))
+            else:
+                result.append(x)
+        return uniq(result)
+        
+    # Return the minimum set of preceding events for a given event
+    # that is the events before this event in the same run and all
+    # actions required by the partional ordering
+    # If previous is non empty remove all events already in previous
+    def getPrecedingEvents(self,event,previous=[]):
+        # If it is cached return cached version
+        if event.preceding != None:
+            return filter(lambda x: x not in previous,event.preceding)
+        preceding = []
+        for prec in event.getBefore():
+            preceding.append(prec)
+            preceding.extend(self.getPrecedingEvents(prec))
+        for x in event.follows:
+            fol = self.getEvent(x)
+            preceding.append(fol)
+            preceding.extend(self.getPrecedingEvents(fol))
+        preceding = uniq(preceding)
+        event.preceding = preceding
+        preceding = filter(lambda x: x not in previous,preceding)
+        return preceding
+    
+    # Returns -1 if the first event has to be before the second one
+    #         +1 if the second event has to be before the first one
+    #          0 if there is no order defined on the two events 
+    def getOrder(self,event1,event2):
+        if (event1 in self.getPrecedingEvents(event2)):
+            return -1
+        if (event2 in self.getPrecedingEvents(event1)):
+            return 1
+        return 0
+    
+    # Get event by run id and index
+    def getEvent(self,idx):
+        (rid,index) = idx
+        for run in self.runs:
+            if run.id != rid:
+                continue
+            for event in run:
+                if event.index == index:
+                    return event
+        raise InvalidEvent
+    
+    # Get all claim events in the trace
+    def getClaims(self):
+        claims = []
+        for run in self.runs:
+            for event in run:
+                if isinstance(event,EventClaim):
+                    claims.append(event)
+        return claims
+
+    # Returns a list of all initiation events in the semitrace
+    def getInitiations(self):
+        initiations = []
+        for run in self.runs:
+            # Initiations are runs of honest agents
+            if (run.intruder):
+                continue
+            # Which contain no reads before the first send
+            for action in run:
+                if (isinstance(action,EventRead)):
+                    break
+                elif (isinstance(action,EventSend)):
+                    initiations.append(action)
+                    break
+        return initiations
+
+    # Get all runs performed by a specific agent
+    def getAgentRuns(self,agent):
+        result = []
+        for run in self.runs:
+            if run.getAgent() == agent:
+                result.append(run)
+        return result
+
+    # Return a list of all runs that are parallel with this run
+    def getParallelRuns(self,run):
+        parallel = []
+        first = run.getFirstAction()
+        # Process all events that are before the end of the run
+        for event in self.getPrecedingEvents(run.getLastAction()):
+            # Only count those we haven't found yet
+            if event.run in parallel or event.run == run:
+                continue
+            # If the event is also after the beginning of the run it is
+            # parallel
+            if self.getOrder(event,first) == 1:
+                parallel.append(event.run)
+        return parallel
+
+    def getRun(self,runid):
+        for run in self.runs:
+            if run.id == runid:
+                return run
+        return None
+            
+class ProtocolDescription(object):
+    def __init__(self,protocol):
+        self.protocol = protocol
+        self.roledescr = {}
+
+    # Find event by label
+    def findEvent(self,eventlabel,eventType=None):
+        for (role,descr) in self.roledescr.items():
+            for event in descr:
+                if event.label == eventlabel:
+                    if eventType == None or isinstance(event,eventType):
+                        return event
+
+    # Return all events that should have occured before the given event
+    # if the protocol is executed exactly as specified 
+    # (i.e. all previous events in the same run and the preceding events
+    # of the matching sends of all reads)
+    def getPrecedingEvents(self,eventlabel,eventType=None):
+        event = self.findEvent(eventlabel,eventType)
+        if event.preceding != None:
+            return event.preceding
+        preceding = event.getBefore()+[event]
+        for prev in preceding:
+            # For this event and all events that are before it in the run
+            # description see if it is a read and if it is also add the
+            # precedinglabelset of the matching send
+            if (isinstance(prev,EventRead)):
+                match = self.findEvent(prev.label,EventSend)
+                if match:
+                    preceding.extend(self.getPrecedingEvents(match.label,EventSend))
+        preceding = uniq(preceding)
+        event.preceding = preceding
+        return preceding
+    
+    # Calculate the preceding labelset that is all read events
+    # that are in the precedingEvents of a certain event
+    def getPrecedingLabelSet(self,eventlabel):
+        events = self.getPrecedingEvents(eventlabel)
+        events = filter(lambda x: isinstance(x,EventRead),events)
+        return [x.label for x in events]
+
+    # Calculate the roles in preceding labelset that is all roles that
+    # that are in the precedingEvents of a certain event
+    def getPrecedingRoleSet(self,eventlabel):
+        events = self.getPrecedingEvents(eventlabel)
+        roles = uniq([x.run.role for x in events])
+        return roles
+    
+
+    def __str__(self):
+        s = ''
+        for x in self.roledescr.values():
+            for e in x:
+                s += str(e) + "\n"
+        return s
+
+class Run(object):
+    def __init__(self):
+        self.id = None
+        self.protocol = None
+        self.role = None
+        self.roleAgents = {}
+        self.eventList = []
+        self.intruder = False
+        self.attack = None
+
+    def __iter__(self):
+        return iter(self.eventList)
+
+    def getAgent(self):
+        if self.intruder:
+            return None
+        return self.roleAgents[self.role]
+
+    def getFirstAction(self):
+        return self.eventList[0]
+
+    def getLastAction(self):
+        return self.eventList[-1]
+
+class Event(object):
+    def __init__(self,index,label,follows):
+        self.index = index
+        self.label = label
+        self.follows = follows
+        self.run = None
+        self.preceding = None
+        self.rank = None
+    
+    def shortLabel(self):
+        try:
+            return self.label[len(self.label)-1]
+        except:
+            return str(self.label)
+
+    def getBefore(self):
+        result = []
+        for event in self.run:
+            if (event == self):
+                return result
+            result.append(event)
+        # This should never happen
+        assert(False)
+
+class EventSend(Event):
+    def __init__(self,index,label,follows,fr,to,message):
+        Event.__init__(self,index,label,follows)
+        self.fr = fr
+        self.to = to
+        self.message = message
+
+    def __str__(self):
+        if self.run.intruder:
+            return "SEND(%s)" % self.message
+        else:
+            return "SEND_%s(%s,%s)" % (self.shortLabel(),self.to,self.message)
+
+class EventRead(Event):
+    def __init__(self,index,label,follows,fr,to,message):
+        Event.__init__(self,index,label,follows)
+        self.fr = fr
+        self.to = to
+        self.message = message
+    
+    def __str__(self):
+        if self.run.intruder:
+            return "READ(%s)" % self.message
+        else:
+            return "READ_%s(%s,%s)" % (self.shortLabel(),self.fr, self.message)
+
+class EventClaim(Event):
+    def __init__(self,index,label,follows,role,type,argument):
+        Event.__init__(self,index,label,follows)
+        self.role = role
+        self.type = type
+        self.argument = argument
+        self.broken = None
+    
+    # A Claim should be ignored if there is an untrusted agent in the role
+    # agents
+    def ignore(self):
+        for untrusted in self.run.attack.untrusted:
+            if untrusted in self.run.roleAgents.values():
+                return True
+        return False
+        
+    # Return (protocol,role)
+    def protocolRole(self):
+        return "(%s,%s)" % (self.run.protocol,self.run.role)
+    
+    def argstr(self):
+        if self.argument == None:
+            return '*'
+        else:
+            return str(self.argument)
+            
+    def __str__(self):
+        return "CLAIM_%s(%s, %s)" % (self.shortLabel(),self.type,self.argstr())
--- a/gui/XMLReader.py
+++ b/gui/XMLReader.py
@ -0,0 +1,301 @@
+#
+# XMLReader
+#
+# Note:
+# This requires python elementtree to work
+# See: http://effbot.org/zone/element-index.htm
+#
+# On Fedora Core you can install this by installing the python-elementtree rpm
+# Things will be a lot faster and consume less memory if you install the
+# cElementTree module
+#
+
+# Check for cElementTree presence. Otherwise use ElementTree.
+useiter = True
+try:
+    import cElementTree
+except ImportError:
+    useiter = False 
+    from elementtree import ElementTree
+
+## Simply pick cElementTree
+#import cElementTree
+## Simply pick ElementTree
+#useiter = False 
+#from elementtree import ElementTree
+
+import Term
+import Attack
+import Trace
+import Claim
+import sys
+        
+class XMLReader(object):
+    
+    def __init__ (self):
+        self.varlist = []
+        pass
+
+    def readXML(self, input):
+        # Use iter parse when possble so we can clear the attack after reading 
+        # it in order to preserve memory (this requires cElementTree)
+
+        attackbuffer = []
+        claims = []
+        
+        if useiter:
+            parser = cElementTree.iterparse(input)
+        else:
+            parser = ElementTree.parse(input).findall('*')
+
+        for elem in parser:
+            # The iter parser receives the input in tuples (event and element)
+            # we only need the event
+            if useiter:
+                elem = elem[1]
+
+            if elem.tag == 'state':
+                attack = self.readAttack(elem)
+                attackbuffer.append(attack)
+                if useiter:
+                    elem.clear()
+
+            if elem.tag == 'claimstatus':
+                claim = self.readClaim(elem)
+                claim.attacks = attackbuffer
+                claims.append(claim)
+
+                # link to parent
+                for attack in claim.attacks:
+                    attack.claim = claim
+
+                attackbuffer = []
+                if useiter:
+                    elem.clear()
+
+        return claims
+
+    # Read a term from XML
+    def readTerm(self,xml):
+        # If xml is None the term should also be none
+        if xml == None:
+            return None
+        # If this is a term variable read it directly
+        if (xml.tag in ('tuple','const','apply','encrypt','var')):
+            return self.readSubTerm(xml)
+        # Otherwise read from it's first child
+        children = xml.getchildren()
+        assert(len(children) == 1)
+        return self.readSubTerm(children[0])
+
+    def readSubTerm(self, tag):
+        if tag.tag == 'tuple':
+            return Term.TermTuple(self.readTerm(tag.find('op1')),self.readTerm(tag.find('op2')))
+        elif tag.tag == 'const':
+            return Term.TermConstant(tag.text)
+        elif tag.tag == 'apply':
+            return Term.TermApply(self.readTerm(tag.find('function')),self.readTerm(tag.find('arg')))
+        elif tag.tag == 'encrypt':
+            return Term.TermEncrypt(self.readTerm(tag.find('op')),self.readTerm(tag.find('key')))
+        elif tag.tag == 'var':
+            name = Term.TermConstant(tag.get('name'))
+            # Instantiate this variable if possible (note this list is empty while reading
+            # the variables section of the XML file)
+            for inst in self.varlist:
+                    if inst.name == name:
+                        return inst
+            # If it is not instantiated in varlist, just return a variable with this name and no
+            # value
+            return Term.TermVariable(name,None)
+        else:
+            raise Term.InvalidTerm, "Invalid term type in XML: %s" % tag.tag
+    
+    def readEvent(self,xml):
+        label = self.readTerm(xml.find('label'))
+        follows = xml.findall('follows')
+        followlist = []
+        for follow in follows: 
+            follow = follow.find('after')
+            if follow == None:
+                # Ignore follow definitions that do not contain after
+                continue
+            follow = (int(follow.get('run')),int(follow.get('index')))
+            followlist.append(follow)
+            
+        (etype,index) = (xml.get('type'),int(xml.get('index')))
+        if etype in ('send','read'):
+            fr = self.readTerm(xml.find('from'))
+            to = self.readTerm(xml.find('to'))
+            message = self.readTerm(xml.find('message'))
+            if (etype == 'send'):
+                return Trace.EventSend(index,label,followlist,fr,to,message)
+            else:
+                return Trace.EventRead(index,label,followlist,fr,to,message)
+        elif xml.get('type') == 'claim':
+            role = self.readTerm(xml.find('role'))
+            etype = self.readTerm(xml.find('type'))
+            argument = self.readTerm(xml.find('argument'))
+            # Freshness claims are implemented as Empty claims with
+            # (Fresh,Value) as arguments
+            try:
+                if etype == 'Empty' and argument[0] == 'Fresh':
+                    etype = Term.TermConstant('Fresh')
+                    argument = argument[1]
+                elif etype == 'Empty' and argument[0] == 'Compromised':
+                    etype = Term.TermConstant('Compromised')
+                    argument = argument[1]
+            except:
+                pass
+            return Trace.EventClaim(index,label,followlist,role,etype,argument)
+        else:
+            raise Trace.InvalidAction, "Invalid action in XML: %s" % (xml.get('type'))
+
+    def readRun(self,xml):
+        assert(xml.tag == 'run')
+        run = Trace.Run()
+        run.id = int(xml.find('runid').text)
+        # TODO why is protocol name a term??
+        run.protocol = str(self.readTerm(xml.find('protocol')))
+        run.intruder = xml.find('protocol').get('intruder') == 'true'
+        run.role = xml.find('rolename').text
+        for role in xml.find('roleagents'):
+            name = role.find('rolename').text
+            agent = self.readTerm(role.find('agent'))
+            run.roleAgents[name] = agent
+        for eventxml in xml.find('eventlist'):
+            action = self.readEvent(eventxml)
+            action.run = run
+            run.eventList.append(action)
+        return run
+            
+    # Read protocol description for a certain role
+    def readRoleDescr(self,xml):
+        assert(xml.tag == 'role')
+        run = Trace.Run()
+        # We will need the last label later on to see if a 
+        # run is complete
+        run.lastLabel = None
+        run.role = xml.find('rolename').text
+        for eventxml in xml.find('eventlist'):
+            action = self.readEvent(eventxml)
+            action.run = run
+            run.eventList.append(action)
+            run.lastLabel = action.label
+        return run
+    
+    def readTypeList(self,xml):
+        result = []
+        vartypes = xml.find('type').find('termlist')
+        for vartype in vartypes:
+            # We will assume that types are simple strings
+            result.append(str(self.readTerm(vartype)))
+        return result
+        
+    def readClaim(self, xml):
+        claim = Claim.Claim()
+        for event in xml.getchildren():
+            if event.tag == 'claimtype':
+                claim.claimtype = self.readTerm(event)
+            elif event.tag == 'label':
+                # We store the full protocol,label construct for
+                # consistency with the technical parts, so it is left to
+                # the __str__ of claim to select the right element
+                claim.label = self.readTerm(event)
+            elif event.tag == 'protocol':
+                claim.protocol = self.readTerm(event)
+            elif event.tag == 'role':
+                claim.role = self.readTerm(event)
+            elif event.tag == 'parameter':
+                claim.parameter = self.readTerm(event)
+
+            elif event.tag == 'failed':
+                claim.failed = int(event.text)
+            elif event.tag == 'count':
+                claim.count = int(event.text)
+            elif event.tag == 'states':
+                claim.states = int(event.text)
+
+            elif event.tag == 'complete':
+                claim.complete = True
+            elif event.tag == 'timebound':
+                claim.timebound = True
+            else:
+                print >>sys.stderr,"Warning unknown tag in claim: %s" % claim.tag
+
+        claim.analyze()
+        return claim
+
+    def readAttack(self, xml):
+        self.varlist = []
+        attack = Attack.Attack()
+        attack.id = int(xml.get('id'))
+        # A state contains 4 direct child nodes:
+        # broken, system, variables and semitrace
+        # optionally a fifth: dot
+        for event in xml.getchildren():
+            if event.tag == 'broken':
+                attack.broken.append((self.readTerm(event.find('claim')),
+                    self.readTerm(event.find('label'))))
+            elif event.tag == 'system':
+                attack.match = int(event.find('match').text)
+                for term in event.find('commandline'):
+                    if attack.commandline != '':
+                        attack.commandline += ' ' 
+                    attack.commandline += term.text 
+                for term in event.find('untrusted').find('termlist'):
+                    attack.untrusted.append(str(self.readTerm(term)))
+                for term in event.find('initialknowledge').find('termlist'):
+                    attack.initialKnowledge.append(self.readTerm(term))
+                for keypair in event.find('inversekeys'):
+                    inverse = []
+                    for term in keypair:
+                        inverse.append(self.readTerm(term))
+                    assert(len(inverse) == 0 or len(inverse) == 2)
+                    attack.inverseKeys.append(inverse)
+                # TODO why is protocol name a term??
+                for protocolxml in event.findall('protocol'):
+                    protocol = str(self.readTerm(protocolxml.find('name')))
+                    descr = Trace.ProtocolDescription(protocol)
+                    attack.protocoldescr[protocol] = descr
+                    for rolexml in protocolxml.findall('role'):
+                        roledescr = self.readRoleDescr(rolexml)
+                        descr.roledescr[roledescr.role] = roledescr
+                    
+            elif event.tag == 'semitrace':
+                for runxml in event:
+                    run = self.readRun(runxml)
+                    run.attack = attack
+                    attack.semiTrace.runs.append(run)
+
+            elif event.tag == 'dot':
+                # Apparently Scyther already generated dot output,
+                # store
+                attack.scytherDot = event.text
+
+            elif event.tag == 'variables':
+                # Read the variables one by one
+                for varxml in event:
+                    if varxml.get('typeflaw') == 'true':
+                        attack.typeflaws = True
+                    var = self.readTerm(varxml.find('name').find('term'))
+                    var.types = self.readTypeList(varxml.find('name'))
+                    
+                    substxml = varxml.find('substitution')
+                    # Read substitution if present
+                    if substxml != None:
+                        subst = self.readTerm(substxml.find('term'))
+                        subst.types = self.readTypeList(substxml)
+                        newvar = Term.TermVariable(var.name,subst)
+                        newvar.types = var.types
+                        var = newvar
+                        
+                    attack.variables.append(var)
+                    
+                # When all have been read set self.varlist so that when
+                # we read terms in the attacks they can be filled in using
+                # this list
+                self.varlist = attack.variables
+            else:
+                print >>sys.stderr,"Warning unknown tag in attack: %s" % event.tag
+        return attack
+    
--- a/gui/images/scyther-icon.svg
+++ b/gui/images/scyther-icon.svg
@ -0,0 +1,222 @@
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<!-- Created with Inkscape (http://www.inkscape.org/) -->
+<svg
+   xmlns:dc="http://purl.org/dc/elements/1.1/"
+   xmlns:cc="http://web.resource.org/cc/"
+   xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#"
+   xmlns:svg="http://www.w3.org/2000/svg"
+   xmlns="http://www.w3.org/2000/svg"
+   xmlns:xlink="http://www.w3.org/1999/xlink"
+   xmlns:sodipodi="http://inkscape.sourceforge.net/DTD/sodipodi-0.dtd"
+   xmlns:inkscape="http://www.inkscape.org/namespaces/inkscape"
+   width="841.88977pt"
+   height="595.27557pt"
+   id="svg2"
+   sodipodi:version="0.32"
+   inkscape:version="0.43"
+   version="1.0"
+   sodipodi:docbase="/home/cas/bzr/scyther-gui/images"
+   sodipodi:docname="scyther-icon.svg"
+   inkscape:export-filename="/home/cas/svn/scyther/Design download page Scyther/scyther-icon16.png"
+   inkscape:export-xdpi="1.6494846"
+   inkscape:export-ydpi="1.6494846">
+  <defs
+     id="defs4">
+    <linearGradient
+       id="linearGradient11078">
+      <stop
+         id="stop11080"
+         offset="0"
+         style="stop-color:#000000;stop-opacity:0.57731956;" />
+      <stop
+         style="stop-color:#000000;stop-opacity:0;"
+         offset="0.209216"
+         id="stop11084" />
+      <stop
+         id="stop11086"
+         offset="0.65205503"
+         style="stop-color:#000000;stop-opacity:0.2371134;" />
+      <stop
+         id="stop11082"
+         offset="1"
+         style="stop-color:#000000;stop-opacity:0.67010307;" />
+    </linearGradient>
+    <linearGradient
+       id="linearGradient11052">
+      <stop
+         id="stop11054"
+         offset="0"
+         style="stop-color:#000000;stop-opacity:1;" />
+      <stop
+         style="stop-color:#276816;stop-opacity:1;"
+         offset="0.25145975"
+         id="stop11060" />
+      <stop
+         id="stop11066"
+         offset="0.57149941"
+         style="stop-color:#000000;stop-opacity:1;" />
+      <stop
+         id="stop11062"
+         offset="0.57149941"
+         style="stop-color:#010400;stop-opacity:1;" />
+      <stop
+         style="stop-color:#002583;stop-opacity:1;"
+         offset="0.8028897"
+         id="stop11064" />
+      <stop
+         id="stop11056"
+         offset="1"
+         style="stop-color:#000000;stop-opacity:1;" />
+    </linearGradient>
+    <linearGradient
+       id="linearGradient11044">
+      <stop
+         style="stop-color:#000000;stop-opacity:1;"
+         offset="0"
+         id="stop11046" />
+      <stop
+         style="stop-color:#000000;stop-opacity:0;"
+         offset="1"
+         id="stop11048" />
+    </linearGradient>
+    <linearGradient
+       id="linearGradient7532">
+      <stop
+         id="stop7534"
+         offset="0"
+         style="stop-color:#9e9e9e;stop-opacity:1;" />
+      <stop
+         id="stop7536"
+         offset="1"
+         style="stop-color:#9e9e9e;stop-opacity:0;" />
+    </linearGradient>
+    <linearGradient
+       inkscape:collect="always"
+       xlink:href="#linearGradient11052"
+       id="linearGradient5737"
+       x1="521.7384"
+       y1="589.8822"
+       x2="521.7384"
+       y2="174.88217"
+       gradientUnits="userSpaceOnUse" />
+    <linearGradient
+       inkscape:collect="always"
+       xlink:href="#linearGradient11044"
+       id="linearGradient8364"
+       gradientUnits="userSpaceOnUse"
+       x1="323.7384"
+       y1="278.88214"
+       x2="477.7384"
+       y2="322.88214" />
+  </defs>
+  <sodipodi:namedview
+     id="base"
+     pagecolor="#ffffff"
+     bordercolor="#666666"
+     borderopacity="1.0"
+     inkscape:pageopacity="0.0"
+     inkscape:pageshadow="2"
+     inkscape:zoom="1"
+     inkscape:cx="526.18109"
+     inkscape:cy="372.04724"
+     inkscape:document-units="px"
+     inkscape:current-layer="layer1"
+     showguides="true"
+     inkscape:guide-bbox="true"
+     inkscape:window-width="1280"
+     inkscape:window-height="953"
+     inkscape:window-x="0"
+     inkscape:window-y="0">
+    <sodipodi:guide
+       orientation="horizontal"
+       position="296.88141"
+       id="guide1366" />
+    <sodipodi:guide
+       orientation="horizontal"
+       position="571.88122"
+       id="guide8421" />
+    <sodipodi:guide
+       orientation="vertical"
+       position="206.87725"
+       id="guide8423" />
+  </sodipodi:namedview>
+  <metadata
+     id="metadata7">
+    <rdf:RDF>
+      <cc:Work
+         rdf:about="">
+        <dc:format>image/svg+xml</dc:format>
+        <dc:type
+           rdf:resource="http://purl.org/dc/dcmitype/StillImage" />
+      </cc:Work>
+    </rdf:RDF>
+  </metadata>
+  <g
+     inkscape:label="Black base"
+     inkscape:groupmode="layer"
+     id="layer1"
+     style="display:inline"
+     sodipodi:insensitive="true">
+    <rect
+       style="opacity:1;fill:url(#linearGradient5737);fill-opacity:1;stroke:#000000;stroke-width:6.73799992;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"
+       id="rect7546"
+       width="323.44028"
+       height="320.51846"
+       x="194.92915"
+       y="162.62292" />
+  </g>
+  <g
+     inkscape:groupmode="layer"
+     id="layer9"
+     inkscape:label="inner fade"
+     sodipodi:insensitive="true"
+     style="display:inline">
+    <rect
+       style="opacity:1;fill:url(#linearGradient8364);fill-opacity:1;stroke:#000000;stroke-width:6.73799992;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1;display:inline"
+       id="rect7489"
+       width="323.44028"
+       height="320.51846"
+       x="194.92915"
+       y="162.62292" />
+  </g>
+  <g
+     inkscape:groupmode="layer"
+     id="layer7"
+     inkscape:label="blacker fades"
+     style="display:inline"
+     sodipodi:insensitive="true" />
+  <g
+     inkscape:groupmode="layer"
+     id="layer4"
+     inkscape:label="white inner"
+     style="display:inline">
+    <path
+       style="font-size:48px;font-style:oblique;font-variant:normal;font-weight:bold;font-stretch:normal;text-align:start;line-height:125%;writing-mode:lr-tb;text-anchor:start;opacity:1;fill:#ffffff;fill-opacity:1;stroke:#000000;stroke-width:15.39999962;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:8.60000038;stroke-dasharray:none;stroke-opacity:1;display:inline;font-family:Luxi Serif"
+       d="M 439.625,186.5625 L 228.875,186.96875 L 229,447.625 L 298.46875,447.0625 C 330.87282,446.92031 358.52897,437.28122 380.09375,420.40625 C 401.65809,403.53126 412.43728,382.80494 412.4375,358.21875 C 412.43728,345.47874 408.75517,334.539 401.375,325.375 C 394.57101,316.65817 381.16868,305.92772 361.21875,293.1875 L 346,283.46875 C 335.8349,277.00229 328.44922,270.61422 323.78125,264.34375 C 307.04223,258.53812 294.42062,259.0563 268.875,259.90625 C 278.05518,239.8488 296.11407,242.38722 300.21875,237.3125 C 304.95019,231.46292 305.43096,234.13065 309.84375,229.25 C 321.81701,216.0073 334.34348,209.33336 346.96875,206.0625 C 353.47544,203.07236 360.58299,201.56871 368.3125,201.65625 C 397.62337,201.98826 427.75001,225.34375 427.75,225.34375 L 439.625,186.5625 z "
+       id="path7544"
+       sodipodi:nodetypes="ccccsscccccsscscc" />
+  </g>
+  <g
+     inkscape:groupmode="layer"
+     id="layer8"
+     inkscape:label="upper white"
+     style="display:inline">
+    <path
+       style="font-size:48px;font-style:oblique;font-variant:normal;font-weight:bold;font-stretch:normal;text-align:start;line-height:125%;writing-mode:lr-tb;text-anchor:start;opacity:1;fill:#ffffff;fill-opacity:1;stroke:none;stroke-width:8.89999962;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:8.60000038;stroke-dasharray:none;stroke-opacity:1;display:inline;font-family:Luxi Serif"
+       d="M 439.625,186.5625 L 228.875,186.96875 L 229,447.625 L 298.46875,447.0625 C 330.87282,446.92031 358.52897,437.28122 380.09375,420.40625 C 401.65809,403.53126 412.43728,382.80494 412.4375,358.21875 C 412.43728,345.47874 408.75517,334.539 401.375,325.375 C 394.57101,316.65817 381.16868,305.92772 361.21875,293.1875 L 346,283.46875 C 335.8349,277.00229 328.44922,270.61422 323.78125,264.34375 C 307.04223,258.53812 294.42062,259.0563 268.875,259.90625 C 278.05518,239.8488 296.11407,242.38722 300.21875,237.3125 C 304.95019,231.46292 305.43096,234.13065 309.84375,229.25 C 321.81701,216.0073 334.34348,209.33336 346.96875,206.0625 C 353.47544,203.07236 360.58299,201.56871 368.3125,201.65625 C 397.62337,201.98826 427.75001,225.34375 427.75,225.34375 L 439.625,186.5625 z "
+       id="path6613"
+       sodipodi:nodetypes="ccccsscccccsscscc" />
+  </g>
+  <g
+     inkscape:groupmode="layer"
+     id="layer5"
+     inkscape:label="beak"
+     style="display:inline"
+     sodipodi:insensitive="true" />
+  <g
+     inkscape:groupmode="layer"
+     id="layer3"
+     inkscape:label="cyther"
+     style="display:inline"
+     sodipodi:insensitive="true" />
+</svg>
--- a/gui/images/scyther-logo.svg
+++ b/gui/images/scyther-logo.svg
--- a/gui/images/scyther-splash.png
+++ b/gui/images/scyther-splash.png
--- a/gui/images/scyther-splash.xcf
+++ b/gui/images/scyther-splash.xcf
--- a/gui/ns3.spdl
+++ b/gui/ns3.spdl
@ -0,0 +1,51 @@
+/* 
+ * Needham-Schroeder protocol
+ */
+
+// PKI infrastructure
+
+const pk: Function;
+secret sk: Function;
+inversekeys (pk,sk);
+
+// The protocol description
+
+protocol ns3(I,R)
+{
+	role I
+	{
+		const ni: Nonce;
+		var nr: Nonce;
+
+		send_1(I,R, {I,ni}pk(R) );
+		read_2(R,I, {ni,nr}pk(I) );
+		send_3(I,R, {nr}pk(R) );
+
+		claim_i1(I,Secret,ni);
+		claim_i2(I,Secret,nr);
+		claim_i3(I,Niagree);
+		claim_i4(I,Nisynch);
+	}	
+	
+	role R
+	{
+		var ni: Nonce;
+		const nr: Nonce;
+
+		read_1(I,R, {I,ni}pk(R) );
+		send_2(R,I, {ni,nr}pk(I) );
+		read_3(I,R, {nr}pk(R) );
+
+		claim_r1(R,Secret,ni);
+		claim_r2(R,Secret,nr);
+		claim_r3(R,Niagree);
+		claim_r4(R,Nisynch);
+	}
+}
+
+// An untrusted agent, with leaked information
+
+const Eve: Agent;
+untrusted Eve;
+compromised sk(Eve);
+
--- a/gui/nsl3.spdl
+++ b/gui/nsl3.spdl
@ -0,0 +1,51 @@
+/* 
+ * Needham-Schroeder-Lowe protocol
+ */
+
+// PKI infrastructure
+
+const pk: Function;
+secret sk: Function;
+inversekeys (pk,sk);
+
+// The protocol description
+
+protocol nsl3(I,R)
+{
+	role I
+	{
+		const ni: Nonce;
+		var nr: Nonce;
+
+		send_1(I,R, {I,ni}pk(R) );
+		read_2(R,I, {ni,nr,R}pk(I) );
+		send_3(I,R, {nr}pk(R) );
+
+		claim_i1(I,Secret,ni);
+		claim_i2(I,Secret,nr);
+		claim_i3(I,Niagree);
+		claim_i4(I,Nisynch);
+	}	
+	
+	role R
+	{
+		var ni: Nonce;
+		const nr: Nonce;
+
+		read_1(I,R, {I,ni}pk(R) );
+		send_2(R,I, {ni,nr,R}pk(I) );
+		read_3(I,R, {nr}pk(R) );
+
+		claim_r1(R,Secret,ni);
+		claim_r2(R,Secret,nr);
+		claim_r3(R,Niagree);
+		claim_r4(R,Nisynch);
+	}
+}
+
+// An untrusted agent, with leaked information
+
+const Eve: Agent;
+untrusted Eve;
+compromised sk(Eve);
+
--- a/gui/scyther-gui-16.ico
+++ b/gui/scyther-gui-16.ico
--- a/gui/scyther-gui-32.ico
+++ b/gui/scyther-gui-32.ico
--- a/gui/scyther-gui-64.ico
+++ b/gui/scyther-gui-64.ico
--- a/gui/scyther-gui.py
+++ b/gui/scyther-gui.py
@ -0,0 +1,77 @@
+#!/usr/bin/python
+
+#---------------------------------------------------------------------------
+
+""" Import externals """
+import wx
+
+#---------------------------------------------------------------------------
+
+""" Import scyther-gui components """
+import Preference
+import Mainwindow
+import Misc
+
+#---------------------------------------------------------------------------
+
+class MySplashScreen(wx.SplashScreen):
+    def __init__(self):
+        bmp = wx.Image(Misc.mypath("images/scyther-splash.png")).ConvertToBitmap()
+        wx.SplashScreen.__init__(self, bmp,
+                                 wx.SPLASH_CENTRE_ON_SCREEN | wx.SPLASH_TIMEOUT,
+                                 5000, None, -1)
+        self.Bind(wx.EVT_CLOSE, self.OnClose)
+        self.fc = wx.FutureCall(2000, self.ShowMain)
+
+    def OnClose(self, evt):
+        # Make sure the default handler runs too so this window gets
+        # destroyed
+        evt.Skip()
+        self.Hide()
+        
+        # if the timer is still running then go ahead and show the
+        # main frame now
+        if self.fc.IsRunning():
+            self.fc.Stop()
+            self.ShowMain()
+
+
+    def ShowMain(self):
+        if self.fc.IsRunning():
+            self.Raise()
+        
+
+
+class ScytherApp(wx.App):
+    def OnInit(self):
+
+        """
+        Load preferences file
+        """
+
+        Preference.init()
+
+        """
+        Create and show the splash screen.  It will then create and show
+        the main frame when it is time to do so.
+        """
+
+
+        splash = MySplashScreen()
+        splash.Show()
+
+        """ Build up """
+        self.mainWindow = Mainwindow.MainWindow('scythergui-default.spdl')
+        self.SetTopWindow(self.mainWindow)
+        self.mainWindow.Show()
+
+        return True
+
+    def OnExit(self):
+        """ Tear down """
+
+if __name__ == '__main__':
+    scythergui = ScytherApp()
+    scythergui.MainLoop()
+
+
--- a/gui/scythergui-default.spdl
+++ b/gui/scythergui-default.spdl
@ -0,0 +1,51 @@
+/* 
+ * Needham-Schroeder protocol
+ */
+
+// PKI infrastructure
+
+const pk: Function;
+secret sk: Function;
+inversekeys (pk,sk);
+
+// The protocol description
+
+protocol ns3(I,R)
+{
+	role I
+	{
+		const ni: Nonce;
+		var nr: Nonce;
+
+		send_1(I,R, {I,ni}pk(R) );
+		read_2(R,I, {ni,nr}pk(I) );
+		send_3(I,R, {nr}pk(R) );
+
+		claim_i1(I,Secret,ni);
+		claim_i2(I,Secret,nr);
+		claim_i3(I,Niagree);
+		claim_i4(I,Nisynch);
+	}	
+	
+	role R
+	{
+		var ni: Nonce;
+		const nr: Nonce;
+
+		read_1(I,R, {I,ni}pk(R) );
+		send_2(R,I, {ni,nr}pk(I) );
+		read_3(I,R, {nr}pk(R) );
+
+		claim_r1(R,Secret,ni);
+		claim_r2(R,Secret,nr);
+		claim_r3(R,Niagree);
+		claim_r4(R,Nisynch);
+	}
+}
+
+// An untrusted agent, with leaked information
+
+const Eve: Agent;
+untrusted Eve;
+compromised sk(Eve);
+
--- a/gui/todo.txt
+++ b/gui/todo.txt
@ -0,0 +1,9 @@
+- Ideally we somehow color the correct/incorrect tags in the editor.
+- Line numbering is needed for the editor window otherwise you cannot
+  interpret attacks.
+- Bottom bar should have obvious 'view' buttons for attacks that provide
+  views, to guide the user.
+- Preferences window.
+  - Save in local file on close.
+  - Scyther executable should be able to be set by means of preferences.
+    (Using a file select dialog)