Merge branch 'stable' of ssh://cas@roivas.shape9.nl/export/git/scyther-develop/

Conflicts:

	gui/Gui/Scytherthread.py
This commit is contained in:
Cas Cremers 2007-05-19 23:38:10 +02:00
commit 173b1e8d41
163 changed files with 246 additions and 26310 deletions

66
dist/gitdist.sh vendored Executable file
View File

@ -0,0 +1,66 @@
#!/bin/sh
#
# Make a new distribution archive. Command line specification of the tag
#
# For now, just windows. Others will follow.
#
# Usage will be:
#
# gitdist ARCH TAG
#
ARCH=w32
TAG="v1.0-beta7.1"
DOCDIR=doc/manual
MANUAL=scyther-manual.pdf
DNAM="scyther-$TAG"
TMPDIR="/tmp"
RESDIR="$TMPDIR/$DNAM"
rm -rf $RESDIR
ZIPDIR=$TMPDIR
ZIPNAME=scyther-$ARCH-$TAG.zip
rm -f $ZIPDIR/$ZIPNAME
cd .. && git-archive --format=tar --prefix=$DNAM/ $TAG | (cd $TMPDIR && tar xf -)
ls $RESDIR
# Windows binary
cd $RESDIR/src
# Where is stuff going to
DESTDIR=$RESDIR/gui
# Prepare version.h with the correct flag (tag)
echo "#define SVNVERSION \"Unknown\"" >$RESDIR/src/version.h
echo "#define TAGVERSION \"$TAG\"" >>$RESDIR/src/version.h
echo "" >>$RESDIR/src/version.h
# Manual
cp $RESDIR/$DOCDIR/$MANUAL $DESTDIR
# Default flags
CMFLAGS="-D CMAKE_BUILD_TYPE:STRING=Release"
# Make for windows and linux
cmake $CMFLAGS -D TARGETOS=Win32 . && make
#cmake $CMFLAGS . && make
BINDIR=$RESDIR/gui/Scyther/Bin
mkdir $BINDIR
cp scyther-w32.exe $BINDIR
# Prepare tag for gui version
echo "SCYTHER_GUI_VERSION = \"$TAG\"" >$DESTDIR/Gui/Version.py
# Make archive out of the result
WORKNAME="scyther-$TAG"
cd $RESDIR
mv gui $WORKNAME
zip -r $ZIPDIR/$ZIPNAME $WORKNAME
rm -rf $RESDIR

View File

@ -1,54 +1,60 @@
---------------------
- Scyther changelog -
---------------------
Scyther 1.0-beta7
Bugfixes:
* Windows Vista causes a number of problems. The biggest problem
is now fixed, which is the bad implementation of the tmpfile() C
function, causing no attack output, for which there is a
workaround now.
Scyther 1.0-beta6
Big new features:
* [Gui] Added Mac support (added universal binary)
* [Gui] Switched to Scintilla editor component, providing undo
and line numbering, and highlighting of error lines.
Other new features:
* [Backend] Scyther now detects when a read event cannot match
with a send event. This significantly helps in reducing errors
in the protocol descriptions.
* [Language] Added claim parameter for Reachable claim;
Reachable,R means that role R should be trusted (as well as the
actor), but not any other role. This can be useful for showing
stronger authentication properties of protocols with more than
two parties.
* [Backend] Added '--max-of-role=N' switch (to narrow scenarios)
* [Backend] Added '--scan-claims' switch (allows for retrieving
a list of claims)
* [Scripting] Added 'verifyOne' and 'scanClaims' methods to
Scyther object, to help with singular claim testing.
Bugfixes:
* [Scripting] Fixed bug in python interface backend (e.g. with mpa.py)
Scyther 1.0-beta5
* Change of switch semantics. '--max-attacks=N' now defines the
maximum number of attacks per claim. Previously this was a
global maximum for all claims combined.
* Improved attack graph output.
* added switch '--errors=FILE' to redirect standard error output
to a file.
* Rewrote parts of the gui code for improved stability.
Scyther 1.0-beta4
* (Changelog starts after the release of Scyther 1.0-beta4)
---------------------
- Scyther changelog -
---------------------
Scyther 1.0-beta7.1
Bugfixes:
* Windows Vista fix broke Windows XP support.
Scyther 1.0-beta7
Bugfixes:
* Windows Vista causes a number of problems. The biggest problem
is now fixed, which is the bad implementation of the tmpfile() C
function, causing no attack output, for which there is a
workaround now.
Scyther 1.0-beta6
Big new features:
* [Gui] Added Mac support (added universal binary)
* [Gui] Switched to Scintilla editor component, providing undo
and line numbering, and highlighting of error lines.
Other new features:
* [Backend] Scyther now detects when a read event cannot match
with a send event. This significantly helps in reducing errors
in the protocol descriptions.
* [Language] Added claim parameter for Reachable claim;
Reachable,R means that role R should be trusted (as well as the
actor), but not any other role. This can be useful for showing
stronger authentication properties of protocols with more than
two parties.
* [Backend] Added '--max-of-role=N' switch (to narrow scenarios)
* [Backend] Added '--scan-claims' switch (allows for retrieving
a list of claims)
* [Scripting] Added 'verifyOne' and 'scanClaims' methods to
Scyther object, to help with singular claim testing.
Bugfixes:
* [Scripting] Fixed bug in python interface backend (e.g. with mpa.py)
Scyther 1.0-beta5
* Change of switch semantics. '--max-attacks=N' now defines the
maximum number of attacks per claim. Previously this was a
global maximum for all claims combined.
* Improved attack graph output.
* added switch '--errors=FILE' to redirect standard error output
to a file.
* Rewrote parts of the gui code for improved stability.
Scyther 1.0-beta4
* (Changelog starts after the release of Scyther 1.0-beta4)

View File

@ -15,6 +15,7 @@ import StringIO
""" Import scyther components """
import Scyther.Scyther
import Scyther.Error
from Scyther.Misc import *
""" Import scyther-gui components """
import Tempfile
@ -153,6 +154,15 @@ class AttackThread(threading.Thread):
return
graphLine("%s [%s]" % (edge,atxt))
if sys.platform.startswith("darwin"):
self.fontname = "Helvetica"
elif sys.platform.startswith("win"):
self.fontname = "Courier"
else:
#font = wx.Font(9,wx.SWISS,wx.NORMAL,wx.NORMAL)
#self.fontname = font.GetFaceName()
self.fontname = "\"Helvetica\""
# write all graph lines but add layout modifiers
for l in txt.splitlines():
fp.write(l)
@ -165,20 +175,19 @@ 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
if self.fontname:
fontstring = "fontname=%s" % (self.fontname)
setAttr(fontstring)
# 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)
@ -188,6 +197,7 @@ class AttackThread(threading.Thread):
def makeImage(self,attack):
""" create image for this particular attack """
if Preference.usePIL():
# If we have the PIL library, we can do postscript! great
# stuff.
@ -201,21 +211,17 @@ class AttackThread(threading.Thread):
# command to write to temporary file
(fd2,fpname2) = Tempfile.tempcleaned(ext)
f = os.fdopen(fd2,'w')
(fd3,fpname3) = Tempfile.tempcleaned(ext)
dotfile = os.fdopen(fd3,'w')
self.writeGraph(attack.scytherDot,dotfile)
dotfile.flush()
dotfile.seek(0)
cmd = "dot -T%s" % (type)
cmd = "dot -T%s -o%s %s" % (type,fpname2,fpname3)
# execute command
cin,cout = os.popen2(cmd,'b')
self.writeGraph(attack.scytherDot,cin)
cin.close()
for l in cout.read():
f.write(l)
cout.close()
f.flush()
f.close()
# Start the process
safeCommand(cmd)
# if this is done, store and report
attack.filetype = type

View File

@ -2,15 +2,9 @@
Scyther
1.0-beta5
an automatic verification tool for security protocols
by Cas Cremers
Microsoft Windows binary
and
Linux binary (compiled for Linux i686 environments)
------------------------------------------------------------------------
@ -35,7 +29,7 @@ Start the graphical user interface by starting
Some protocol description files (with extension .spdl) can be found in
the base directory. Many other protocol input files can be found in the
SPORE directory.
'Protocols' directory.
3. Citing Scyther

Binary file not shown.

Binary file not shown.

Binary file not shown.

View File

@ -5,7 +5,14 @@
#---------------------------------------------------------------------------
""" Import externals """
import sys
import os.path
try:
from subprocess import Popen
AvailablePopen = True
except:
import os
AvailablePopen = False
#---------------------------------------------------------------------------
@ -43,3 +50,21 @@ def mypath(file):
basedir = os.path.dirname(__file__)
return os.path.join(basedir,file)
def safeCommand(cmd):
""" Execute a command with some arguments. Safe cross-platform
version, I hope. """
global AvailablePopen
if AvailablePopen:
if sys.platform.startswith("win"):
shell=False
else:
shell=True
p = Popen(cmd, shell=shell)
sts = p.wait()
else:
sts = os.system(cmd)
return sts

View File

@ -12,6 +12,7 @@ import sys
import StringIO
import tempfile
#---------------------------------------------------------------------------
""" Import scyther components """
@ -226,7 +227,7 @@ class Scyther(object):
##print self.cmd
# Start the process
os.system(self.cmd)
safeCommand(self.cmd)
# reseek
fhe = os.fdopen(fde)

View File

