From 1542d65def722fc10121fd299651f71aa1d313be Mon Sep 17 00:00:00 2001 From: Cas Cremers Date: Fri, 18 May 2007 14:06:29 +0200 Subject: [PATCH] - Big catchup commit to make sure we are up to beta7. This includes a number of single patches, ranging from the vista fix with the buffers, to the start of many new minor features. --- gui/.gitignore | 1 + gui/Gui/About.py | 23 +++++- gui/Gui/Attackwindow.py | 1 + gui/Gui/Editor.py | 25 ++++++ gui/Gui/Mainwindow.py | 90 +++++++++++++++++---- gui/Gui/Scytherthread.py | 69 +++++++++++----- gui/Gui/Settingswindow.py | 4 +- gui/Scyther/Claim.py | 4 +- gui/Scyther/Error.py | 2 +- gui/Scyther/Scyther.py | 29 +++++++ src/BuildUnix-Win32.cmake | 7 ++ src/BuildUnix.cmake | 4 + src/CMakeLists.txt | 4 +- src/arachne.c | 163 ++++++++++++++++++++++++++++++-------- src/binding.c | 4 +- src/bugs.txt | 39 +++++++++ src/build.sh | 6 -- src/compiler.c | 58 +++++++++----- src/intruderknowledge.c | 2 + src/list.c | 7 +- src/mgu.c | 13 +-- src/mgu.h | 1 - src/problem.spdl | 6 +- src/reindent.sh | 2 - src/specialterm.c | 27 ++++++- src/specialterm.h | 7 ++ src/system.c | 5 +- src/term.h | 4 +- src/termlist.c | 6 +- src/termlist.h | 1 - src/todo.txt | 5 +- src/type.c | 113 +++++++++++++------------- src/type.h | 4 +- src/warshall.h | 2 + src/xmlout.c | 4 +- 35 files changed, 538 insertions(+), 204 deletions(-) create mode 100644 gui/.gitignore diff --git a/gui/.gitignore b/gui/.gitignore new file mode 100644 index 0000000..0d20b64 --- /dev/null +++ b/gui/.gitignore @@ -0,0 +1 @@ +*.pyc diff --git a/gui/Gui/About.py b/gui/Gui/About.py index 1398c50..5ac5ee8 100644 --- a/gui/Gui/About.py +++ b/gui/Gui/About.py @@ -11,6 +11,8 @@ import os.path """ Import scyther-gui components """ +import Scyther + #--------------------------------------------------------------------------- """ Globals """ @@ -19,9 +21,17 @@ basedir = "" #--------------------------------------------------------------------------- +def setBaseDir(mybasedir): + global basedir + + basedir = mybasedir + +#--------------------------------------------------------------------------- + class AboutScyther(wx.Dialog): def __init__(self,parent,mybasedir=None): + from Version import SCYTHER_GUI_VERSION global basedir self.text = ''' @@ -29,6 +39,7 @@ class AboutScyther(wx.Dialog):

Scyther : $VERSION

+

Scyther is an automatic tool for the verification and falsification of security protocols. @@ -42,21 +53,31 @@ class AboutScyther(wx.Dialog): http://people.inf.ethz.ch/cremersc/scyther/index.html

+

+ $DETAILS +

Credits: Cas Cremers (Scyther theory, backend, and main GUI code), Gijs Hollestelle (Python parser for Scyther XML output).

