diff --git a/gui/Attack.py b/gui/Attack.py new file mode 100644 index 0000000..b48c9df --- /dev/null +++ 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 diff --git a/gui/Attackimage.py b/gui/Attackimage.py new file mode 100644 index 0000000..950ffb3 --- /dev/null +++ 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 + +#--------------------------------------------------------------------------- + diff --git a/gui/Attackwindow.py b/gui/Attackwindow.py new file mode 100644 index 0000000..7460d1a --- /dev/null +++ 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() + diff --git a/gui/Claim.py b/gui/Claim.py new file mode 100644 index 0000000..edcef99 --- /dev/null +++ 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 + + diff --git a/gui/Icon.py b/gui/Icon.py new file mode 100644 index 0000000..10abb78 --- /dev/null +++ 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) + + diff --git a/gui/Mainwindow.py b/gui/Mainwindow.py new file mode 100644 index 0000000..ef1a612 --- /dev/null +++ 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) + +#--------------------------------------------------------------------------- + + + diff --git a/gui/Misc.py b/gui/Misc.py new file mode 100644 index 0000000..4346491 --- /dev/null +++ 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) + diff --git a/gui/Preference.py b/gui/Preference.py new file mode 100644 index 0000000..974227e --- /dev/null +++ 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() + + diff --git a/gui/Scyther.py b/gui/Scyther.py new file mode 100755 index 0000000..6dadb06 --- /dev/null +++ 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() + + diff --git a/gui/Scytherthread.py b/gui/Scytherthread.py new file mode 100644 index 0000000..9194ee7 --- /dev/null +++ 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 ] + + diff --git a/gui/Tempfile.py b/gui/Tempfile.py new file mode 100644 index 0000000..8d5d038 --- /dev/null +++ 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) diff --git a/gui/Term.py b/gui/Term.py new file mode 100644 index 0000000..fcb4b23 --- /dev/null +++ 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) + diff --git a/gui/Trace.py b/gui/Trace.py new file mode 100644 index 0000000..1f6718a --- /dev/null +++ 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()) diff --git a/gui/XMLReader.py b/gui/XMLReader.py new file mode 100644 index 0000000..94221f1 --- /dev/null +++ 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 + diff --git a/gui/images/scyther-icon.svg b/gui/images/scyther-icon.svg new file mode 100644 index 0000000..7586c82 --- /dev/null +++ b/gui/images/scyther-icon.svg @@ -0,0 +1,222 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + image/svg+xml + + + + + + + + + + + + + + + + + + + + diff --git a/gui/images/scyther-logo.svg b/gui/images/scyther-logo.svg new file mode 100644 index 0000000..45a080f --- /dev/null +++ b/gui/images/scyther-logo.svg @@ -0,0 +1,249 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + image/svg+xml + + + + + + + + + + + + + + + + + + + + + + + diff --git a/gui/images/scyther-splash.png b/gui/images/scyther-splash.png new file mode 100644 index 0000000..30849f3 Binary files /dev/null and b/gui/images/scyther-splash.png differ diff --git a/gui/images/scyther-splash.xcf b/gui/images/scyther-splash.xcf new file mode 100644 index 0000000..9a3ff93 Binary files /dev/null and b/gui/images/scyther-splash.xcf differ diff --git a/gui/ns3.spdl b/gui/ns3.spdl new file mode 100644 index 0000000..caef79c --- /dev/null +++ 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); + diff --git a/gui/nsl3.spdl b/gui/nsl3.spdl new file mode 100644 index 0000000..04d02a0 --- /dev/null +++ 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); + diff --git a/gui/scyther-gui-16.ico b/gui/scyther-gui-16.ico new file mode 100644 index 0000000..a92d822 Binary files /dev/null and b/gui/scyther-gui-16.ico differ diff --git a/gui/scyther-gui-32.ico b/gui/scyther-gui-32.ico new file mode 100644 index 0000000..b87d7f9 Binary files /dev/null and b/gui/scyther-gui-32.ico differ diff --git a/gui/scyther-gui-64.ico b/gui/scyther-gui-64.ico new file mode 100644 index 0000000..2fb682f Binary files /dev/null and b/gui/scyther-gui-64.ico differ diff --git a/gui/scyther-gui.py b/gui/scyther-gui.py new file mode 100755 index 0000000..2945667 --- /dev/null +++ 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() + + diff --git a/gui/scythergui-default.spdl b/gui/scythergui-default.spdl new file mode 100644 index 0000000..caef79c --- /dev/null +++ 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); + diff --git a/gui/todo.txt b/gui/todo.txt new file mode 100644 index 0000000..a4f2b01 --- /dev/null +++ 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)