@ -1,54 +1,3 @@
/*
* 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);
/*
* Needham-Schroeder-Lowe protocol
*/
@ -68,7 +17,7 @@ protocol nsl3(I,R)
const ni: Nonce;
var nr: Nonce;
send_1(I,R, {I,ni}pk(R) );
send_1(I,R, {ni,I}pk(R) );
read_2(R,I, {ni,nr,R}pk(I) );
send_3(I,R, {nr}pk(R) );
@ -83,7 +32,59 @@ protocol nsl3(I,R)
var ni: Nonce;
const nr: Nonce;
read_1(I,R, {I,ni}pk(R) );
read_1(I,R, {ni,I}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);
/*
* Needham-Schroeder-Lowe protocol,
* broken version (wrong role name in first message)
*/
// PKI infrastructure
const pk: Function;
secret sk: Function;
inversekeys (pk,sk);
// The protocol description
protocol nsl3-broken(I,R)
{
role I
{
const ni: Nonce;
var nr: Nonce;
send_1(I,R, {ni,R}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, {ni,R}pk(R) );
send_2(R,I, {ni,nr,R}pk(I) );
read_3(I,R, {nr}pk(R) );

View File

@ -17,7 +17,7 @@ protocol ns3(I,R)
const ni: Nonce;
var nr: Nonce;
send_1(I,R, {I,ni}pk(R) );
send_1(I,R, {ni,I}pk(R) );
read_2(R,I, {ni,nr}pk(I) );
send_3(I,R, {nr}pk(R) );
@ -32,7 +32,7 @@ protocol ns3(I,R)
var ni: Nonce;
const nr: Nonce;
read_1(I,R, {I,ni}pk(R) );
read_1(I,R, {ni,I}pk(R) );
send_2(R,I, {ni,nr}pk(I) );
read_3(I,R, {nr}pk(R) );

View File

@ -18,7 +18,7 @@ protocol nsl3-broken(I,R)
const ni: Nonce;
var nr: Nonce;
send_1(I,R, {R,ni}pk(R) );
send_1(I,R, {ni,R}pk(R) );
read_2(R,I, {ni,nr,R}pk(I) );
send_3(I,R, {nr}pk(R) );
@ -33,7 +33,7 @@ protocol nsl3-broken(I,R)
var ni: Nonce;
const nr: Nonce;
read_1(I,R, {R,ni}pk(R) );
read_1(I,R, {ni,R}pk(R) );
send_2(R,I, {ni,nr,R}pk(I) );
read_3(I,R, {nr}pk(R) );

View File

@ -17,7 +17,7 @@ protocol nsl3(I,R)
const ni: Nonce;
var nr: Nonce;
send_1(I,R, {I,ni}pk(R) );
send_1(I,R, {ni,I}pk(R) );
read_2(R,I, {ni,nr,R}pk(I) );
send_3(I,R, {nr}pk(R) );
@ -32,7 +32,7 @@ protocol nsl3(I,R)
var ni: Nonce;
const nr: Nonce;
read_1(I,R, {I,ni}pk(R) );
read_1(I,R, {ni,I}pk(R) );
send_2(R,I, {ni,nr,R}pk(I) );
read_3(I,R, {nr}pk(R) );

View File

@ -1,8 +0,0 @@
################################################################
# Name: BuildMacIntel-MacPPC.cmake
# Purpose: Build MacPPC binary on MacIntel
# Author: Cas Cremers
################################################################
include (BuildMacPPC.cmake)

View File

@ -1,11 +0,0 @@
################################################################
# Name: BuildMacIntel.cmake
# Purpose: Build MacIntel binary
# Author: Cas Cremers
################################################################
message (STATUS "Building Apple Mac Intel version")
set (scythername "scyther-macintel")
add_executable (${scythername} ${Scyther_sources})
set (CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -fnested-functions -arch i386")

View File

@ -1,8 +0,0 @@
################################################################
# Name: BuildMacPPC-MacIntel.cmake
# Purpose: Build MacIntel binary on MacPPC
# Author: Cas Cremers
################################################################
include (BuildMacIntel.cmake)

View File

@ -1,11 +0,0 @@
################################################################
# Name: BuildMacPPC.cmake
# Purpose: Build MacPPC binary
# Author: Cas Cremers
################################################################
message (STATUS "Building Apple Mac PPC version")
set (scythername "scyther-macppc")
add_executable (${scythername} ${Scyther_sources})
set (CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -fnested-functions -arch ppc")

View File

@ -1,36 +0,0 @@
################################################################
# Name: BuildPlatform.cmake
# Purpose: Make platform-dependant decisions
# Author: Cas Cremers
################################################################
# Add target for Universal Binary when needed
if (APPLE)
include (UniversalBinary.cmake)
endif (APPLE)
# Retrieve Source_OS, Destination_OS (from -DTARGET)
include (GetOS.cmake)
# From source_os and destination_os make a new name for the build script
if (Source_OS STREQUAL Destination_OS)
set (BuildScriptName "Build${Source_OS}.cmake")
else (Source_OS STREQUAL Destination_OS)
set (BuildScriptName "Build${Source_OS}-${Destination_OS}.cmake")
endif (Source_OS STREQUAL Destination_OS)
message (STATUS "Locating platform specific file ${BuildScriptName}")
# Locate the file. If it exists, start it
if (EXISTS ${BuildScriptName})
# Execute the build script
include (${BuildScriptName})
else (EXISTS ${BuildScriptName})
# Could not find it!
message (STATUS "Could not find ${BuildScriptName}")
if (Source_OS STREQUAL Destination_OS)
message (FATAL_ERROR "Don't know how to build on ${Source_OS}")
else (Source_OS STREQUAL Destination_OS)
message (FATAL_ERROR "Don't know how to build for ${Destination_OS} on ${Source_OS}")
endif (Source_OS STREQUAL Destination_OS)
endif (EXISTS ${BuildScriptName})

View File

@ -1,15 +0,0 @@
################################################################
# Name: BuildUnix-Win32.cmake
# Purpose: Build Win32 binary on Unix
# Author: Cas Cremers
################################################################
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
set (scythername "scyther-w32.exe")
add_executable (${scythername} ${Scyther_sources})

View File

@ -1,12 +0,0 @@
################################################################
# Name: BuildUnix.cmake
# Purpose: Build Unix binary on self
# Author: Cas Cremers
################################################################
# We call it linux, because that is what de-facto is the case.
message (STATUS "Building Linux version")
set (scythername "scyther-linux")
add_executable (${scythername} ${Scyther_sources})

View File

@ -1,37 +0,0 @@
################################################################
# Name: CMakeLists.txt
# Purpose: Input file for CMake for the Scyther tool
# Author: Cas Cremers
################################################################
# Scyther project
project (Scyther)
# I need 2.4 for flex/etc although it does not run yet
CMAKE_MINIMUM_REQUIRED(VERSION 2.4)
# List all the source files
set (Scyther_sources
arachne.c binding.c claim.c color.c compiler.c cost.c
debug.c depend.c dotout.c error.c heuristic.c hidelevel.c
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
termlist.c termmap.c term.c timer.c type.c warshall.c xmlout.c
parser.c scanner.c
)
# 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)
# Make scanner and parser
include (ScannerParser.cmake)
# Set build target settings according to platform
include (BuildPlatform.cmake)

View File

@ -1,33 +0,0 @@
# - Try to find Bison
# Once done this will define
#
# BISON_FOUND - system has Bison
# BISON_EXECUTABLE - path of the bison executable
# BISON_VERSION - the version string, like "2.5.31"
#
FIND_PROGRAM(BISON_EXECUTABLE NAMES bison)
mark_as_advanced(BISON_DIR Bison_DIR)
#INCLUDE(MacroEnsureVersion)
IF(BISON_EXECUTABLE)
SET(BISON_FOUND TRUE)
EXECUTE_PROCESS(COMMAND ${BISON_EXECUTABLE} --version
OUTPUT_VARIABLE _BISON_VERSION
)
string (REGEX MATCH "[0-9]+\\.[0-9]+\\.[0-9]+" BISON_VERSION "${_bison_VERSION}")
ENDIF(BISON_EXECUTABLE)
IF(BISON_FOUND)
IF(NOT Bison_FIND_QUIETLY)
MESSAGE(STATUS "Found Bison: ${BISON_EXECUTABLE}")
ENDIF(NOT Bison_FIND_QUIETLY)
ELSE(BISON_FOUND)
IF(Bison_FIND_REQUIRED)
MESSAGE(FATAL_ERROR "Could not find Bison")
ENDIF(Bison_FIND_REQUIRED)
ENDIF(BISON_FOUND)

View File

@ -1,33 +0,0 @@
# - Try to find Flex
# Once done this will define
#
# FLEX_FOUND - system has Flex
# FLEX_EXECUTABLE - path of the flex executable
# FLEX_VERSION - the version string, like "2.5.31"
#
FIND_PROGRAM(FLEX_EXECUTABLE NAMES flex)
mark_as_advanced(FLEX_DIR Flex_DIR)
#INCLUDE(MacroEnsureVersion)
IF(FLEX_EXECUTABLE)
SET(FLEX_FOUND TRUE)
EXECUTE_PROCESS(COMMAND ${FLEX_EXECUTABLE} --version
OUTPUT_VARIABLE _FLEX_VERSION
)
string (REGEX MATCH "[0-9]+\\.[0-9]+\\.[0-9]+" FLEX_VERSION "${_FLEX_VERSION}")
ENDIF(FLEX_EXECUTABLE)
IF(FLEX_FOUND)
IF(NOT Flex_FIND_QUIETLY)
MESSAGE(STATUS "Found Flex: ${FLEX_EXECUTABLE}")
ENDIF(NOT Flex_FIND_QUIETLY)
ELSE(FLEX_FOUND)
IF(Flex_FIND_REQUIRED)
MESSAGE(FATAL_ERROR "Could not find Flex")
ENDIF(Flex_FIND_REQUIRED)
ENDIF(FLEX_FOUND)

View File

@ -1,43 +0,0 @@
################################################################
# Name: GetOS.cmake
# Purpose: Determine Source_OS and Destination_OS (-DTARGETOS)
# Author: Cas Cremers
################################################################
# Supported types:
#
# Win32
# Unix
# MacPPC
# MacIntel
# First we find out the current operating system
set (Source_OS)
if (WIN32)
# Windows
set (Source_OS "Win32")
else (WIN32)
# Not windows, is it a mac?
if (APPLE)
# TODO: A mac, but what architecture?
# For now we assume intel (Christoph Sprenger's machine)
set (Source_OS "MacIntel")
else (APPLE)
# Not a mac, not windows
if (UNIX)
set (Source_OS "Unix")
else (UNIX)
message (FATAL "Unrecognized source platform.")
endif (UNIX)
endif (APPLE)
endif (WIN32)
#message (STATUS "Source platform: ${Source_OS}")
# Destination? If target is unset, we just take the source
if (TARGETOS)
set (Destination_OS "${TARGETOS}")
else (TARGETOS)
set (Destination_OS "${Source_OS}")
endif (TARGETOS)
#message (STATUS "Destination platform: ${Destination_OS}")

View File

@ -1,86 +0,0 @@
#
# Scyther Makefile
#
#
# DEBUG or optimization settings: uncomment a single line:
#
CFLAGS = -g3 -D DEBUG # default usage, for e.g. with valgrind
#CFLAGS = -g3 -D DEBUG -pg # for code profiling with gprof
#CFLAGS = -O3 -static -finline-functions -fomit-frame-pointer
#
# Compiler and linkage
#
CC = gcc
# Note that these paths must include the path to the argtable library.
CPPFLAGS = -I/scratch/ccremers/include -I/usr/local/include -Wall
LDFLAGS = -L/scratch/ccremers/lib -L/usr/local/lib
LOADLIBS = -lfl
LDLIBS = -largtable2
OPTIONS = ${CPPFLAGS} ${CFLAGS} ${LDFLAGS}
#
# Module set for the modelchecker
#
MODULES=memory.o terms.o termlists.o symbols.o knowledge.o runs.o modelchecker.o \
report.o debug.o mgu.o substitutions.o \
match_basic.o \
match_clp.o constraints.o \
output.o latex.o \
varbuf.o tracebuf.o attackminimize.o \
tac.o parser.o compiler.o
#
# Dependencies
#
MODELCHECKER = ${MODULES} main.o
all: scyther tags
${Target}.o: ${Target}.c
$(CC) $(OPTIONS) ${Target}.c -c
scanner.c: scanner.lex
flex scanner.lex
cp lex.yy.c scanner.c
tok.h: parser.c
parser.c: parser.y
bison -d -v parser.y
cp parser.tab.c parser.c
cmp -s parser.tab.h tok.h || cp parser.tab.h tok.h
tags: *.c *.h
ctags *.c *.h
modules: $(MODULES)
scyther: scanner.o $(MODELCHECKER)
$(CC) $(OPTIONS) $(MODELCHECKER) -o scyther $(LOADLIBS) $(LDLIBS)
ptestmain.o scanner.o : tok.h
#
# Cleanup
#
clean:
rm -f *.o
rm -f scyther
rm -f scanner.c
rm -f parser.c
rm -f tok.h
#
# Clean and rebuild: 'make new'
#
new:
make clean
make all
#
# Make doxygen reference manuals. (in ../refman)
#
refman: doxyconfig
doxygen doxyconfig

View File

@ -1,58 +0,0 @@
################################################################
# Name: SVNVersion.cmake
# Purpose: Determine subversion revision id for Scyther
# and write it into a macro in version.h
# Author: Cas Cremers
################################################################
# Technically, this only needs to be redone each time a file
# changes, so this is a target with dependencies on all files.
# Checkout version info
find_program (SVNVERSION_EXECUTABLE NAMES svnversion)
mark_as_advanced (SVNVERSION_EXECUTABLE)
mark_as_advanced (SVNVERSION_DYNAMIC)
set (SVNVERSION_DYNAMIC false)
if (SVNVERSION_EXECUTABLE)
# test whether svnversion gives useful info
execute_process (
COMMAND ${SVNVERSION_EXECUTABLE} --no-newline
OUTPUT_VARIABLE SVN_Result
)
mark_as_advanced (SVN_Result)
if (NOT ${SVN_Result} STREQUAL "exported")
# svnversion gives useful stuff
## write to file
#file (WRITE version.h "#define SVNVERSION \"${SVN_Result}\"\n")
set (SVNVERSION_DYNAMIC true)
endif (NOT ${SVN_Result} STREQUAL "exported")
mark_as_advanced (SVNDIR)
endif (SVNVERSION_EXECUTABLE)
# If dynamic generation is required, this means another target in the
# makefile
if (SVNVERSION_DYNAMIC)
# add a command to generate version.h
message (STATUS "Generating version.h dynamically using svnversion command")
add_custom_command (
OUTPUT version.h
# The version number depends on all the files; if they
# don't change, neither should the version number
# (although this might be incorrect when updating the
# current directory)
DEPENDS ${Scyther_sources}
DEPENDS .svn
COMMAND ./subbuild-version-information.sh
COMMENT "Generating subversion and tag version information in version.h using svnversion command"
)
else (SVNVERSION_DYNAMIC)
# Don't dynamically generate, simply empty every time
file (WRITE version.h "#define SVNVERSION \"Unknown\"\n#define TAGVERSION \"Unknown\"")
endif (SVNVERSION_DYNAMIC)
# add the version number to the sources
set_source_files_properties(version.h
PROPERTIES
GENERATED true)
set (Scyther_sources ${Scyther_sources} version.h)

View File

@ -1,41 +0,0 @@
################################################################
# Name: ScannerParser.cmake
# Purpose: If flex/bison are available, generate parser and scanner
# Author: Cas Cremers
################################################################
# Make the scanner using flex, if it can be found
include(FindFLEX.cmake)
if (FLEX_FOUND)
set_source_files_properties(scanner.c PROPERTIES GENERATED true)
ADD_CUSTOM_COMMAND (
OUTPUT scanner.c
DEPENDS scanner.l
COMMAND ${FLEX_EXECUTABLE}
# TODO: I should look up from which version the -o
# switch works, might not be portable.
ARGS -oscanner.c scanner.l
COMMENT "Building scanner.c from scanner.l using flex"
)
else (FLEX_FOUND)
message (STATUS "Because flex is not found, we will use the existing scanner.c")
endif (FLEX_FOUND)
# Make the parser using bison, if it can be found
include(FindBISON.cmake)
if (BISON_FOUND)
set_source_files_properties(parser.c PROPERTIES GENERATED true)
ADD_CUSTOM_COMMAND (
OUTPUT parser.c
DEPENDS parser.y
COMMAND ${BISON_EXECUTABLE}
# TODO: I should look up from which version the -o
# switch works, might not be portable.
ARGS -d -oparser.c parser.y
COMMENT "Building parser.c from parser.y using bison"
)
else (BISON_FOUND)
message (STATUS "Because bison is not found, we will use the existing parser.c")
endif (BISON_FOUND)

View File

@ -1,789 +0,0 @@
[Project]
FileName=Scyther.dev
Name=Scyther
UnitCount=72
Type=1
Ver=1
ObjFiles=
Includes=
Libs=
PrivateResource=
ResourceIncludes=
MakeIncludes=
Compiler=
CppCompiler=
Linker=
IsCpp=0
Icon=
ExeOutput=..\gui\Scyther
ObjectOutput=
OverrideOutput=0
OverrideOutputName=Scyther.exe
HostApplication=
Folders=
CommandLine=
UseCustomMakefile=0
CustomMakefile=
IncludeVersionInfo=0
SupportXPThemes=0
CompilerSet=0
CompilerSettings=0000000000000000000000
[Unit1]
FileName=xmlout.h
CompileCpp=0
Folder=Scyther
Compile=1
Link=1
Priority=1000
OverrideBuildCmd=0
BuildCmd=
[Unit2]
FileName=arachne.c
CompileCpp=0
Folder=Scyther
Compile=1
Link=1
Priority=1000
OverrideBuildCmd=0
BuildCmd=
[Unit3]
FileName=arachne.h
CompileCpp=0
Folder=Scyther
Compile=1
Link=1
Priority=1000
OverrideBuildCmd=0
BuildCmd=
[Unit4]
FileName=binding.c
CompileCpp=0
Folder=Scyther
Compile=1
Link=1
Priority=1000
OverrideBuildCmd=0
BuildCmd=
[Unit5]
FileName=binding.h
CompileCpp=0
Folder=Scyther
Compile=1
Link=1
Priority=1000
OverrideBuildCmd=0
BuildCmd=
[Unit6]
FileName=claim.c
CompileCpp=0
Folder=Scyther
Compile=1
Link=1
Priority=1000
OverrideBuildCmd=0
BuildCmd=
[Unit7]
FileName=claim.h
CompileCpp=0
Folder=Scyther
Compile=1
Link=1
Priority=1000
OverrideBuildCmd=0
BuildCmd=
[Unit8]
FileName=color.c
CompileCpp=0
Folder=Scyther
Compile=1
Link=1
Priority=1000
OverrideBuildCmd=0
BuildCmd=
[Unit9]
FileName=color.h
CompileCpp=0
Folder=Scyther
Compile=1
Link=1
Priority=1000
OverrideBuildCmd=0
BuildCmd=
[Unit10]
FileName=compiler.c
CompileCpp=0
Folder=Scyther
Compile=1
Link=1
Priority=1000
OverrideBuildCmd=0
BuildCmd=
[Unit11]
FileName=compiler.h
CompileCpp=0
Folder=Scyther
Compile=1
Link=1
Priority=1000
OverrideBuildCmd=0
BuildCmd=
[Unit12]
FileName=cost.c
CompileCpp=0
Folder=Scyther
Compile=1
Link=1
Priority=1000
OverrideBuildCmd=0
BuildCmd=
[Unit13]
FileName=cost.h
CompileCpp=0
Folder=Scyther
Compile=1
Link=1
Priority=1000
OverrideBuildCmd=0
BuildCmd=
[Unit14]
FileName=debug.c
CompileCpp=0
Folder=Scyther
Compile=1
Link=1
Priority=1000
OverrideBuildCmd=0
BuildCmd=
[Unit15]
FileName=debug.h
CompileCpp=0
Folder=Scyther
Compile=1
Link=1
Priority=1000
OverrideBuildCmd=0
BuildCmd=
[Unit16]
FileName=depend.c
CompileCpp=0
Folder=Scyther
Compile=1
Link=1
Priority=1000
OverrideBuildCmd=0
BuildCmd=
[Unit17]
FileName=depend.h
CompileCpp=0
Folder=Scyther
Compile=1
Link=1
Priority=1000
OverrideBuildCmd=0
BuildCmd=
[Unit18]
FileName=dotout.c
CompileCpp=0
Folder=Scyther
Compile=1
Link=1
Priority=1000
OverrideBuildCmd=0
BuildCmd=
[Unit19]
FileName=dotout.h
CompileCpp=0
Folder=Scyther
Compile=1
Link=1
Priority=1000
OverrideBuildCmd=0
BuildCmd=
[Unit20]
FileName=error.c
CompileCpp=0
Folder=Scyther
Compile=1
Link=1
Priority=1000
OverrideBuildCmd=0
BuildCmd=
[Unit21]
FileName=error.h
CompileCpp=0
Folder=Scyther
Compile=1
Link=1
Priority=1000
OverrideBuildCmd=0
BuildCmd=
[Unit22]
FileName=heuristic.c
CompileCpp=0
Folder=Scyther
Compile=1
Link=1
Priority=1000
OverrideBuildCmd=0
BuildCmd=
[Unit23]
FileName=heuristic.h
CompileCpp=0
Folder=Scyther
Compile=1
Link=1
Priority=1000
OverrideBuildCmd=0
BuildCmd=
[Unit24]
FileName=hidelevel.c
CompileCpp=0
Folder=Scyther
Compile=1
Link=1
Priority=1000
OverrideBuildCmd=0
BuildCmd=
[Unit25]
FileName=hidelevel.h
CompileCpp=0
Folder=Scyther
Compile=1
Link=1
Priority=1000
OverrideBuildCmd=0
BuildCmd=
[Unit26]
FileName=intruderknowledge.c
CompileCpp=0
Folder=Scyther
Compile=1
Link=1
Priority=1000
OverrideBuildCmd=0
BuildCmd=
[Unit27]
FileName=intruderknowledge.h
CompileCpp=0
Folder=Scyther
Compile=1
Link=1
Priority=1000
OverrideBuildCmd=0
BuildCmd=
[Unit28]
FileName=knowledge.c
CompileCpp=0
Folder=Scyther
Compile=1
Link=1
Priority=1000
OverrideBuildCmd=0
BuildCmd=
[Unit29]
FileName=knowledge.h
CompileCpp=0
Folder=Scyther
Compile=1
Link=1
Priority=1000
OverrideBuildCmd=0
BuildCmd=
[Unit30]
FileName=label.c
CompileCpp=0
Folder=Scyther
Compile=1
Link=1
Priority=1000
OverrideBuildCmd=0
BuildCmd=
[Unit31]
FileName=label.h
CompileCpp=0
Folder=Scyther
Compile=1
Link=1
Priority=1000
OverrideBuildCmd=0
BuildCmd=
[Unit32]
FileName=list.c
CompileCpp=0
Folder=Scyther
Compile=1
Link=1
Priority=1000
OverrideBuildCmd=0
BuildCmd=
[Unit33]
FileName=list.h
CompileCpp=0
Folder=Scyther
Compile=1
Link=1
Priority=1000
OverrideBuildCmd=0
BuildCmd=
[Unit35]
FileName=mgu.h
CompileCpp=0
Folder=Scyther
Compile=1
Link=1
Priority=1000
OverrideBuildCmd=0
BuildCmd=
[Unit36]
FileName=pheading.h
CompileCpp=0
Folder=Scyther
Compile=1
Link=1
Priority=1000
OverrideBuildCmd=0
BuildCmd=
[Unit37]
FileName=prune_bounds.c
CompileCpp=0
Folder=Scyther
Compile=1
Link=1
Priority=1000
OverrideBuildCmd=0
BuildCmd=
[Unit38]
FileName=prune_bounds.h
CompileCpp=0
Folder=Scyther
Compile=1
Link=1
Priority=1000
OverrideBuildCmd=0
BuildCmd=
[Unit39]
FileName=prune_theorems.c
CompileCpp=0
Folder=Scyther
Compile=1
Link=1
Priority=1000
OverrideBuildCmd=0
BuildCmd=
[Unit40]
FileName=prune_theorems.h
CompileCpp=0
Folder=Scyther
Compile=1
Link=1
Priority=1000
OverrideBuildCmd=0
BuildCmd=
[Unit41]
FileName=role.c
CompileCpp=0
Folder=Scyther
Compile=1
Link=1
Priority=1000
OverrideBuildCmd=0
BuildCmd=
[Unit42]
FileName=role.h
CompileCpp=0
Folder=Scyther
Compile=1
Link=1
Priority=1000
OverrideBuildCmd=0
BuildCmd=
[Unit43]
FileName=specialterm.c
CompileCpp=0
Folder=Scyther
Compile=1
Link=1
Priority=1000
OverrideBuildCmd=0
BuildCmd=
[Unit44]
FileName=specialterm.h
CompileCpp=0
Folder=Scyther
Compile=1
Link=1
Priority=1000
OverrideBuildCmd=0
BuildCmd=
[Unit45]
FileName=states.c
CompileCpp=0
Folder=Scyther
Compile=1
Link=1
Priority=1000
OverrideBuildCmd=0
BuildCmd=
[Unit46]
FileName=states.h
CompileCpp=0
Folder=Scyther
Compile=1
Link=1
Priority=1000
OverrideBuildCmd=0
BuildCmd=
[Unit48]
FileName=switches.h
CompileCpp=0
Folder=Scyther
Compile=1
Link=1
Priority=1000
OverrideBuildCmd=0
BuildCmd=
[Unit49]
FileName=symbol.c
CompileCpp=0
Folder=Scyther
Compile=1
Link=1
Priority=1000
OverrideBuildCmd=0
BuildCmd=
[Unit50]
FileName=symbol.h
CompileCpp=0
Folder=Scyther
Compile=1
Link=1
Priority=1000
OverrideBuildCmd=0
BuildCmd=
[Unit51]
FileName=system.c
CompileCpp=0
Folder=Scyther
Compile=1
Link=1
Priority=1000
OverrideBuildCmd=0
BuildCmd=
[Unit52]
FileName=system.h
CompileCpp=0
Folder=Scyther
Compile=1
Link=1
Priority=1000
OverrideBuildCmd=0
BuildCmd=
[Unit53]
FileName=tac.c
CompileCpp=0
Folder=Scyther
Compile=1
Link=1
Priority=1000
OverrideBuildCmd=0
BuildCmd=
[Unit54]
FileName=tac.h
CompileCpp=0
Folder=Scyther
Compile=1
Link=1
Priority=1000
OverrideBuildCmd=0
BuildCmd=
[Unit55]
FileName=term.c
CompileCpp=0
Folder=Scyther
Compile=1
Link=1
Priority=1000
OverrideBuildCmd=0
BuildCmd=
[Unit56]
FileName=term.h
CompileCpp=0
Folder=Scyther
Compile=1
Link=1
Priority=1000
OverrideBuildCmd=0
BuildCmd=
[Unit57]
FileName=termlist.c
CompileCpp=0
Folder=Scyther
Compile=1
Link=1
Priority=1000
OverrideBuildCmd=0
BuildCmd=
[Unit58]
FileName=termlist.h
CompileCpp=0
Folder=Scyther
Compile=1
Link=1
Priority=1000
OverrideBuildCmd=0
BuildCmd=
[Unit59]
FileName=termmap.c
CompileCpp=0
Folder=Scyther
Compile=1
Link=1
Priority=1000
OverrideBuildCmd=0
BuildCmd=
[Unit60]
FileName=termmap.h
CompileCpp=0
Folder=Scyther
Compile=1
Link=1
Priority=1000
OverrideBuildCmd=0
BuildCmd=
[Unit61]
FileName=timer.c
CompileCpp=0
Folder=Scyther
Compile=1
Link=1
Priority=1000
OverrideBuildCmd=0
BuildCmd=
[Unit62]
FileName=timer.h
CompileCpp=0
Folder=Scyther
Compile=1
Link=1
Priority=1000
OverrideBuildCmd=0
BuildCmd=
[Unit63]
FileName=type.c
CompileCpp=0
Folder=Scyther
Compile=1
Link=1
Priority=1000
OverrideBuildCmd=0
BuildCmd=
[Unit64]
FileName=type.h
CompileCpp=0
Folder=Scyther
Compile=1
Link=1
Priority=1000
OverrideBuildCmd=0
BuildCmd=
[Unit65]
FileName=warshall.c
CompileCpp=0
Folder=Scyther
Compile=1
Link=1
Priority=1000
OverrideBuildCmd=0
BuildCmd=
[Unit66]
FileName=warshall.h
CompileCpp=0
Folder=Scyther
Compile=1
Link=1
Priority=1000
OverrideBuildCmd=0
BuildCmd=
[Unit67]
FileName=xmlout.c
CompileCpp=0
Folder=Scyther
Compile=1
Link=1
Priority=1000
OverrideBuildCmd=0
BuildCmd=
[Unit68]
FileName=main.c
CompileCpp=0
Folder=Scyther
Compile=1
Link=1
Priority=1000
OverrideBuildCmd=0
BuildCmd=
[Unit69]
FileName=version.h
CompileCpp=0
Folder=
Compile=1
Link=1
Priority=1000
OverrideBuildCmd=0
BuildCmd=
[Unit70]
FileName=parser.h
CompileCpp=0
Folder=Scyther
Compile=1
Link=1
Priority=1000
OverrideBuildCmd=0
BuildCmd=
[Unit71]
FileName=scanner.c
CompileCpp=0
Folder=Scyther
Compile=1
Link=1
Priority=1000
OverrideBuildCmd=0
BuildCmd=
[VersionInfo]
Major=0
Minor=1
Release=1
Build=1
LanguageID=1033
CharsetID=1252
CompanyName=
FileVersion=
FileDescription=Developed using the Dev-C++ IDE
InternalName=
LegalCopyright=
LegalTrademarks=
OriginalFilename=
ProductName=
ProductVersion=
AutoIncBuildNr=0
[Unit34]
FileName=mgu.c
CompileCpp=0
Folder=Scyther
Compile=1
Link=1
Priority=1000
OverrideBuildCmd=0
BuildCmd=
[Unit72]
FileName=parser.c
CompileCpp=0
Folder=Scyther
Compile=1
Link=1
Priority=1000
OverrideBuildCmd=0
BuildCmd=
[Unit73]
FileName=scanner.c
CompileCpp=0
Folder=Scyther
Compile=1
Link=1
Priority=1000
OverrideBuildCmd=0
BuildCmd=
[Unit74]
FileName=parser.c
CompileCpp=0
Folder=Scyther
Compile=1
Link=1
Priority=1000
OverrideBuildCmd=0
BuildCmd=
[Unit47]
FileName=switches.c
CompileCpp=0
Folder=Scyther
Compile=1
Link=1
Priority=1000
OverrideBuildCmd=0
BuildCmd=

View File

@ -1,42 +0,0 @@
################################################################
# Name: UniversalBinary.cmake
# Purpose: Add target to make a Mac universal binary
# Needs pre-build mac versions first!
# Author: Cas Cremers
################################################################
find_program(lipoexecutable lipo)
if (lipoexecutable)
# Check whether we already have the binaries
set (UBrequiredfiles FALSE)
set (ppcfile "scyther-macppc")
set (intelfile "scyther-macintel")
if (EXISTS "${ppcfile}")
if (EXISTS "${intelfile}")
set (UBrequiredfiles TRUE)
else (EXISTS "${intelfile}")
message (STATUS "Could not find scyther-macintel.")
endif (EXISTS "${intelfile}")
else (EXISTS "${ppcfile}")
message (STATUS "Could not find scyther-macppc.")
endif (EXISTS "${ppcfile}")
# Use information to proceed
if (UBrequiredfiles)
message (STATUS "Adding target for Mac universal binary")
add_custom_target (scyther-mac
COMMAND lipo -create "${ppcfile}" "${intelfile}" -output scyther-mac
COMMENT "Generating Mac universal binary"
DEPENDS scyther-macintel
DEPENDS scyther-macppc
)
else (UBrequiredfiles)
message (STATUS "No universal binary possible yet. Please do the following:")
message (STATUS " cmake -DTARGETOS=MacPPC . && make")
message (STATUS " cmake -DTARGETOS=MacIntel . && make")
message (STATUS " cmake . && make scyther-mac")
endif (UBrequiredfiles)
else (lipoexecutable)
message (FATAL_ERROR "Cannot find the 'lipo' program that is required for creating universal binaries")
endif (lipoexecutable)

File diff suppressed because it is too large Load Diff

View File

@ -1,20 +0,0 @@
#ifndef ARACHNE
#define ARACHNE
#include "system.h"
void arachneInit (const System sys);
void arachneDone ();
int arachne ();
int get_semitrace_length ();
void indentPrint ();
int isTriviallyKnownAtArachne (const System sys, const Term t, const int run,
const int index);
int isTriviallyKnownAfterArachne (const System sys, const Term t,
const int run, const int index);
void arachneOutputAttack ();
void printSemiState ();
int countIntruderActions ();
void role_name_print (const int run);
#endif

View File

@ -1,61 +0,0 @@
\documentclass{article}
\usepackage{a4wide}
\usepackage{msc}
\usepackage{ifthen}
%\setlength{\instwidth}{3.0cm}
%\setlength{\instdist}{4cm}
%\setlength{\actionwidth}{3.6cm}
%\setlength{\conditionoverlap}{1.9cm}
% Action macro from MSC documentation
\newsavebox{\labelbox}
\newlength{\oldwd}
\newlength{\oldht}
\newcommand{\Action}[2]{%
\setlength{\oldwd}{\actionwidth}%
\setlength{\oldht}{\actionheight}%
\savebox{\labelbox}{#1}%
\setlength{\actionwidth}{\wd\labelbox + 2\labeldist}%
\setlength{\actionheight}{\ht\labelbox + \dp\labelbox + 2\labeldist}%
\action{\usebox{\labelbox}}{#2}%
\setlength{\actionwidth}{\oldwd}%
\setlength{\actionheight}{\oldht}%
}
\newlength{\mscspacer}
\setlength{\mscspacer}{1ex}
\newcommand{\ActionBox}[2]{%
\Action{\parbox{\maxmscaction - 2\mscspacer}{\centering #1}}{#2}
}
\newlength{\maxtemp}
\newcommand{\maxlength}[2]{
\settowidth{\maxtemp}{#2}
\ifthenelse{\lengthtest{#1 < \maxtemp}}{\setlength{#1}{\maxtemp}}{}
\ifthenelse{\lengthtest{\maxmscall < \maxtemp}}{\setlength{\maxmscall}{\maxtemp}}{}
}
\newlength{\maxmscall}
\newlength{\maxmscinst}
\newlength{\maxmscaction}
\newlength{\maxmsccondition}
\setlength{\maxmscall}{\mscspacer}
\setlength{\maxmscinst}{\mscspacer}
\setlength{\maxmscaction}{\mscspacer}
\setlength{\maxmsccondition}{\mscspacer}
% pagestyle without numbering
\pagestyle{empty}
\begin{document}
\input{attack}
\end{document}

View File

@ -1,617 +0,0 @@
/**
* Handle bindings for Arache engine.
*/
#include "list.h"
#include "role.h"
#include "label.h"
#include "system.h"
#include "binding.h"
#include "warshall.h"
#include "debug.h"
#include "term.h"
#include "termmap.h"
#include "arachne.h"
#include "switches.h"
#include "depend.h"
#include "error.h"
#if !defined(__APPLE__)
#include <malloc.h>
#endif
static System sys; //!< local storage of system pointer
extern Protocol INTRUDER; //!< The intruder protocol
extern Role I_M; //!< special role; precedes all other events always
/*
*
* Assist stuff
*
*/
//! Create mem for binding
Binding
binding_create (Term term, int run_to, int ev_to)
{
Binding b;
b = malloc (sizeof (struct binding));
b->done = false;
b->blocked = false;
b->run_from = -1;
b->ev_from = -1;
b->run_to = run_to;
b->ev_to = ev_to;
b->term = term;
b->level = 0;
return b;
}
//! Remove mem for binding
void
binding_destroy (Binding b)
{
if (b->done)
{
goal_unbind (b);
}
free (b);
}
/*
*
* Main
*
*/
//! Init module
void
bindingInit (const System mysys)
{
sys = mysys;
sys->bindings = NULL;
dependInit (sys);
}
//! Close up
void
bindingDone ()
{
int delete (Binding b)
{
binding_destroy (b);
return true;
}
list_iterate (sys->bindings, delete);
list_destroy (sys->bindings);
dependDone (sys);
}
/**
*
* Externally available functions
*
*/
//! Print a binding (given a binding list pointer)
int
binding_print (const Binding b)
{
if (b->done)
eprintf ("Binding (%i,%i) --( ", b->run_from, b->ev_from);
else
eprintf ("Unbound --( ");
termPrint (b->term);
eprintf (" )->> (%i,%i)", b->run_to, b->ev_to);
if (b->blocked)
eprintf ("[blocked]");
return true;
}
//! Bind a goal (true if success, false if it must be pruned)
int
goal_bind (const Binding b, const int run, const int ev)
{
if (b->blocked)
{
error ("Trying to bind a blocked goal.");
}
if (!b->done)
{
#ifdef DEBUG
if (run >= sys->maxruns || sys->runs[run].step <= ev)
{
globalError++;
eprintf ("For term: ");
termPrint (b->term);
eprintf (" needed for r%ii%i.\n", b->run_to, b->ev_to);
eprintf ("Current limits: %i runs, %i events for this run.\n",
sys->maxruns, sys->runs[run].step);
globalError--;
error
("trying to bind to something not yet in the semistate: r%ii%i.",
run, ev);
}
#endif
b->run_from = run;
b->ev_from = ev;
if (dependPushEvent (run, ev, b->run_to, b->ev_to))
{
b->done = true;
if (switches.output == PROOF)
{
indentPrint ();
binding_print (b);
eprintf ("\n");
}
return true;
}
}
else
{
globalError++;
binding_print (b);
error ("Trying to bind a bound goal again.");
}
return false;
}
//! Unbind a goal
void
goal_unbind (const Binding b)
{
if (b->done)
{
dependPopEvent ();
b->done = false;
}
else
{
error ("Trying to unbind an unbound goal again.");
}
}
//! Bind a goal as a dummy (block)
/**
* Especially made for tuple expansion
*
* @TODO Weird that this returns a value (always true, otherwise error)
*/
int
binding_block (Binding b)
{
if (!b->blocked)
{
b->blocked = true;
return true;
}
error ("Trying to block a goal again.");
return false;
}
//! Unblock a binding
/*
* @TODO Weird that this returns a value (always true, otherwise error)
*/
int
binding_unblock (Binding b)
{
if (b->blocked)
{
b->blocked = false;
return true;
}
error ("Trying to unblock a non-blocked goal.");
return false;
}
//! Add a goal
/**
* The int parameter 'level' is just to store additional info. Here, it stores priorities for a goal.
* Higher level goals will be selected first. Typically, a normal goal is level 0, a key is 1.
*
* Returns the number of added goals (sometimes unfolding tuples)
*/
int
goal_add (Term term, const int run, const int ev, const int level)
{
term = deVar (term);
#ifdef DEBUG
if (term == NULL)
{
globalError++;
roledefPrint (eventRoledef (sys, run, ev));
eprintf ("\n");
globalError--;
error ("Trying to add an emtpy goal term to r%ii%i, with level %i.",
run, ev, level);
}
if (run >= sys->maxruns)
error ("Trying to add a goal for a run that does not exist.");
if (ev >= sys->runs[run].step)
error
("Trying to add a goal for an event that is not in the semistate yet.");
#endif
if (switches.intruder && realTermTuple (term))
{
// Only split if there is an intruder
return goal_add (TermOp1 (term), run, ev, level) +
goal_add (TermOp2 (term), run, ev, level);
}
else
{
// Determine whether we already had it
int createnew;
int testSame (void *data)
{
Binding b;
b = (Binding) data;
if (isTermEqual (b->term, term))
{
// binding of same term
if (run == b->run_to && ev == b->ev_to)
{
// identical binding
createnew = false;
}
}
return true;
}
createnew = true;
list_iterate (sys->bindings, testSame);
if (createnew)
{
// Add a new binding
Binding b;
b = binding_create (term, run, ev);
b->level = level;
sys->bindings = list_insert (sys->bindings, b);
#ifdef DEBUG
if (DEBUGL (3))
{
eprintf ("Adding new binding for ");
termPrint (term);
eprintf (" to run %i, ev %i.\n", run, ev);
}
#endif
return 1;
}
}
return 0;
}
//! Remove a goal
void
goal_remove_last (int n)
{
while (n > 0)
{
if (sys->bindings != NULL)
{
Binding b;
b = (Binding) sys->bindings->data;
binding_destroy (b);
sys->bindings = list_delete (sys->bindings);
n--;
}
else
{
error
("goal_remove_last error: trying to remove %i too many bindings.",
n);
}
}
}
//! Determine whether some label set is ordered w.r.t. send/read order.
/**
* Assumes all these labels exist in the system, within length etc, and that the run mappings are valid.
*/
int
labels_ordered (Termmap runs, Termlist labels)
{
while (labels != NULL)
{
// Given this label, and the mapping of runs, we want to know if the order is okay. Thus, we need to know sendrole and readrole
Labelinfo linfo;
int send_run, send_ev, read_run, read_ev;
int get_index (const int run)
{
Roledef rd;
int i;
i = 0;
rd = sys->runs[run].start;
while (rd != NULL && !isTermEqual (rd->label, labels->term))
{
rd = rd->next;
i++;
}
#ifdef DEBUG
if (rd == NULL)
error
("Could not locate send or read for label, after niagree holds, to test for order.");
#endif
return i;
}
linfo = label_find (sys->labellist, labels->term);
if (!linfo->ignore)
{
send_run = termmapGet (runs, linfo->sendrole);
read_run = termmapGet (runs, linfo->readrole);
send_ev = get_index (send_run);
read_ev = get_index (read_run);
if (!isDependEvent (send_run, send_ev, read_run, read_ev))
{
// Not ordered; false
return false;
}
}
// Proceed
labels = labels->next;
}
return true;
}
//! Check whether the binding denotes a sensible thing such that we can use run_from and ev_from
int
valid_binding (Binding b)
{
if (b->done && (!b->blocked))
return true;
else
return false;
}
//! Iterate over all bindings
/**
* Iterator should return true to proceed
*/
int
iterate_bindings (int (*func) (Binding b))
{
List bl;
for (bl = sys->bindings; bl != NULL; bl = bl->next)
{
Binding b;
b = (Binding) bl->data;
if (!func (b))
{
return false;
}
}
return true;
}
//! Iterate over preceding bindings (this does not include stuff bound to the same destination)
/**
* Iterator should return true to proceed
*/
int
iterate_preceding_bindings (const int run, const int ev,
int (*func) (Binding b))
{
int precs (Binding b)
{
if (isDependEvent (b->run_to, b->ev_to, run, ev))
{
return func (b);
}
return true;
}
return iterate_bindings (precs);
}
//! Check for unique origination
/*
* Contrary to a previous version, we simply check for unique origination.
* This immediately takes care of any 'occurs before' things. Complexity is N
* log N.
*
* Each term should originate only at one point (thus in one binding)
*
*@returns True, if it's okay. If false, it needs to be pruned.
*/
int
unique_origination ()
{
List bl;
bl = sys->bindings;
while (bl != NULL)
{
Binding b;
b = (Binding) bl->data;
// Check for a valid binding; it has to be 'done' and sensibly bound (not as in tuple expanded stuff)
if (valid_binding (b))
{
Termlist terms;
terms = tuple_to_termlist (b->term);
if (terms != NULL)
{
/* Apparently this is a good term.
* Now we check whether it occurs in any previous bindings as well.
*/
List bl2;
bl2 = sys->bindings;
while (bl2 != bl)
{
Binding b2;
b2 = (Binding) bl2->data;
if (valid_binding (b2))
{
Termlist terms2, sharedterms;
if (switches.intruder)
{
// For intruder we work with sets here
terms2 = tuple_to_termlist (b2->term);
}
else
{
// For regular agents we use terms
terms2 = termlistAdd (NULL, b2->term);
}
sharedterms = termlistConjunct (terms, terms2);
// Compare terms
if (sharedterms != NULL)
{
// Apparently, this binding shares a term.
// Equal terms should originate at the same point
if (b->run_from != b2->run_from ||
b->ev_from != b2->ev_from)
{
// Not equal: thus no unique origination.
return false;
}
}
termlistDelete (terms2);
termlistDelete (sharedterms);
}
bl2 = bl2->next;
}
}
termlistDelete (terms);
}
bl = bl->next;
}
return true;
}
//! Prune invalid state w.r.t. <=C minimal requirement
/**
* Intuition says this can be done a lot more efficient. Luckily this is the prototype.
*
*@returns True, if it's okay. If false, it needs to be pruned.
*/
int
bindings_c_minimal ()
{
if (!unique_origination ())
{
return false;
}
{
List bl;
// For all goals
bl = sys->bindings;
while (bl != NULL)
{
Binding b;
b = (Binding) bl->data;
// Check for a valid binding; it has to be 'done' and sensibly bound (not as in tuple expanded stuff)
if (valid_binding (b))
{
int run;
// Find all preceding events
for (run = 0; run < sys->maxruns; run++)
{
int ev;
//!@todo hardcoded reference to step, should be length
for (ev = 0; ev < sys->runs[run].step; ev++)
{
if (isDependEvent (run, ev, b->run_from, b->ev_from))
{
// this node is *before* the from node
Roledef rd;
int occursthere;
rd = roledef_shift (sys->runs[run].start, ev);
if (switches.intruder)
{
// intruder: interm bindings should cater for the first occurrence
occursthere = termInTerm (rd->message, b->term);
}
else
{
// no intruder, then simple test
occursthere = isTermEqual (rd->message, b->term);
}
if (occursthere)
{
// This term already occurs in a previous node!
#ifdef DEBUG
if (DEBUGL (4))
{
// Report this
indentPrint ();
eprintf ("Binding for ");
termPrint (b->term);
eprintf
(" at r%i i%i is not c-minimal because it occurred before at r%i i%i in ",
b->run_from, b->ev_from, run, ev);
termPrint (rd->message);
eprintf ("\n");
}
#endif
return false;
}
}
else
{
// If this event is not before the target, then the
// next in the run certainly is not either (because
// that would imply that this one is before it)
// Thus, we effectively exit the loop.
break;
}
}
}
}
bl = bl->next;
}
}
return true;
}
//! Count the number of bindings that are done.
int
countBindingsDone ()
{
int count;
int countDone (Binding b)
{
if ((!b->blocked) && b->done)
{
count++;
}
return true;
}
count = 0;
iterate_bindings (countDone);
return count;
}

View File

@ -1,53 +0,0 @@
#ifndef BINDINGS
#define BINDINGS
#include "term.h"
#include "termmap.h"
#include "system.h"
//! Binding structure
/*
* Idea is the ev_from *has to* precede the ev_to
*/
struct binding
{
int done; //!< Iff true, it is bound
int blocked; //!< Iff true, ignore it
int run_from; //!< origination run
int ev_from; //!< step in origination run
int run_to; //!< destination run
int ev_to; //!< step in destination run
Term term; //!< Binding term
int level; //!< ???
};
typedef struct binding *Binding; //!< pointer to binding structure
void bindingInit (const System mysys);
void bindingDone ();
int binding_print (Binding b);
int valid_binding (Binding b);
int goal_add (Term term, const int run, const int ev, const int level);
int goal_add_fixed (Term term, const int run, const int ev, const int fromrun,
const int fromev);
void goal_remove_last (int n);
int goal_bind (const Binding b, const int run, const int ev);
void goal_unbind (const Binding b);
int binding_block (Binding b);
int binding_unblock (Binding b);
int labels_ordered (Termmap runs, Termlist labels);
int iterate_bindings (int (*func) (Binding b));
int iterate_preceding_bindings (const int run, const int ev,
int (*func) (Binding b));
int bindings_c_minimal ();
int countBindingsDone ();
#endif

View File

@ -1,119 +0,0 @@
--+++ 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
public key search stuff. That is a flaw in the heuristic: we should not look
for anything that is in the intruder knowledge already. In fact, it is a
problem with branching. We should not look for PK(X), even if X is a
variable. Priority should go to keys of which the constructor is not in M_0,
maybe that heuristic works.
However, there seems to be an infinite loop for this in the algorithm, which
I did not anticipate. Investigate!
<br>
Maybe self-loops are the problem. This has to do with tuple alternation
decoding. Consider re-introducing explicit intruder strands OR self-loop
pruning.
---+++ Would like to have
---++++ 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.
* Fix 'never sent secrets' list, that are e.g. secret keys of regular agents
and such. The intruder can never learn these, we need this for pruning.
If a goal is such a term, we prune. Investigate how this can be incorporated.
Investigate also whether this actually makes a difference.
* Make 'generate_trace_bindings' to create the bindings for a given trace.
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.
* Fix function handling (signatures).
* Move initial intruder knowledge maybe into the title of the MSC.
* Implement run knowledge, and use this in protocol compiler.
* Introduce 'Ticket' default type in the compiler, along with some
handling for that.
* The 'choose' operator must always be typed, I think. Yes.
* The woolam-ce is incorrect because it is illegal to have a variable
term in a key that is read, by CMV semantics. I don't know what it
means for CE semantics (yet).
* Idea: run bla.bla(params) [compromised <localterm> [,<localterm>] ];
1. These local terms are given to the intruder. Technically this
should only happen _after_ they are first sent in the run. Maybe add
this to send semantics: if termOccurs(sendterm, compromisedterm) then
add compromisedterm to M, remove compromisedterm from list of terms to
compromise.
1. All claims in the run are ignored (add untrusted flag to run)
Alternative: run x.x(x) untrusted; or just compromised, to give up
all constants.
Note this is not sufficient yet, because it does not consider any
partner runs. Maybe declare a 'compromised' section first; other runs
will only activate after these have completed. Note this is much more
expensive.
* Woolam-ce gives nothing. But then again, it's a wrong impl.
* Global/protocol variables should not exist in the current system.
* run nsl.initiator(alice, all Agent) constructs?
* 'all' would generate the roles with the corresponding type.
* or maybe for clarity/complexity control: use 'runs' for constructs
with 'all' in it.
* Maybe function application ought to be a different basic term type.
* After role construction, msc consistency can be checked.
* Reduce knowledge to a simple term list? That would simplify a number
of things, and also allow for easier addition of stuff.
* 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.

View File

@ -1,16 +0,0 @@
#!/bin/sh
PLATFORM=`uname`
echo $PLATFORM
if [ "$PLATFORM" = "Darwin" ]
then
./subbuild-mac-universal.sh
else
if [ "$PLATFORM" = "Linux" ]
then
./subbuild-unix-both.sh
else
echo "I don't know platform $PLATFORM, so I won't do anything"
fi
fi

File diff suppressed because it is too large Load Diff

View File

@ -1,18 +0,0 @@
#ifndef CLAIMS
#define CLAIMS
int check_claim_nisynch (const System sys, const int i);
int check_claim_niagree (const System sys, const int i);
int arachne_claim_niagree (const System sys, const int claim_run,
const int claim_index);
int arachne_claim_nisynch (const System sys, const int claim_run,
const int claim_index);
int prune_claim_specifics (const System sys);
int add_claim_specifics (const System sys, const Claimlist cl, const
Roledef rd, int (*callback) (void));
void count_false_claim (const System sys);
int property_check (const System sys);
int claimStatusReport (const System sys, Claimlist cl);
#endif

View File

@ -1,39 +0,0 @@
/** @file color.c \brief Color output for terminals.
*
* Depends on the switches (to disable them with a --plain switch)
*/
#include <string.h>
#include <stdlib.h>
#include <stdio.h>
#include "switches.h"
//! Substitution string for --plain output
char *empty = "";
//! Reset colors
char *COLOR_Reset = "";
//! Red
char *COLOR_Red = "";
//! Green
char *COLOR_Green = "";
//! Bold
char *COLOR_Bold = "";
//! Init colors
void
colorInit (void)
{
if (switches.plain)
{
COLOR_Reset = empty;
COLOR_Red = empty;
COLOR_Green = empty;
COLOR_Bold = empty;
}
}
//! Exit colors
void
colorDone (void)
{
}

View File

@ -1,12 +0,0 @@
#ifndef COLOROUTPUT
#define COLOROUTPUT
extern char *COLOR_Reset;
extern char *COLOR_Red;
extern char *COLOR_Green;
extern char *COLOR_Bold;
void colorInit (void);
void colorDone (void);
#endif

View File

@ -1,18 +0,0 @@
How to compile Scyther
Requirements expressed as Ubuntu packages where [name][location]
Needed:
gcc
If you don't know what this is, please stop reading.
scons
A Python script set to replace the make etc. toolchain.
For cross-compilation (Windows):
[mingw32][universe]
GCC variant to compile for windows + w32 binutils.
Use 'scons arch=windows' to generate the binary.

File diff suppressed because it is too large Load Diff

View File

@ -1,26 +0,0 @@
#ifndef COMPILER
#define COMPILER
#include "tac.h"
#include "role.h"
#include "system.h"
void compilerInit (const System sys);
void compilerDone (void);
void compile (Tac tc, int maxruns);
void preprocess (const System sys);
Term findGlobalConstant (const char *s);
Term makeGlobalConstant (const char *s);
Term makeGlobalVariable (const char *s);
void compute_role_variables (const System sys, Protocol p, Role r);
Term symbolDeclare (Symbol s, int isVar);
void levelTacDeclaration (Tac tc, int isVar);
#define levelDeclareVar(s) levelTacDeclaration(s,1)
#define levelDeclareConst(s) levelTacDeclaration(s,0)
#define levelVar(s) symbolDeclare(s,1)
#define levelConst(s) symbolDeclare(s,0)
#endif

View File

@ -1,11 +0,0 @@
#!/bin/sh
cp scyther-linux ../gui/Scyther/Bin
cp scyther-w32.exe ../gui/Scyther/Bin
cp scyther-mac ../gui/Scyther/Bin
# bonus...
cp scyther-linux ~/bin
echo Copied the files to their respective locations and ~/bin

View File

@ -1,74 +0,0 @@
/**
*
*@file cost.c
*
* Determine cost of a given semitrace in sys
* Constructed for Arachne results, unreliable otherwise.
*
*/
#include "switches.h"
#include "system.h"
#include "binding.h"
#include "error.h"
#include <limits.h>
//************************************************************************
// Private methods
//************************************************************************
//************************************************************************
// Public methods
//************************************************************************
//! Determine cost of an attack
/*
* This should also work on uncompleted semitraces, and should be monotonous
* (i.e. further iterations should increase the cost only) so that it can be
* used for branch and bound.
*
* A lower value (closer to 0) is a more feasible attack.
*/
int
attackCost (const System sys)
{
if (switches.prune == 0)
{
return 0;
}
if (switches.prune == 1)
{
// Select the first attack.
// Implied by having the cost of traces after finding an attack to be always higher.
//
if (sys->current_claim->failed > 0)
{
// we already have an attack
return INT_MAX;
}
else
{
// return some value relating to the cost (anything less than int_max will do)
return 1;
}
}
if (switches.prune == 2)
{
// Use nice heuristic cf. work of Gijs Hollestelle. Hand-picked parameters.
int cost;
cost = 0;
//cost += get_semitrace_length ();
cost += 10 * selfInitiators (sys);
cost += 7 * selfResponders (sys);
cost += 10 * sys->num_regular_runs;
cost += 3 * countInitiators (sys);
cost += 2 * countBindingsDone ();
cost += 1 * sys->num_intruder_runs;
return cost;
}
error ("Unknown pruning method (cost function not found)");
return 0;
}

View File

@ -1,6 +0,0 @@
#ifndef COST
#define COST
int attackCost (const System sys);
#endif

View File

@ -1,52 +0,0 @@
/**
*@file debug.c
*\brief Debugging code.
*
* It is hoped that this code will become redundant over time.
*/
#include <stdio.h>
#include <stdlib.h>
#include "debug.h"
#include "system.h"
#include "error.h"
static int debuglevel;
//! Set the debuglevel from the main code.
void
debugSet (int level)
{
debuglevel = level;
}
//! Test whether some debuglevel is meant to be printed.
/**
*@param level The debuglevel
*@return True iff level is smaller than, or equal to, the last set debuglevel.
*\sa debugSet()
*/
int
debugCond (int level)
{
return (level <= debuglevel);
}
//! Print some debug string for some level, if desired.
/**
*@param level The debuglevel
*@param string The string to be displayed for this level.
*@return If the debuglevel is higher than the level, the string is ignored.
* Otherwise it will be printed.
*\sa debugCond()
*/
void
debug (int level, char *string)
{
#ifdef DEBUG
if (debugCond (level))
{
indent ();
printfstderr ("DEBUG [%i]: %s\n", level, string);
}
#endif
}

View File

@ -1,10 +0,0 @@
#ifndef DEBUG_H
#define DEBUG_H
void debugSet (int level);
int debugCond (int level);
void debug (int level, char *string);
#define DEBUGL(a) debugCond(a)
#endif

View File

@ -1,569 +0,0 @@
/**
* @file depend.c
* \brief interface for graph code from the viewpoint of events.
*
*/
#include <stdlib.h>
#include <string.h>
#include "depend.h"
#include "term.h"
#include "system.h"
#include "binding.h"
#include "warshall.h"
#include "debug.h"
#include "error.h"
/*
* Generic structures
* ---------------------------------------------------------------
*/
//! Event dependency structure
struct depeventgraph
{
//! Flag denoting what it was made for (newrun|newbinding)
int fornewrun;
//! Number of runs;
int runs;
//! System where it derives from
System sys;
//! Number of nodes
int n;
//! Rowsize
int rowsize;
//! Graph structure
unsigned int *G;
//! Zombie dummy push
int zombie;
//! Previous graph
struct depeventgraph *prev;
};
//! Pointer shorthard
typedef struct depeventgraph *Depeventgraph;
/*
* External
* ---------------------------------------------------------------
*/
extern Protocol INTRUDER; //!< The intruder protocol
extern Role I_M; //!< special role; precedes all other events always
/*
* Globals
* ---------------------------------------------------------------
*/
Depeventgraph currentdepgraph;
/*
* Default code
* ---------------------------------------------------------------
*/
//! Default init
void
dependInit (const System sys)
{
currentdepgraph = NULL;
}
//! Pring
void
dependPrint ()
{
Depeventgraph dg;
eprintf ("Printing DependEvent stack, top first.\n\n");
for (dg = currentdepgraph; dg != NULL; dg = dg->prev)
{
eprintf ("%i nodes, %i rowsize, %i zombies, %i runs: created for new ",
dg->n, dg->rowsize, dg->zombie, dg->runs);
if (dg->fornewrun)
{
eprintf ("run");
}
else
{
eprintf ("binding");
}
eprintf ("\n");
}
eprintf ("\n");
#ifdef DEBUG
{
int n1;
int r1;
int o1;
r1 = 0;
o1 = 0;
eprintf ("Printing dependency graph.\n");
eprintf ("Y axis nodes comes before X axis node.\n");
for (n1 = 0; n1 < nodeCount (); n1++)
{
int n2;
int r2;
int o2;
if ((n1 - o1) >= currentdepgraph->sys->runs[r1].rolelength)
{
o1 += currentdepgraph->sys->runs[r1].rolelength;
r1++;
eprintf ("\n");
}
r2 = 0;
o2 = 0;
eprintf ("%5i : ", n1);
for (n2 = 0; n2 < nodeCount (); n2++)
{
if ((n2 - o2) >= currentdepgraph->sys->runs[r2].rolelength)
{
o2 += currentdepgraph->sys->runs[r2].rolelength;
r2++;
eprintf (" ");
}
eprintf ("%i", getNode (n1, n2));
}
eprintf ("\n");
}
eprintf ("\n");
}
#endif
}
//! Default cleanup
void
dependDone (const System sys)
{
if (currentdepgraph != NULL)
{
globalError++;
eprintf ("\n\n");
dependPrint ();
globalError--;
error
("depgraph stack (depend.c) not empty at dependDone, bad iteration?");
}
}
/*
* Libs
* ---------------------------------------------------------------
*/
//! Convert from event to node in a graph (given that sys is set)
int
eventtonode (const Depeventgraph dgx, const int r, const int e)
{
int i;
int n;
n = 0;
for (i = 0; i < dgx->sys->maxruns; i++)
{
if (i == r)
{
// this run
#ifdef DEBUG
if (dgx->sys->runs[i].rolelength <= e)
{
error ("Bad offset for eventtonode");
}
#endif
return (n + e);
}
else
{
// not this run, add offset
n += dgx->sys->runs[i].rolelength;
}
}
error ("Bad offset (run number too high?) for eventtonode");
return 0;
}
//! Return the number of nodes in a graph
int
countnodes (const Depeventgraph dgx)
{
int i;
int nodes;
nodes = 0;
for (i = 0; i < dgx->sys->maxruns; i++)
{
nodes += dgx->sys->runs[i].rolelength;
}
return nodes;
}
//! Graph size given the number of nodes
unsigned int
getGraphSize (const Depeventgraph dgx)
{
return (dgx->n * dgx->rowsize);
}
//! Create graph from sys
Depeventgraph
dependCreate (const System sys)
{
Depeventgraph dgnew;
dgnew = (Depeventgraph) MALLOC (sizeof (struct depeventgraph));
dgnew->sys = sys;
dgnew->fornewrun = true;
dgnew->runs = sys->maxruns;
dgnew->zombie = 0;
dgnew->prev = NULL;
dgnew->n = countnodes (dgnew); // count nodes works on ->sys
dgnew->rowsize = WORDSIZE (dgnew->n);
dgnew->G = (unsigned int *) CALLOC (1, getGraphSize (dgnew) * sizeof (unsigned int)); // works on ->n and ->rowsize
return dgnew;
}
//! Copy graph from current one
Depeventgraph
dependCopy (const Depeventgraph dgold)
{
Depeventgraph dgnew;
// Copy old to new
dgnew = (Depeventgraph) MALLOC (sizeof (struct depeventgraph));
memcpy ((void *) dgnew, (void *) dgold,
(size_t) sizeof (struct depeventgraph));
// New copy
dgnew->fornewrun = false;
dgnew->zombie = 0;
// copy inner graph
dgnew->G =
(unsigned int *) MALLOC (getGraphSize (dgold) * sizeof (unsigned int));
memcpy ((void *) dgnew->G, (void *) dgold->G,
getGraphSize (dgold) * sizeof (unsigned int));
return dgnew;
}
//! Destroy graph
void
dependDestroy (const Depeventgraph dgold)
{
FREE (dgold->G);
FREE (dgold);
}
//! push graph to stack (generic)
void
dependPushGeneric (Depeventgraph dgnew)
{
dgnew->prev = currentdepgraph;
currentdepgraph = dgnew;
}
//! restore graph from stack (generic)
void
dependPopGeneric (void)
{
Depeventgraph dgprev;
dgprev = currentdepgraph->prev;
dependDestroy (currentdepgraph);
currentdepgraph = dgprev;
}
// Dependencies from role order
void
dependDefaultRoleOrder (void)
{
int r;
for (r = 0; r < currentdepgraph->sys->maxruns; r++)
{
int e;
for (e = 1; e < currentdepgraph->sys->runs[r].rolelength; e++)
{
setDependEvent (r, e - 1, r, e);
}
}
}
// Dependencies fro bindings order
void
dependDefaultBindingOrder (void)
{
List bl;
for (bl = currentdepgraph->sys->bindings; bl != NULL; bl = bl->next)
{
Binding b;
b = (Binding) bl->data;
if (valid_binding (b))
{
int r1, e1, r2, e2;
r1 = b->run_from;
e1 = b->ev_from;
r2 = b->run_to;
e2 = b->ev_to;
if (!((r1 == r2) && (e1 == e2)))
{
// Not a self-binding
setDependEvent (r1, e1, r2, e2);
}
}
}
}
//! Construct graph dependencies from sys
/**
* uses currentdepgraph->sys
*/
void
dependFromSys (void)
{
dependDefaultRoleOrder ();
dependDefaultBindingOrder ();
}
//! Detect whether the graph has a cycle. If so, a node can get to itself (through the cycle)
int
hasCycle ()
{
int n;
for (n = 0; n < currentdepgraph->n; n++)
{
if (getNode (n, n))
{
return true;
}
}
return false;
}
/*
* Public Code
* ---------------------------------------------------------------
*/
//! get node
int
getNode (const int n1, const int n2)
{
return BIT (currentdepgraph->G + currentdepgraph->rowsize * n1, n2);
}
//! set node
void
setNode (const int n1, const int n2)
{
SETBIT (currentdepgraph->G + currentdepgraph->rowsize * n1, n2);
}
//! Count nodes
int
nodeCount (void)
{
return countnodes (currentdepgraph);
}
/*
* Simple setting
*/
void
setDependEvent (const int r1, const int e1, const int r2, const int e2)
{
int n1, n2;
n1 = eventtonode (currentdepgraph, r1, e1);
n2 = eventtonode (currentdepgraph, r2, e2);
setNode (n1, n2);
}
/*
* Simple testing
*/
int
isDependEvent (const int r1, const int e1, const int r2, const int e2)
{
int n1, n2;
n1 = eventtonode (currentdepgraph, r1, e1);
n2 = eventtonode (currentdepgraph, r2, e2);
return getNode (n1, n2);
}
//! create new graph after adding runs or events (new number of nodes)
void
dependPushRun (const System sys)
{
#ifdef DEBUG
debug (5, "Push dependGraph for new run\n");
#endif
dependPushGeneric (dependCreate (sys));
dependFromSys ();
}
//! restore graph to state after previous run add
void
dependPopRun (void)
{
if (!currentdepgraph->fornewrun)
{
globalError++;
dependPrint ();
globalError--;
error ("Trying to pop graph created for new binding.");
}
#ifdef DEBUG
debug (5, "Pop dependGraph for new run\n");
#endif
dependPopGeneric ();
}
//! create new graph by adding event bindings
/*
* The push code returns true or false: if false, the operation fails because
* it there is now a cycle in the graph, and there is no need to pop the
* result.
*/
int
dependPushEvent (const int r1, const int e1, const int r2, const int e2)
{
if (isDependEvent (r2, e2, r1, e1))
{
// Adding would imply a cycle, so we won't do that.
#ifdef DEBUG
if (DEBUGL (3))
{
eprintf ("Cycle detected for binding %i,%i -> %i,%i.\n", r1, e1, r2,
e2);
}
if (DEBUGL (5))
{
dependPrint ();
}
#endif
return false;
}
else
{
// No immediate cycle: new graph, return true TODO disabled
if ((1 == 1) && (((r1 == r2) && (e1 == e2))
|| isDependEvent (r1, e1, r2, e2)))
{
// if n->n or the binding already existed, no changes
// no change: add zombie
currentdepgraph->zombie += 1;
#ifdef DEBUG
debug (5, "Push dependGraph for new event (zombie push)\n");
if (DEBUGL (5))
{
globalError++;
eprintf ("r%ii%i --> r%ii%i\n", r1, e1, r2, e2);
globalError--;
}
#endif
}
else
{
// change: make new graph copy of the old one
dependPushGeneric (dependCopy (currentdepgraph));
// add new binding
setDependEvent (r1, e1, r2, e2);
// recompute closure
transitive_closure (currentdepgraph->G, currentdepgraph->n);
// check for cycles
if (hasCycle ())
{
//warning ("Cycle slipped undetected by the reverse check.");
// Closure introduced cycle, undo it
dependPopEvent ();
return false;
}
#ifdef DEBUG
debug (5, "Push dependGraph for new event (real push)\n");
if (DEBUGL (5))
{
globalError++;
eprintf ("r%ii%i --> r%ii%i\n", r1, e1, r2, e2);
globalError--;
}
#endif
}
return true;
}
}
//! restore graph to state before previous binding add
void
dependPopEvent (void)
{
if (currentdepgraph->zombie > 0)
{
// zombie pushed
#ifdef DEBUG
debug (5, "Pop dependGraph for new event (zombie pop)\n");
#endif
currentdepgraph->zombie -= 1;
}
else
{
if (currentdepgraph->fornewrun)
{
globalError++;
dependPrint ();
globalError--;
error ("Trying to pop graph created for new run.");
}
else
{
// real graph
#ifdef DEBUG
debug (5, "Pop dependGraph for new event (real pop)\n");
#endif
dependPopGeneric ();
}
}
}
//! Current event to node
int
eventNode (const int r, const int e)
{
return eventtonode (currentdepgraph, r, e);
}
//! Iterate over any preceding events
int
iteratePrecedingEvents (const System sys, int (*func) (int run, int ev),
const int run, const int ev)
{
int run2;
for (run2 = 0; run2 < sys->maxruns; run2++)
{
int ev2;
for (ev2 = 0; ev2 < sys->runs[run2].step; ev2++)
{
if (isDependEvent (run2, ev2, run, ev))
{
if (!func (run2, ev2))
{
return false;
}
}
}
}
return true;
}

View File

@ -1,44 +0,0 @@
#ifndef DEPEND
#define DEPEND
#include "system.h"
/*
* The code here mainly involves an interface for creating graphs etc., but
* most of it is implicit: we just add dependencies/runs and undo them again
* later.
*/
void dependInit (const System sys);
void dependPrint ();
void dependDone (const System sys);
/*
* The push code returns true or false: if false, the operation fails because
* it there is now a cycle in the graph, and there is no need to pop the
* result.
*/
void dependPushRun (const System sys);
void dependPopRun ();
int dependPushEvent (const int r1, const int e1, const int r2, const int e2);
void dependPopEvent ();
/*
* Test/set
*/
int getNode (const int n1, const int n2);
void setNode (const int n1, const int n2);
int isDependEvent (const int r1, const int e1, const int r2, const int e2);
void setDependEvent (const int r1, const int e1, const int r2, const int e2);
/*
* Outside helpers
*/
int hasCycle ();
int eventNode (const int r, const int e);
int nodeCount (void);
int iteratePrecedingEvents (const System sys, int (*func) (int run, int ev),
const int run, const int ev);
#endif

View File

@ -1,47 +0,0 @@
Design Issues for the Model Checker
-----------------------------------
- For secrecy, we can trigger all sends at once. For synchronisation,
this is not the case.
- Modules have to be split up sensibly.
- Although 'knowledge' and 'term matching' seem to different items,
their intertwined workings suggest that they should be implemented
in parallel.
- State generation (as in creating instances) might already allow for
a lot of static analysis.
- We should make a list of required operations. Ingmar's work can serve
as a starting point.
- For now, there will be no parser, and test cases will be input by
hand.
- Synchronisation is more difficult to test, so we focus on secrecy
first. I've got some good ideas on Synchronisation testing though
(with narrowing sets of possible partners). Synchronisation is very
hard to prune, I presume. I have to prove that though ;)
Sketch for secrecy:
SimulateStep(F,M,constraints):
if Empty(F):
return
else:
for (s in PossibleSends):
add s.message to M
if (secrecy violated):
halt
remove s from F
ReadSets = supersetTransitions(F)
for (ReadSet in ReadSets):
for (s in ReadSet):
// dit is vaag
if NonMatch goto next ReadSet
constraint = F,M,match()
SimulateStep(F \ s,M,constraints)

File diff suppressed because it is too large Load Diff

View File

@ -1,6 +0,0 @@
#ifndef DOTOUTPUT
#define DOTOUTPUT
void dotSemiState (const System sys);
#endif

View File

@ -1,94 +0,0 @@
#include <stdlib.h>
#include <stdio.h>
#include <stdarg.h>
#include "error.h"
//! Die from error with exit code
void
error_die (void)
{
exit (EXIT_ERROR);
}
//! print to stderror (must be generic to capture linux variants)
void
vprintfstderr (char *fmt, va_list args)
{
#ifdef USESTDERR
vfprintf (stderr, fmt, args);
#else
// no alternative yet
#endif
}
void
printfstderr (char *fmt, ...)
{
va_list args;
va_start (args, fmt);
vprintfstderr (fmt, args);
va_end (args);
}
//! Print error message header
/**
* Adapted from [K&R2], p. 174
*@todo It would be nice to redirect all output to stderr, which would enable use of termprint etc.
*/
void
error_pre (void)
{
printfstderr ("error: ");
}
//! Print post-error message and die.
/**
* Adapted from [K&R2], p. 174
* Input is comparable to printf, only end of line is not required.
*/
void
error_post (char *fmt, ...)
{
va_list args;
va_start (args, fmt);
vprintfstderr (fmt, args);
printfstderr ("\n");
va_end (args);
exit (EXIT_ERROR);
}
//! Print error message and die.
/**
* Adapted from [K&R2], p. 174
* Input is comparable to printf, only end of line is not required.
*/
void
error (char *fmt, ...)
{
va_list args;
error_pre ();
va_start (args, fmt);
vprintfstderr (fmt, args);
printfstderr ("\n");
va_end (args);
error_die ();
}
//! Print warning
/**
* Input is comparable to printf, only end of line is not required.
*/
void
warning (char *fmt, ...)
{
va_list args;
va_start (args, fmt);
printfstderr ("warning: ");
vprintfstderr (fmt, args);
printfstderr ("\n");
va_end (args);
}

View File

@ -1,19 +0,0 @@
#ifndef ERROR
#define ERROR
//! usestderr is defined iff we use it
#define USESTDERR
//! Types of exit codes
enum exittypes
{ EXIT_NOATTACK = 0, EXIT_ERROR = 1, EXIT_ATTACK = 3 };
void vprintfstderr (char *fmt, va_list args);
void printfstderr (char *fmt, ...);
void error_die (void);
void error_pre (void);
void error_post (char *fmt, ...);
void error (char *fmt, ...);
void warning (char *fmt, ...);
#endif

View File

@ -1,4 +0,0 @@
Test file to see whether it works.
Wow.
New line.
And a better conflict should start here.

View File

@ -1,399 +0,0 @@
/**
*
*@file heuristic.c
*
* Heuristics code for Arachne method
*
*/
#include <float.h>
#include <stdlib.h>
#include "binding.h"
#include "system.h"
#include "specialterm.h"
#include "switches.h"
#include "hidelevel.h"
#include "arachne.h"
#include "error.h"
//! Check whether a binding (goal) is selectable
int
is_goal_selectable (const Binding b)
{
if (b != NULL)
{
if ((!b->blocked) && (!b->done))
{
return true;
}
}
return false;
}
//! Count selectable goals
int
count_selectable_goals (const System sys)
{
List bl;
int n;
n = 0;
bl = sys->bindings;
while (bl != NULL)
{
Binding b;
b = (Binding) bl->data;
if (is_goal_selectable (b))
{
n++;
}
bl = bl->next;
}
return n;
}
//! Return first selectable goal in the list
/**
* The return list entry is either NULL, or a selectable goal.
*/
List
first_selectable_goal (List bl)
{
while (bl != NULL && !is_goal_selectable ((Binding) bl->data))
{
bl = bl->next;
}
return bl;
}
//! Determine whether a term is an open nonce variable
/**
* Does not explore subterms
*/
int
isOpenNonceVar (Term t)
{
t = deVar (t);
if (realTermVariable (t))
{
return inTermlist (t->stype, TERM_Nonce);
}
else
{
return 0;
}
}
//! Count unique open variables in term
/**
*/
int
count_open_variables (const Term t)
{
Termlist tl;
int n;
tl = NULL;
termlistAddVariables (tl, t);
n = 0;
while (tl != NULL)
{
if (!inTermlist (tl->next, t))
{
if (isOpenNonceVar (t))
{
n = n + 1;
}
}
tl = tl->next;
}
termlistDelete (tl);
return n;
}
//! Athena-like factor
/**
* Lower is better (more nonce variables)
*/
float
term_noncevariables_level (const Term t)
{
int onv;
const int enough = 2;
onv = count_open_variables (t);
if (onv >= enough)
{
return 0;
}
else
{
return 1 - (onv / enough);
}
}
//! Determine weight based on hidelevel
float
weighHidelevel (const System sys, const Term t, const float massknow,
const float massprot)
{
switch (hidelevelFlag (sys, t))
{
case HLFLAG_NONE:
return 0;
case HLFLAG_KNOW:
return massknow;
case HLFLAG_PROT:
return massprot;
}
return 1;
}
//! newkeylevel (weighted)
int
newkeylevel (const int level)
{
// keylevel is from { -1,0,1 } where -1 means delay
if (level == 1)
return 0;
else
return 1;
}
//! count local constants
float
term_constcount (const System sys, Term t)
{
int n, total;
float ratio;
int countMe (Term t)
{
if (TermRunid (t) >= 0)
{
total++;
if (!isTermVariable (t))
{
n++;
}
}
return 1;
}
n = 0;
total = 0;
term_iterate_deVar (t, countMe, NULL, NULL, NULL);
if (total == 0)
{
ratio = 1;
}
else
{
ratio = ((total - n) / total);
}
return ratio;
}
//! Determine the weight of a given goal
/**
* 0 to ... (lower is better)
*
* --heuristic has two distint interpretations. If it is 0 or greater, it a
* selection mask. If it is smaller than 0, it is some special tactic.
*
* selection masks for --select-goal
* 1: constrain level of term
* 2: key or not
* 4: consequences determination
* 8: select also single variables (that are not role variables)
* 16: single variables are better
* 32: incorporate keylevel information
*
* special tactics for --select-goal
* -1: random goal selection
*
*/
float
computeGoalWeight (const System sys, const Binding b)
{
float w;
int smode;
Term t;
void erode (const float deltaw)
{
if (smode & 1)
{
w = w + deltaw;
}
smode = smode / 2;
}
// Total weight
w = 0;
// We will shift this mode variable
smode = switches.heuristic;
t = b->term;
// Determine buf_constrain levels
// Bit 0: 1 use hidelevel
erode (2 * weighHidelevel (sys, t, 0.5, 0.5));
// Bit 1: 2 key level (inverted)
erode (0.5 * (1 - b->level));
// Bit 2: 4 constrain level
erode (term_constrain_level (t));
// Bit 3: 8 nonce variables level (Cf. what I think is in Athena)
erode (term_noncevariables_level (t));
// Bit 4: 16 use hidelevel (normal)
erode (1 * weighHidelevel (sys, t, 0.5, 0.5));
// Bit 5: 32 use known nonces (Athena try 2)
erode (term_constcount (sys, t));
// Bit 6: 64 use hidelevel (but only single-weight)
erode (weighHidelevel (sys, t, 0.5, 0.5));
// Bit 7: 128 use hidelevel (quadruple-weight)
erode (4 * weighHidelevel (sys, t, 0.5, 0.5));
// Bit 8: 256 use known nonces (Athena try 2), half weight
erode (0.5 * term_constcount (sys, t));
// Define legal range
if (smode > 0)
error ("--heuristic mode %i is illegal", switches.heuristic);
// Return
return w;
}
//! Goal selection
/**
* Selects the most constrained goal.
*
* Because the list starts with the newest terms, and we use <= (as opposed to <), we
* ensure that for goals with equal constraint levels, we select the oldest one.
*
*/
Binding
select_goal_masked (const System sys)
{
List bl;
Binding best;
float best_weight;
// Find the most constrained goal
if (switches.output == PROOF)
{
indentPrint ();
eprintf ("Listing open goals that might be chosen: ");
}
best_weight = FLT_MAX;
best = NULL;
bl = sys->bindings;
while (bl != NULL)
{
Binding b;
b = (Binding) bl->data;
// Only if not done and not blocked
if (is_goal_selectable (b))
{
if (!isTermVariable (b->term))
{
float w;
w = computeGoalWeight (sys, b);
// Spacing between output
if (switches.output == PROOF && best != NULL)
eprintf (", ");
// Better alternative?
if (w <= best_weight)
{
best_weight = w;
best = b;
if (switches.output == PROOF)
eprintf ("*");
}
if (switches.output == PROOF)
{
termPrint (b->term);
eprintf ("<%.2f>", w);
}
}
}
bl = bl->next;
}
if (switches.output == PROOF)
{
if (best == NULL)
eprintf ("none");
eprintf ("\n");
}
return best;
}
//! Goal selection special case -1: random
/**
* Simply picks an open goal randomly. Has to be careful to skip singular stuff etc.
*/
Binding
select_goal_random (const System sys)
{
int n;
n = count_selectable_goals (sys);
if (n > 0)
{
int choice;
List bl;
// Choose a random goal between 0 and n
choice = rand () % n;
// Fetch it
bl = sys->bindings;
while (choice >= 0)
{
bl = first_selectable_goal (bl);
if (bl == NULL)
{
error ("Random chooser selected a NULL goal.");
}
choice--;
}
return (Binding) bl->data;
}
else
{
return (Binding) NULL;
}
}
//! Goal selection function, generic
Binding
select_goal (const System sys)
{
if (switches.heuristic >= 0)
{
// Masked
return select_goal_masked (sys);
}
else
{
// Special cases
switch (switches.heuristic)
{
case -1:
return select_goal_random (sys);
}
error ("Unknown value (<0) for --goal-select.");
}
return (Binding) NULL;
}

Some files were not shown because too many files have changed in this diff Show More