+ ''' if mybasedir: basedir = mybasedir + # Debugging output of some parameters + splashdir = os.path.join(basedir,"Images") splashimage = os.path.join(splashdir,"scyther-splash.png") + details_html = "Base directory: %s
\n" % (basedir) + details_html += Scyther.Scyther.GetInfo(html=True) + self.text = self.text.replace("$SPLASH",splashimage) + self.text = self.text.replace("$DETAILS",details_html) # version information - self.text = self.text.replace("$VERSION", "1.0-beta6") + self.text = self.text.replace("$VERSION", SCYTHER_GUI_VERSION) wx.Dialog.__init__(self, parent, -1, 'About Scyther', size=(660,620)) diff --git a/gui/Gui/Attackwindow.py b/gui/Gui/Attackwindow.py index 5987f5e..a8b8741 100644 --- a/gui/Gui/Attackwindow.py +++ b/gui/Gui/Attackwindow.py @@ -183,6 +183,7 @@ class AttackWindow(wx.Frame): # Add attacks (possible with tabs) self.displays=[] attacks = self.claim.attacks + n = len(attacks) if n <= 1: # Just a single window diff --git a/gui/Gui/Editor.py b/gui/Gui/Editor.py index b8c40d5..1474e0b 100644 --- a/gui/Gui/Editor.py +++ b/gui/Gui/Editor.py @@ -71,10 +71,35 @@ class Editor(object): def __init__(self, parent): # Empty start self.SetText("") + self.SetChanged(False) + + def SetText(self): + pass def SetErrors(self,errors): pass + def GetChanged(self): + """ + Return true if file was changed + """ + return self.savedtext != self.GetText() + + def SetChanged(self,nowchanged=False): + """ + Set changed status + """ + if nowchanged: + self.savedtext = "" + else: + self.SetSaved() + + def SetSaved(self): + self.savedtext = self.GetText() + + def SetOpened(self): + self.SetSaved() + #--------------------------------------------------------------------------- class EditorNormal(Editor): diff --git a/gui/Gui/Mainwindow.py b/gui/Gui/Mainwindow.py index 006ece5..d4f50cc 100644 --- a/gui/Gui/Mainwindow.py +++ b/gui/Gui/Mainwindow.py @@ -20,7 +20,7 @@ import Editor """ Some constants """ ID_VERIFY = 100 ID_AUTOVERIFY = 101 -ID_STATESPACE = 102 +ID_CHARACTERIZE = 102 ID_CHECK = 103 #--------------------------------------------------------------------------- @@ -47,7 +47,7 @@ class MainWindow(wx.Frame): if len(args) > 0: filename = args[0] if filename != '' and os.path.isfile(filename): - self.filename = filename + (self.dirname,self.filename) = os.path.split(filename) self.load = True Icon.ScytherIcon(self) @@ -60,7 +60,7 @@ class MainWindow(wx.Frame): (wx.ACCEL_NORMAL, wx.WXK_F1, ID_VERIFY), (wx.ACCEL_NORMAL, wx.WXK_F2, - ID_STATESPACE), + ID_CHARACTERIZE), (wx.ACCEL_NORMAL, wx.WXK_F5, ID_CHECK), (wx.ACCEL_NORMAL, wx.WXK_F6, @@ -85,9 +85,9 @@ class MainWindow(wx.Frame): #bt = wx.Button(self,ID_VERIFY) #buttons.Add(bt,0) #self.Bind(wx.EVT_BUTTON, self.OnVerify, bt) - #bt = wx.Button(self,ID_STATESPACE) + #bt = wx.Button(self,ID_CHARACTERIZE) #buttons.Add(bt,0) - #self.Bind(wx.EVT_BUTTON, self.OnStatespace, bt) + #self.Bind(wx.EVT_BUTTON, self.OnCharacterize, bt) #sizer.Add(buttons, 0, wx.ALIGN_LEFT) # Top: input @@ -98,8 +98,11 @@ class MainWindow(wx.Frame): if self.load: textfile = open(os.path.join(self.dirname, self.filename), 'r') self.editor.SetText(textfile.read()) - os.chdir(self.dirname) + if self.dirname != "": + os.chdir(self.dirname) textfile.close() + self.editor.SetOpened() + self.top.AddPage(self.editor.control,"Protocol description") self.settings = Settingswindow.SettingsWindow(self.top,self) self.top.AddPage(self.settings,"Settings") @@ -138,8 +141,8 @@ class MainWindow(wx.Frame): 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.OnStatespace) , + (ID_CHARACTERIZE, '&Characterize roles\tF2','TODO' , + self.OnCharacterize) , (None, None, None, None), ### Disabled for now (given that it is not reliable enough yet) #(ID_CHECK, '&Check protocol\tF5','TODO', @@ -179,7 +182,49 @@ class MainWindow(wx.Frame): dialog.Destroy() return userProvidedFilename - # Event handlers: + # Are we dropping a changed file? + + def ConfirmLoss(self,text=None): + """ + Try to drop the current file. If it was changed, try to save + (as) + + Returns true after the user seems to be happy either way, false + if we need to cancel this. + """ + if self.editor.GetChanged(): + # File changed, we need to confirm this + title = "Unsaved changes" + if text: + title = "%s - " + title + txt = "The protocol file '%s' has been modified.\n\n" % (self.filename) + txt = txt + "Do you want to" + txt = txt + " save your changes (Yes)" + txt = txt + " or" + txt = txt + " discard them (No)" + txt = txt + "?" + dialog = wx.MessageDialog(self,txt,title,wx.YES_NO | wx.CANCEL | wx.ICON_EXCLAMATION) + result = dialog.ShowModal() + dialog.Destroy() + if result == wx.ID_NO: + # Drop changes + return True + elif result == wx.ID_YES: + # First save(as)! + if self.OnSaveAs(None): + # Succeeded, we can continue with the operation + return True + else: + # Save did not succeed + return False + else: + # Assume cancel (wx.ID_CANCEL) otherwise + return False + else: + # File was not changed, so we can just proceed + return True + + # Event handlers def OnAbout(self, event): dlg = About.AboutScyther(self) @@ -187,25 +232,36 @@ class MainWindow(wx.Frame): dlg.Destroy() def OnExit(self, event): - self.Close() # Close the main window. + if self.ConfirmLoss("Exit"): + self.Close() # Close the main window. + return True + return False def OnSave(self, event): textfile = open(os.path.join(self.dirname, self.filename), 'w') textfile.write(self.editor.GetText()) textfile.close() + self.editor.SetSaved() + return True def OnOpen(self, event): - if self.askUserForFilename(style=wx.OPEN, - **self.defaultFileDialogOptions()): - textfile = open(os.path.join(self.dirname, self.filename), 'r') - self.editor.SetText(textfile.read()) - textfile.close() + if self.ConfirmLoss("Open"): + if self.askUserForFilename(style=wx.OPEN, + **self.defaultFileDialogOptions()): + textfile = open(os.path.join(self.dirname, self.filename), 'r') + self.editor.SetText(textfile.read()) + textfile.close() + self.editor.SetOpened() + return True + return False def OnSaveAs(self, event): if self.askUserForFilename(defaultFile=self.filename, style=wx.SAVE, **self.defaultFileDialogOptions()): self.OnSave(event) os.chdir(self.dirname) + return True + return False def RunScyther(self, mode): # Clear errors before verification @@ -220,8 +276,8 @@ class MainWindow(wx.Frame): def OnAutoVerify(self, event): self.RunScyther("autoverify") - def OnStatespace(self, event): - self.RunScyther("statespace") + def OnCharacterize(self, event): + self.RunScyther("characterize") def OnCheck(self, event): self.RunScyther("check") diff --git a/gui/Gui/Scytherthread.py b/gui/Gui/Scytherthread.py index 36a5624..004788a 100644 --- a/gui/Gui/Scytherthread.py +++ b/gui/Gui/Scytherthread.py @@ -34,11 +34,12 @@ class ScytherThread(threading.Thread): """ # Override Thread's __init__ method to accept the parameters needed: - def __init__ ( self, spdl, options="", callback=None ): + def __init__ ( self, spdl, options="", callback=None, mode=None ): self.spdl = spdl self.options = options self.callback = callback + self.mode = mode threading.Thread.__init__ ( self ) def run(self): @@ -49,6 +50,17 @@ class ScytherThread(threading.Thread): if self.callback: wx.CallAfter(self.callback, scyther, claims, summary) + def claimFixViewOne(self,claims): + if claims: + for cl in claims: + if len(cl.attacks) > 1: + # Fix it such that by default, only the best attack is + # shown, unless we are in characterize or check mode + # TODO [X] [CC] make switch-dependant. + if not self.mode in ["characterize","check"]: + cl.attacks = [cl.attacks[-1]] + + return claims def claimResults(self): """ Convert spdl to result (using Scyther) @@ -68,6 +80,8 @@ class ScytherThread(threading.Thread): summary = str(scyther) + claims = self.claimFixViewOne(claims) + return (scyther, claims, summary) #--------------------------------------------------------------------------- @@ -123,6 +137,7 @@ class AttackThread(threading.Thread): def graphLine(txt): fp.write("\t%s;\n" % (txt)) + print txt # DEBUG ONLY def setAttr(atxt,EdgeNodeDefAll=ALL): if EdgeNodeDefAll == ALL: @@ -139,6 +154,13 @@ class AttackThread(threading.Thread): return graphLine("%s [%s]" % (edge,atxt)) + # Precompute font name + # Set a font with sans + # We only retrieve the name, so the size '9' here is + # irrelevant. + font = wx.Font(9,wx.SWISS,wx.NORMAL,wx.NORMAL) + self.fontname = font.GetFaceName() + # write all graph lines but add layout modifiers for l in txt.splitlines(): fp.write(l) @@ -151,23 +173,22 @@ class AttackThread(threading.Thread): #graphLine("nodesep=0.1") #graphLine("ranksep=0.001") #graphLine("mindist=0.1") - if sys.platform.startswith("lin"): - # For Linux, choose Helvetica - # TODO - # This is really a Mac font so it might not be - # available. Still, it works better on my Ubuntu - # than Verdana, and finding a good sans default for - # linux seems problematic. - setAttr("fontname=\"Helvetica\"") - if sys.platform.startswith("mac"): - # For Mac choose Helvetica - setAttr("fontname=\"Helvetica\"") - if sys.platform.startswith("win"): - # For Windows choose Verdana - setAttr("fontname=\"Verdana\"") + + # Set fontname + fontstring = "fontname=%s" % (self.fontname) + setAttr(fontstring,EDGE) + + # Stupid Mac <> Graphviz bug fix + if (sys.platform.startswith("mac")) or (sys.platform.startswith("darwin")): + # Note that dot on Mac cannot find the fonts by default, + # and we have to set them accordingly. + os.environ["DOTFONTPATH"]="~/Library/Fonts:/Library/Fonts:/System/Library/Fonts" + + # Select font size if self.parent and self.parent.mainwin: fontsize = self.parent.mainwin.settings.fontsize setAttr("fontsize=%s" % fontsize) + #setAttr("height=\"0.1\"",NODE) #setAttr("width=\"1.0\"",NODE) #setAttr("margin=\"0.3,0.03\"",NODE) @@ -188,25 +209,29 @@ class AttackThread(threading.Thread): (fd2,fpname2) = Tempfile.tempcleaned(ext) f = os.fdopen(fd2,'w') - cmd = "dot -T%s" % (type) + cmd = "dot -T%s >%s" % (type,fpname2) # execute command cin,cout = os.popen2(cmd,'b') self.writeGraph(attack.scytherDot,cin) + cin.flush() cin.close() - - for l in cout.read(): - f.write(l) - cout.close() + f.flush() f.close() + # Print + print fpname2 + raw_input() + # if this is done, store and report attack.filetype = type attack.file = fpname2 # this is where the file name is stored + # Maybe we should remove the temporary file... TODO + #--------------------------------------------------------------------------- class VerificationWindow(wx.Dialog): @@ -344,7 +369,7 @@ class ResultWindow(wx.Frame): views += self.BuildClaim(grid,claims[index],index+1) if views > 0: - titlebar(7,"Classes",1) + titlebar(7,"Patterns",1) self.SetSizer(grid) self.Fit() @@ -480,7 +505,7 @@ class ScytherRun(object): # start the thread self.verifywin.SetCursor(wx.StockCursor(wx.CURSOR_WAIT)) - t = ScytherThread(self.spdl, self.options, self.verificationDone) + t = ScytherThread(self.spdl, self.options, self.verificationDone, self.mode) t.start() # after verification, we proceed to the callback below... diff --git a/gui/Gui/Settingswindow.py b/gui/Gui/Settingswindow.py index 78af9c5..4abc8a1 100644 --- a/gui/Gui/Settingswindow.py +++ b/gui/Gui/Settingswindow.py @@ -150,13 +150,13 @@ class SettingsWindow(wx.Panel): tstr += "--check " elif mode == "autoverify": tstr += "--auto-claims " - elif mode == "statespace": + elif mode == "characterize": tstr += "--state-space " # Anything else? if self.misc != "": tstr += " " + self.misc + " " - return tstr + return str(tstr) # turn it into a str (might have been unicode weirdness) #--------------------------------------------------------------------------- diff --git a/gui/Scyther/Claim.py b/gui/Scyther/Claim.py index 4d241be..27a3067 100644 --- a/gui/Scyther/Claim.py +++ b/gui/Scyther/Claim.py @@ -6,9 +6,9 @@ import Term def stateDescription(okay,n=1,caps=False): if okay: - s = "trace class" + s = "trace pattern" if n != 1: - s += "es" + s += "s" else: s = "attack" if n != 1: diff --git a/gui/Scyther/Error.py b/gui/Scyther/Error.py index d498a35..a71a2c1 100644 --- a/gui/Scyther/Error.py +++ b/gui/Scyther/Error.py @@ -86,6 +86,6 @@ class StringListError(Error): self.obj = obj def __str__(self): - return "Got %s instead of a (list of) string." % self.obj + return "Got '%s', which is type '%s' instead of a (list of) string." % (self.obj, type(self.obj)) # vim: set ts=4 sw=4 et list lcs=tab\:>-: diff --git a/gui/Scyther/Scyther.py b/gui/Scyther/Scyther.py index 761d8b6..63a9475 100755 --- a/gui/Scyther/Scyther.py +++ b/gui/Scyther/Scyther.py @@ -68,6 +68,7 @@ def Check(): program = getScytherBackend() CheckSanity(program) + #--------------------------------------------------------------------------- def CheckSanity(program): @@ -85,6 +86,9 @@ def EnsureString(x,sep=" "): Takes a thing that is either a list or a string. Turns it into a string. If it was a list, is inserted, and the process iterats. + + TODO does not accept unicode yet, that is something that must be + handled to or we run into wxPython problems eventually. """ if type(x) is str: return x @@ -362,4 +366,29 @@ class Scyther(object): else: return "Scyther has not been run yet." +#--------------------------------------------------------------------------- + +def GetInfo(html=False): + """ + Retrieve a tuple (location,string) with information about the tool, + retrieved from the --expert --version data + """ + + program = getScytherBackend() + arg = "--expert --version" + sc = Scyther() + (output,errors) = sc.doScytherCommand(spdl=None, args=arg) + if not html: + return (program,output) + else: + sep = "
\n" + html = "Backend: %s%s" % (program,sep) + for l in output.splitlines(): + l.strip() + html += "%s%s" % (l,sep) + return html + + +#--------------------------------------------------------------------------- + # vim: set ts=4 sw=4 et list lcs=tab\:>-: diff --git a/src/BuildUnix-Win32.cmake b/src/BuildUnix-Win32.cmake index ba4a26f..9f58fbb 100644 --- a/src/BuildUnix-Win32.cmake +++ b/src/BuildUnix-Win32.cmake @@ -5,11 +5,18 @@ ################################################################ message (STATUS "Building W32 version") + # This should work on win32 platform, but also when the compiler # is available anyway under linux set (CMAKE_C_COMPILER "i586-mingw32msvc-gcc") set (CMAKE_CXX_COMPILER "i586-mingw32msvc-g++") set (CMAKE_SHARED_LIBRARY_LINK_C_FLAGS) # to get rid of -rdynamic +# Signal for windows +set (CMAKE_C_FLAGS "-DFORWINDOWS") + +# Static where possible (i.e. only not on the APPLE) +set (CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -static") + set (scythername "scyther-w32.exe") add_executable (${scythername} ${Scyther_sources}) diff --git a/src/BuildUnix.cmake b/src/BuildUnix.cmake index 8985f42..49f6ddf 100644 --- a/src/BuildUnix.cmake +++ b/src/BuildUnix.cmake @@ -7,6 +7,10 @@ # We call it linux, because that is what de-facto is the case. message (STATUS "Building Linux version") + +# Static where possible (i.e. only not on the APPLE) +set (CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -static") + set (scythername "scyther-linux") add_executable (${scythername} ${Scyther_sources}) diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index dc4b53c..aaf8a91 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -16,6 +16,7 @@ set (Scyther_sources intruderknowledge.c knowledge.c label.c list.c main.c mgu.c prune_bounds.c prune_theorems.c role.c specialterm.c states.c switches.c symbol.c system.c tac.c + tempfile.c termlist.c termmap.c term.c timer.c type.c warshall.c xmlout.c parser.c scanner.c ) @@ -23,9 +24,6 @@ set (Scyther_sources # If we are in a debug mode we want to be strict set (CMAKE_C_FLAGS_DEBUG "${CMAKE_C_FLAGS_DEBUG} -Wall -DDEBUG") -# Usual static -set (CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -static") - # Determine version number include (SVNVersion.cmake) diff --git a/src/arachne.c b/src/arachne.c index 7b98005..79b0d6f 100644 --- a/src/arachne.c +++ b/src/arachne.c @@ -11,12 +11,8 @@ #include #include #include -#if !defined(__APPLE__) -#ifdef DEBUG -#include -#endif -#endif +#include "mymalloc.h" #include "term.h" #include "termlist.h" #include "role.h" @@ -580,13 +576,6 @@ proof_suppose_binding (Binding b) } } -//! Create a new temporary file and return the pointer. -FILE * -scyther_tempfile (void) -{ - return tmpfile (); -} - //------------------------------------------------------------------------ // Sub //------------------------------------------------------------------------ @@ -1925,11 +1914,27 @@ makeTraceClass (const System sys, Termlist varlist) termlistDelete (varlist); } +//! Determine whether to filter to a single attack +int +useAttackBuffer (void) +{ + if (switches.useAttackBuffer) + { + // it is possible + if (switches.prune != 0) + { + // it is also desired + return true; + } + } + return false; +} + //! Start attack output void attackOutputStart (void) { - if (switches.prune != 0) + if (useAttackBuffer ()) { FILE *fd; @@ -2153,20 +2158,101 @@ iterateOneBinding (void) return flag; } +//! Unfold this particular name in this way +void +iterateAgentUnfoldThis (const Term rolevar, const Term agent) +{ + Term buffer; + + buffer = rolevar->subst; + rolevar->subst = agent; + iterate (); + rolevar->subst = buffer; +} + +//! Unfold this particular name +void +iterateAgentUnfolding (const System sys, const Term rolevar) +{ + Termlist kl; + int count; + + iterateAgentUnfoldThis (rolevar, AGENT_Eve); + kl = knowledgeSet (sys->know); + count = 0; + while (kl != NULL && count < switches.agentUnfold) + { + Term t; + + t = deVar (kl->term); + if (realTermLeaf (t) && inTermlist (t->stype, TERM_Agent)) + { + if (!inTermlist (sys->untrusted, t)) + { + iterateAgentUnfoldThis (rolevar, t); + count++; + } + } + kl = kl->next; + } + termlistDelete (kl); +} + +//! Unfold names +/** + * Returns true if nothing was unfolded and the iteration must be done. + * Returns false when the iteration should not be done. + */ +int +doAgentUnfolding (const System sys) +{ + int run; + + for (run = 0; run < sys->maxruns; run++) + { + Termlist tl; + + tl = sys->runs[run].rho; + while (tl != NULL) + { + Term t; + + t = deVar (tl->term); + if (realTermVariable (t)) + { + // Hey, this role name is still a variable. + // We don't want that and so we unfold it as expected. + iterateAgentUnfolding (sys, t); + return false; + } + tl = tl->next; + } + } + return true; +} + //! Main recursive procedure for Arachne int iterate () { int flag; - flag = 1; + + // check unfolding agent names + if (switches.agentUnfold > 0) + { + if (!doAgentUnfolding (sys)) + return flag; + } + if (!prune_theorems (sys)) { if (!prune_claim_specifics (sys)) { if (!prune_bounds (sys)) { + // Go and pick a binding for iteration flag = iterateOneBinding (); } @@ -2194,11 +2280,7 @@ iterate () int iterate_buffer_attacks (void) { - if (switches.prune == 0) - { - return iterate (); - } - else + if (useAttackBuffer ()) { // We are pruning attacks, so they should go into a temporary file. /* @@ -2230,6 +2312,11 @@ iterate_buffer_attacks (void) return result; } + else + { + // No attack buffering, just output all of them + return iterate (); + } } //! Arachne single claim test @@ -2291,15 +2378,22 @@ arachneClaimTest (Claimlist cl) int m0run; m0tl = knowledgeSet (sys->know); - m0t = termlist_to_tuple (m0tl); - // eprintf("Initial intruder knowledge node for "); - // termPrint(m0t); - // eprintf("\n"); - I_M->roledef->message = m0t; - m0run = semiRunCreate (INTRUDER, I_M); - newruns++; - proof_suppose_run (m0run, 0, 1); - sys->runs[m0run].height = 1; + if (m0tl != NULL) + { + m0t = termlist_to_tuple (m0tl); + // eprintf("Initial intruder knowledge node for "); + // termPrint(m0t); + // eprintf("\n"); + I_M->roledef->message = m0t; + m0run = semiRunCreate (INTRUDER, I_M); + newruns++; + proof_suppose_run (m0run, 0, 1); + sys->runs[m0run].height = 1; + } + else + { + m0run = -1; + } { /** @@ -2311,11 +2405,14 @@ arachneClaimTest (Claimlist cl) } - // remove initial knowledge node - termDelete (m0t); - termlistDelete (m0tl); - semiRunDestroy (); - newruns--; + if (m0run != -1) + { + // remove initial knowledge node + termDelete (m0t); + termlistDelete (m0tl); + semiRunDestroy (); + newruns--; + } } // remove claiming run goals goal_remove_last (newgoals); diff --git a/src/binding.c b/src/binding.c index f5f9bb5..4ca36fb 100644 --- a/src/binding.c +++ b/src/binding.c @@ -15,9 +15,7 @@ #include "switches.h" #include "depend.h" #include "error.h" -#if !defined(__APPLE__) -#include -#endif +#include "mymalloc.h" static System sys; //!< local storage of system pointer diff --git a/src/bugs.txt b/src/bugs.txt index 0d014ba..98e77b0 100644 --- a/src/bugs.txt +++ b/src/bugs.txt @@ -1,7 +1,13 @@ --+++ Crititcal Bugs + * soph segfaults at no switch or -r4 (-r3 is okay??) using non-debug version. + * './scyther -a ../spdl/nsl3.spdl --increment-runs' segfaults. The main reason is that the Archne engine uses runs in a different way. + Maybe it is best to disable --increment rules for non-ModelChecker verification. + ---+++ Bugs + * Problem with goal bindings: instantiation of variable with a tuple might + introduce a tuple goal, which is forbidden. We must find a way to deal with this. This typically occurs in type flaw searches. * Arachne seems to trip over claims with empty prec sets. Maybe we simply should not test these. * Splice/AS does not work well because priority key search stumbles over the @@ -21,9 +27,19 @@ ---++++ ArachneEngine + * There is no good test on the correct workings of + add_goals/destruction of these. We can test this if after + termination, we have 0 goals; for this we need to store the + initially added goals as well. Furthermore, we can generate an + error when <0 goals occur. * Consider where in Arachne dependency graph is used. If this is only for pruning states, we can construct it there only. However, the base 'role defs/bindings' graph might be re-used. + * Add switch for arachne to prune encryption levels when using -m2. + * To store attacks for arachne, maybe the following is needed: + * The roles for each run + * The variable bindings for all (local) variables + * The goal bindings * Agent terms must have keylevel 0; enforce this! * Select_goal should consider, for singular variables, whether their type can be found in M_0. If so, the goal can be ignored. @@ -35,11 +51,19 @@ Note that there can be multiple solutions; for now, simply try to take the shortest one. +---++++ ModelChecker + + * For secrecy, one trusted agent and one untrusted agent suffices. + Implement this in the modelchecker. + * Implement delayed protocol compiler (on run demand only) for the modelchecker? + ---++++ Misc * Make different error codes for compilation error/ other error. This can be useful for scripts. However, it might shift some constants for the Elegast scripts. + * Rewrite termMguTerm such that it iterates and adapt all functions + using it. This is to allow for associative tupling later. * Fix constants in intruder knowledge. Auto add single one of each type, when typed expl. Add single constant when untyped. Fix this also in semantics, and add proof to establish sufficiency. @@ -78,3 +102,18 @@ * How is % notation handled in Casper? * Vernam encryption? +---++++ ConstraintLogic (and thus obsolete) + + * CLP: variables in keys must be branched: maybe even in three situations + (have key and contents, have inverse key and content, nothing) + * How should claims behave (trusted/untrusted) wrt uninstantiated + agents? Branch again? That's what is causing the nsl3-var problem. + * Constraints might be a part of a knowledge thing, because with we + might now have a number of local knowledge sets, each with their own + constraint sets. That doesn't make it easier though :( and will cause + some performance loss I suppose. Each local set has to remain + solveable as well. + * Issue: how do untrusted claims work in the context of an intruder? + Claim must be checked if it can be solved such that at least one of + the agents is trusted. + diff --git a/src/build.sh b/src/build.sh index e31ef9c..c68c94e 100755 --- a/src/build.sh +++ b/src/build.sh @@ -1,10 +1,4 @@ #!/bin/sh -# -# The big unifying build script, which builds all binaries it can on a -# given platform. -# -# Effectively, if this script is run both on Darwin and Linux systems, -# all binaries can be constructed. PLATFORM=`uname` echo $PLATFORM diff --git a/src/compiler.c b/src/compiler.c index 8cdfe2c..a50a396 100644 --- a/src/compiler.c +++ b/src/compiler.c @@ -139,8 +139,8 @@ compile (Tac tc, int maxrunsset) /* process the tac */ tacProcess (tac_root); - /* Clean up keylevels */ - symbol_fix_keylevels (); + /* Preprocess the result */ + preprocess (sys); /* cleanup */ levelDone (); @@ -562,25 +562,31 @@ claimCreate (const System sys, const Protocol protocol, const Role role, readvars = compute_read_variables (thisRole); while (claimvars != NULL) { - if (!inTermlist (readvars, claimvars->term)) + if (!inTermlist(protocol->rolenames, claimvars->term)) { - /* this claimvar does not occur in the reads? */ - /* then we should ignore it later */ - cl->alwaystrue = true; - cl->warnings = true; + /* only if it is not a role */ + if (!inTermlist (readvars, claimvars->term)) + { + /* this claimvar does not occur in the reads? */ + /* then we should ignore it later */ + cl->alwaystrue = true; + cl->warnings = true; - /* show a warning for this */ - globalError++; - eprintf ("warning: secrecy claim of role "); - termPrint (cl->rolename); - eprintf (" contains a variable "); - termPrint (claimvars->term); - eprintf - (" which is never read; therefore the claim will be true.\n"); - globalError--; + /* show a warning for this */ + globalError++; + eprintf ("warning: secrecy claim of role "); + termPrint (cl->rolename); + eprintf (" contains a variable "); + termPrint (claimvars->term); + eprintf + (" which is never read; therefore the claim will be true.\n"); + globalError--; + } } claimvars = claimvars->next; } + termlistDelete (claimvars); + termlistDelete (readvars); } return cl; } @@ -2123,6 +2129,16 @@ checkLabelMatching (const System sys) void preprocess (const System sys) { + /* + * Add default terms afterwards + */ + specialTermInitAfter (sys); + + /* + * Clean up keylevels + * */ + symbol_fix_keylevels (); + /* * init some counters */ @@ -2143,10 +2159,6 @@ preprocess (const System sys) { checkUnusedVariables (sys); } - /* - * compute hidelevels - */ - hidelevelCompute (sys); /* * Initial knowledge */ @@ -2154,6 +2166,12 @@ preprocess (const System sys) { initialIntruderKnowledge (sys); } + /* + * compute hidelevels + * + * Needs to be done *after* the initial intruder knowledge derivation. + */ + hidelevelCompute (sys); /* * Check well-formedness */ diff --git a/src/intruderknowledge.c b/src/intruderknowledge.c index b429649..7f758f7 100644 --- a/src/intruderknowledge.c +++ b/src/intruderknowledge.c @@ -20,6 +20,8 @@ addSTerm (const System sys, Term t, Termlist fromlist, Termlist tolist) eprintf (" to the initial intruder knowledge]\n"); globalError--; } + + knowledgeAddTerm (sys->know, t2); } //! Unfold the term for all possible options diff --git a/src/list.c b/src/list.c index c015546..b797ac6 100644 --- a/src/list.c +++ b/src/list.c @@ -5,12 +5,11 @@ * A doubly linked list with void* as data type. */ -#include "list.h" -#if !defined(__APPLE__) -#include -#endif #include +#include "list.h" +#include "mymalloc.h" + //! Make a node List list_create (const void *data) diff --git a/src/mgu.c b/src/mgu.c index 679db67..e73aec5 100644 --- a/src/mgu.c +++ b/src/mgu.c @@ -16,21 +16,12 @@ New version yields a termlist with substituted variables, which can later be reset to NULL. */ -//! Internal constant. If true, typed checking /** - * Analoguous to switches.match + * switches.match * 0 typed * 1 basic typeflaws * 2 all typeflaws */ -static int mgu_match = 0; - -//! Set mgu mode (basically switches.match) -void -setMguMode (const int match) -{ - mgu_match = match; -} void showSubst (Term t) @@ -90,7 +81,7 @@ goodsubst (Term tvar, Term tsubst) tbuf = tvar->subst; tvar->subst = tsubst; - res = checkTypeTerm (mgu_match, tvar); + res = checkTypeTerm (tvar); tvar->subst = tbuf; return res; diff --git a/src/mgu.h b/src/mgu.h index 42ac00e..a90abfd 100644 --- a/src/mgu.h +++ b/src/mgu.h @@ -13,7 +13,6 @@ */ #define MGUFAIL (Termlist) -1 -void setMguMode (const int mgu); Termlist termMguTerm (Term t1, Term t2); int termMguInTerm (Term t1, Term t2, int (*iterator) (Termlist)); int termMguSubTerm (Term t1, Term t2, int (*iterator) (Termlist, Termlist), diff --git a/src/problem.spdl b/src/problem.spdl index 2532860..64d754f 100644 --- a/src/problem.spdl +++ b/src/problem.spdl @@ -15,9 +15,9 @@ protocol yahalomBan(A,B,S) var na; var kab; - read_1(A,B, A,na,B,S); - send_2(B,S, B,nb, {A,na}k(B,S) ); - read_4(A,B, {A,kab,nb}k(B,S) , {nb}kab ); + read_!1(A,B, A,na,B,S); + send_!2(B,S, B,nb, {A,na}k(B,S) ); + read_!4(A,B, {A,kab,nb}k(B,S) , {nb}kab ); claim_6(B, Secret,kab); } } diff --git a/src/reindent.sh b/src/reindent.sh index 3a242b1..bd515fd 100755 --- a/src/reindent.sh +++ b/src/reindent.sh @@ -2,6 +2,4 @@ # # Indent any changed files, ending in .c or .h # -# TODO: Needs to be rewritten as svn of course is no longer used. -# svn st | grep "^[MA].*\.[ch]$"| awk '{print $2}' | xargs indent diff --git a/src/specialterm.c b/src/specialterm.c index 9f9fd78..49ee817 100644 --- a/src/specialterm.c +++ b/src/specialterm.c @@ -9,7 +9,7 @@ * Some macros */ #define langhide(x,y) x = levelConst(symbolSysConst(" _" y "_ ")) -#define langtype(x,y) x->stype = termlistAdd(x->stype,y); +#define langtype(x,y) x->stype = termlistAdd(x->stype,y) #define langcons(x,y,z) x = levelConst(symbolSysConst(y)); langtype(x,z) /* externally used: @@ -30,6 +30,12 @@ Term CLAIM_Niagree; Term CLAIM_Empty; Term CLAIM_Reachable; +Term AGENT_Alice; +Term AGENT_Bob; +Term AGENT_Charlie; +Term AGENT_Dave; +Term AGENT_Eve; + Termlist CLAIMS_dep_prec; //! Init special terms @@ -64,6 +70,25 @@ specialTermInit (const System sys) } +//! After compilation (so the user gets the first choice) +void +specialTermInitAfter (const System sys) +{ + langcons (AGENT_Alice, "Alice", TERM_Agent); + langcons (AGENT_Bob, "Bob", TERM_Agent); + langcons (AGENT_Charlie, "Charlie", TERM_Agent); + langcons (AGENT_Dave, "Dave", TERM_Agent); + langcons (AGENT_Eve, "Eve", TERM_Agent); + + knowledgeAddTerm (sys->know, AGENT_Alice); + knowledgeAddTerm (sys->know, AGENT_Bob); + knowledgeAddTerm (sys->know, AGENT_Charlie); + knowledgeAddTerm (sys->know, AGENT_Dave); + knowledgeAddTerm (sys->know, AGENT_Eve); + + sys->untrusted = termlistAddNew (sys->untrusted, AGENT_Eve); +} + //! Determine whether this is a leaf construct with a ticket in it int isTicketTerm (Term t) diff --git a/src/specialterm.h b/src/specialterm.h index 592fad4..b58f923 100644 --- a/src/specialterm.h +++ b/src/specialterm.h @@ -24,9 +24,16 @@ extern Term CLAIM_Niagree; extern Term CLAIM_Empty; extern Term CLAIM_Reachable; +extern Term AGENT_Alice; +extern Term AGENT_Bob; +extern Term AGENT_Charlie; +extern Term AGENT_Dave; +extern Term AGENT_Eve; + extern Termlist CLAIMS_dep_prec; void specialTermInit (const System sys); +void specialTermInitAfter (const System sys); int isTicketTerm (Term t); int hasTicketSubterm (Term t); diff --git a/src/system.c b/src/system.c index 732e2ba..9483d21 100644 --- a/src/system.c +++ b/src/system.c @@ -108,10 +108,6 @@ systemReset (const System sys) /* transfer switches */ sys->maxtracelength = switches.maxtracelength; - - /* propagate mgu_mode */ - - setMguMode (switches.match); } //! Initialize runtime system (according to cut traces, limited runs) @@ -555,6 +551,7 @@ roleInstanceArachne (const System sys, const Protocol protocol, } } + //! The next function makes locals for all in the list. Flags denote whether it is a variable or role. void createLocals (Termlist list, int isvariable, int isrole) { while (list != NULL) diff --git a/src/term.h b/src/term.h index c1a763d..a10c097 100644 --- a/src/term.h +++ b/src/term.h @@ -2,9 +2,7 @@ #define TERMS #include "symbol.h" - -#define false 0 -#define true 1 +#include "bool.h" // type <= LEAF means it's a leaf, nkay? enum termtypes diff --git a/src/termlist.c b/src/termlist.c index dd748b3..dc8d37f 100644 --- a/src/termlist.c +++ b/src/termlist.c @@ -4,6 +4,7 @@ #include "specialterm.h" #include "debug.h" #include "error.h" +#include "switches.h" /* * Shared stuff @@ -746,20 +747,19 @@ termlistContained (const Termlist tlbig, Termlist tlsmall) /** * Determine whether a variable has been substituted with something with * the right type. - *@param matchmode The system matching mode, typically system::match *@param term The closed variable term. *@return True iff the substitution is valid in the current mode. *\sa system::match */ int -validSubst (const int matchmode, const Term term) +validSubst (const Term term) { if (!realTermVariable (term) || term->subst == NULL) return 1; else { - switch (matchmode) + switch (switches.match) { case 0: /* real type match */ return realTermLeaf (term->subst) diff --git a/src/termlist.h b/src/termlist.h index 491da0e..5874808 100644 --- a/src/termlist.h +++ b/src/termlist.h @@ -52,7 +52,6 @@ Term termLocal (const Term t, Termlist fromlist, Termlist tolist); Termlist termlistLocal (Termlist tl, const Termlist fromlist, const Termlist tolist); int termlistContained (const Termlist tlbig, Termlist tlsmall); -int validSubst (const int matchmode, const Term term); Term termFunction (Termlist fromlist, Termlist tolist, Term tx); Termlist termlistForward (Termlist tl); int termlistOrder (Termlist tl1, Termlist tl2); diff --git a/src/todo.txt b/src/todo.txt index 5b18085..595b7c1 100644 --- a/src/todo.txt +++ b/src/todo.txt @@ -1,5 +1,6 @@ -- Version number should be retrieved from git now (as opposed to - subversion, so it should give the sha1 thing, and possibly a tag). +- When saving a file after 'file changed' warning, an overwrite of the + same file should not necessarily generate a warning. +- Output (claim summary) might have a parameter summary somewhere. - Error should have an additional line number parameter (that might be -1 to ignore it) forcing people to use numbers :) Format: "error: [%i] %s\n" diff --git a/src/type.c b/src/type.c index c9f1274..fca191a 100644 --- a/src/type.c +++ b/src/type.c @@ -66,10 +66,10 @@ isTypelistGeneric (const Termlist typelist) * Non-variables etc. imply true. */ int -checkTypeTerm (const int mgumode, const Term tvar) +checkTypeTerm (const Term tvar) { - // Checks are only needed for mgumode < 2 etc. - if (mgumode < 2 && tvar != NULL && realTermVariable (tvar)) + // Checks are only needed for match < 2 etc. + if (switches.match < 2 && tvar != NULL && realTermVariable (tvar)) { // Non-instantiated terms are fine. if (tvar->subst != NULL) @@ -90,7 +90,7 @@ checkTypeTerm (const int mgumode, const Term tvar) else { // It is a leaf - if (mgumode == 0) + if (switches.match == 0) { /* Types must match exactly. Thus, one of the variable type should match a type of the constant. */ @@ -122,11 +122,11 @@ checkTypeTerm (const int mgumode, const Term tvar) * Empty list implies true. */ int -checkTypeTermlist (const int mgumode, Termlist tl) +checkTypeTermlist (Termlist tl) { while (tl != NULL) { - if (!checkTypeTerm (mgumode, tl->term)) + if (!checkTypeTerm (tl->term)) return false; tl = tl->next; } @@ -144,7 +144,7 @@ checkTypeLocals (const System sys) { if (sys->runs[run].protocol != INTRUDER) { - if (!checkTypeTermlist (switches.match, sys->runs[run].locals)) + if (!checkTypeTermlist (sys->runs[run].locals)) return false; } run++; @@ -178,14 +178,13 @@ agentCompatible (Termlist tl) /** * Depends on some input: * - * mgumode type of matching * agentcheck true if agent type is always restrictive * * returns the new type list (needs to be deleted!) or TERMLISTERROR (should * not be deleted!) */ Termlist -typelistConjunct (Termlist typelist1, Termlist typelist2, const int mgumode, +typelistConjunct (Termlist typelist1, Termlist typelist2, const int agentcheck) { if (typelist1 != TERMLISTERROR && typelist2 != TERMLISTERROR) @@ -202,25 +201,25 @@ typelistConjunct (Termlist typelist1, Termlist typelist2, const int mgumode, /* Now, the result must surely accept agents. Thus, it must be * NULL or accept agents. */ - - if (! - (agentCompatible (typelist1) - && agentCompatible (typelist2))) + if (switches.match == 0) { - // Not good: one of them cannot - return TERMLISTERROR; - } - else - { - // Good: but because an agent is involved, the type reduces to the simple Agent type only. - return termlistAdd (NULL, TERM_Agent); + // only if we are doing matching, otherwise it is always agent-compatible + if (! + (agentCompatible (typelist1) + && agentCompatible (typelist2))) + { + // Not good: one of them cannot + return TERMLISTERROR; + } } + // Good: but because an agent is involved, the type reduces to the simple Agent type only. + return termlistAdd (NULL, TERM_Agent); } else { /* Not the simple agent variable case. Now other things come in to play. */ - if (mgumode == 0) + if (switches.match == 0) { /* * Strict match: (-m0) conjunct of the types must be non-empty. @@ -287,48 +286,51 @@ checkGroundVariable (const System sys, const Term groundvar) int allvalid; allvalid = 1; - if (realTermVariable (groundvar)) + if (switches.match < 2) { - Termlist tl; - Termlist typelist; - - // Check - typelist = termlistShallow (groundvar->stype); - tl = sys->variables; - while (allvalid == 1 && tl != NULL) + if (realTermVariable (groundvar)) { - Term term; + Termlist tl; + Termlist typelist; - term = tl->term; - - // Not actually the same, of course - if (term != groundvar) + // Check + typelist = termlistShallow (groundvar->stype); + tl = sys->variables; + while (allvalid == 1 && tl != NULL) { - // Does this term map to the same variable? - if (isTermEqual (term, groundvar)) + Term term; + + term = tl->term; + + // Not actually the same, of course + if (term != groundvar) { - Termlist tlprev; - - // Maps to same ground term - // Take conjunct - tlprev = typelist; - typelist = - typelistConjunct (tlprev, term->stype, switches.match, - switches.agentTypecheck); - termlistDelete (tlprev); - - if (typelist == TERMLISTERROR) + // Does this term map to the same variable? + if (isTermEqual (term, groundvar)) { - // And this is not valid... - allvalid = 0; + Termlist tlprev; + + // Maps to same ground term + // Take conjunct + tlprev = typelist; + typelist = + typelistConjunct (tlprev, term->stype, + switches.agentTypecheck); + termlistDelete (tlprev); + + if (typelist == TERMLISTERROR) + { + // And this is not valid... + allvalid = 0; + } } } + tl = tl->next; + } + if (typelist != TERMLISTERROR) + { + termlistDelete (typelist); } - tl = tl->next; - } - if (typelist != TERMLISTERROR) - { - termlistDelete (typelist); } } return allvalid; @@ -408,8 +410,7 @@ checkAllSubstitutions (const System sys) else { // Consider match - allvalid = allvalid - && checkTypeTerm (switches.match, tvar); + allvalid = allvalid && checkTypeTerm (tvar); } } } diff --git a/src/type.h b/src/type.h index 88ee607..acfa915 100644 --- a/src/type.h +++ b/src/type.h @@ -4,8 +4,8 @@ #include "term.h" #include "system.h" -int checkTypeTerm (const int mgumode, const Term t); -int checkTypeTermlist (const int mgumode, Termlist tl); +int checkTypeTerm (const Term t); +int checkTypeTermlist (Termlist tl); int checkTypeLocals (const System sys); Termlist typelistConjunct (Termlist typelist1, Termlist Typelist2); int checkAllSubstitutions (const System sys); diff --git a/src/warshall.h b/src/warshall.h index 5920a89..d935030 100644 --- a/src/warshall.h +++ b/src/warshall.h @@ -8,6 +8,8 @@ #include #include +#include "mymalloc.h" + /* machine-dependent definitions */ /* the following definitions are for the Tahoe */ /* they might have to be changed for other machines */ diff --git a/src/xmlout.c b/src/xmlout.c index b585cda..bb725cf 100644 --- a/src/xmlout.c +++ b/src/xmlout.c @@ -317,7 +317,9 @@ xmlVariable (const System sys, const Term variable, const int run) { xmlIndentPrint (); eprintf ("