andr3/scyther
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

- Big catchup commit to make sure we are up to beta7.

Browse Source 
This includes a number of single patches, ranging from the vista fix with the buffers, to the start of many new minor features.
This commit is contained in:
Cas Cremers 2007-05-18 14:06:29 +02:00
parent 5882548643
commit 1542d65def
35 changed files with 538 additions and 204 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
gui/.gitignore vendored Normal file
View File

@ -0,0 +1 @@
*.pyc

23
gui/Gui/About.py
View File

@ -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):
<body bgcolor="#ffffff">
<img src="$SPLASH">
<p align="right"><b>Scyther : $VERSION</b></p>
<small>
<p>
<b>Scyther</b> is an automatic tool for the verification and
falsification of security protocols.
@ -42,21 +53,31 @@ class AboutScyther(wx.Dialog):
<a target="_blank" href="http://people.inf.ethz.ch/cremersc/scyther/index.html">
http://people.inf.ethz.ch/cremersc/scyther/index.html</a>
</p>
<p>
$DETAILS
</p>
<p>
Credits: Cas Cremers (Scyther theory, backend, and main GUI
code), Gijs Hollestelle (Python parser for Scyther XML output).
</p>
</small>
'''
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<br>\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))

1
gui/Gui/Attackwindow.py
View File

@ -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

25
gui/Gui/Editor.py
View File

@ -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):

90
gui/Gui/Mainwindow.py
View File

@ -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")

69
gui/Gui/Scytherthread.py
View File

@ -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...

4
gui/Gui/Settingswindow.py
View File

@ -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)
#---------------------------------------------------------------------------

4
gui/Scyther/Claim.py
View File

@ -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:

2
gui/Scyther/Error.py
View File

@ -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\:>-:

29
gui/Scyther/Scyther.py
View File

@ -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, <sep> 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 = "<br>\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\:>-:

7
src/BuildUnix-Win32.cmake
View File

@ -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})

4
src/BuildUnix.cmake
View File

@ -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})

4
src/CMakeLists.txt
View File

@ -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)

163
src/arachne.c
View File

@ -11,12 +11,8 @@
#include <limits.h>
#include <float.h>
#include <string.h>
#if !defined(__APPLE__)
#ifdef DEBUG
#include <malloc.h>
#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);

4
src/binding.c
View File

@ -15,9 +15,7 @@
#include "switches.h"
#include "depend.h"
#include "error.h"
#if !defined(__APPLE__)
#include <malloc.h>
#endif
#include "mymalloc.h"
static System sys; //!< local storage of system pointer

39
src/bugs.txt
View File

@ -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.

6
src/build.sh
View File

@ -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

58
src/compiler.c
View File

@ -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
*/

2
src/intruderknowledge.c
View File

@ -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

7
src/list.c
View File

@ -5,12 +5,11 @@
* A doubly linked list with void* as data type.
*/
#include "list.h"
#if !defined(__APPLE__)
#include <malloc.h>
#endif
#include <stdlib.h>
#include "list.h"
#include "mymalloc.h"
//! Make a node
List
list_create (const void *data)

13
src/mgu.c
View File

@ -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;

1
src/mgu.h
View File

@ -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),

6
src/problem.spdl
View File

@ -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);
}
}

2
src/reindent.sh
View File

@ -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

27
src/specialterm.c
View File

@ -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)

7
src/specialterm.h
View File

@ -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);

5
src/system.c
View File

@ -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)

4
src/term.h
View File

@ -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

6
src/termlist.c
View File

@ -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)

1
src/termlist.h
View File

@ -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);

5
src/todo.txt
View File

@ -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"

113
src/type.c
View File

@ -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);
}
}
}

4
src/type.h
View File

@ -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);

2
src/warshall.h
View File

@ -8,6 +8,8 @@
#include <stdio.h>
#include <stdlib.h>
#include "mymalloc.h"
/* machine-dependent definitions */
/* the following definitions are for the Tahoe */
/* they might have to be changed for other machines */

4
src/xmlout.c
View File

@ -317,7 +317,9 @@ xmlVariable (const System sys, const Term variable, const int run)
{
xmlIndentPrint ();
eprintf ("<variable typeflaw=\"");
if (!checkTypeTerm (0, variable))
/* TODO this is now wrong, because it does not switch the matching more
* anymore */
if (!checkTypeTerm (variable))
{
eprintf ("true");
}