- Big restructuring of the directories

AUTHORS

@@ -1,31 +0,0 @@
-==================
-# Scyther README #
-==================
-
-----------------
-1. About Scyther
-----------------
-
-Scyther bla Cas andsoforth, bla Lutger, yada yada yada.
-
----------------
-2. Requirements
----------------
-
-Scyther compilation depends on a few external items:
-
-- A C compiler (gcc or anything modern *nixy will do)
-- The Flex and Bison scanner/compiler generation tools.
-
-These two requirements are usually met by default by any modern *nix
-variant, such as GNU/Linux. 
-
-If you want LaTeX output we need
-
-- LaTeX
-- The MSC macro package msc.sty
-
-For the documentation generation, optionally with graphs.
-- Doxygen: http://www.doxygen.org/
-- Dot: http://www.research.att.com/sw/tools/graphviz/
-

Mac-installation-notes.txt

@@ -1,13 +0,0 @@
-Mac
-
-MacPorts (Martijn)
-
-- Easy
-
-Fink (Christoph)
-
-- Lots of stuff problematic, probably easiest to install elementtree locally into the Scyther directory. (package-rev/elementtree into Scyther)
-
-- Leave Python version as is, install dot/graphviz, wx seems to be there already.
-
-- pythonw needed to start for screen access

gui/src/BuildMacIntel-MacPPC.cmake

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

gui/src/BuildMacIntel.cmake

@@ -0,0 +1,11 @@
+################################################################
+# 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")
+

gui/src/BuildMacPPC-MacIntel.cmake

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

gui/src/BuildMacPPC.cmake

@@ -0,0 +1,11 @@
+################################################################
+# 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")
+

gui/src/BuildPlatform.cmake

@@ -0,0 +1,36 @@
+################################################################
+# 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})
+

gui/src/BuildUnix-Win32.cmake

@@ -0,0 +1,15 @@
+################################################################
+# 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})
+

gui/src/BuildUnix.cmake

@@ -0,0 +1,12 @@
+################################################################
+# 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})
+

gui/src/CMakeLists.txt

@@ -0,0 +1,37 @@
+################################################################
+# 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)
+

gui/src/FindBISON.cmake

@@ -0,0 +1,33 @@
+# - 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)
+

gui/src/FindFLEX.cmake

@@ -0,0 +1,33 @@
+# - 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)
+

gui/src/GetOS.cmake

@@ -0,0 +1,43 @@
+################################################################
+# 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}")
+

gui/src/Makefile-fallback

@@ -0,0 +1,86 @@
+#
+#	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
+

gui/src/SVNVersion.cmake

@@ -0,0 +1,58 @@
+################################################################
+# 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)
+

gui/src/ScannerParser.cmake

@@ -0,0 +1,41 @@
+################################################################
+# 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)
+
+

gui/src/Scyther.dev

@@ -0,0 +1,789 @@
+[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=
+

gui/src/UniversalBinary.cmake

@@ -0,0 +1,42 @@
+################################################################
+# 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)
+

gui/src/arachne.h

@@ -0,0 +1,20 @@
+#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

gui/src/attacktemplate.tex

@@ -0,0 +1,61 @@
+\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}

gui/src/binding.c

@@ -0,0 +1,617 @@
+/**
+ * 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;
+}

gui/src/binding.h

@@ -0,0 +1,53 @@
+#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

gui/src/bugs.txt

@@ -0,0 +1,119 @@
+--+++ 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.
+

gui/src/build.sh

@@ -0,0 +1,16 @@
+#!/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
+

gui/src/claim.h

@@ -0,0 +1,18 @@
+#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

gui/src/color.c

@@ -0,0 +1,39 @@
+/** @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)
+{
+}

gui/src/color.h

@@ -0,0 +1,12 @@
+#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

gui/src/compile.txt

@@ -0,0 +1,18 @@
+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.
+

gui/src/compiler.h

@@ -0,0 +1,26 @@
+#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

gui/src/copy2gui.sh

@@ -0,0 +1,11 @@
+#!/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
+

gui/src/cost.c

@@ -0,0 +1,74 @@
+/**
+ *
+ *@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;
+}

gui/src/cost.h

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

gui/src/debug.c

@@ -0,0 +1,52 @@
+/**
+ *@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
+}

gui/src/debug.h

@@ -0,0 +1,10 @@
+#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

gui/src/depend.c

@@ -0,0 +1,569 @@
+/**
+ * @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;
+}

gui/src/depend.h

@@ -0,0 +1,44 @@
+#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

gui/src/design.txt

@@ -0,0 +1,47 @@
+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)
+						
+				
+

gui/src/dotout.h

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

gui/src/error.c

@@ -0,0 +1,94 @@
+#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);
+}

gui/src/error.h

@@ -0,0 +1,19 @@
+#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

gui/src/git-test.txt

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

gui/src/heuristic.c

@@ -0,0 +1,399 @@
+/**
+ *
+ *@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;
+}

gui/src/heuristic.h

@@ -0,0 +1,9 @@
+#ifndef HEURISTIC
+#define HEURISTIC
+
+#include "system.h"
+#include "binding.h"
+
+Binding select_goal (const System sys);
+
+#endif

gui/src/hidelevel.c

@@ -0,0 +1,261 @@
+/** @file hidelevel.c \brief Hidelevel lemma base functions.
+ *
+ * The Hidelevel lemma is fairly complex and so it requires some buffering,
+ * instead of fully recomputing the required data each time again.
+ */
+
+#include <stdlib.h>
+#include <limits.h>
+#include "hidelevel.h"
+#include "system.h"
+#include "debug.h"
+
+extern Term TERM_Hidden;
+
+//! hide level within protocol
+unsigned int
+protocolHidelevel (const System sys, const Term t)
+{
+  unsigned int minlevel;
+
+  int itsends (const Protocol p, const Role r)
+  {
+    int sends (Roledef rd)
+    {
+      if (rd->type == SEND)
+	{
+	  unsigned int l;
+
+	  l = termHidelevel (t, rd->from);
+	  if (l < minlevel)
+	    minlevel = l;
+	  l = termHidelevel (t, rd->to);
+	  if (l < minlevel)
+	    minlevel = l;
+	  l = termHidelevel (t, rd->message);
+	  if (l < minlevel)
+	    minlevel = l;
+	}
+      return true;
+    }
+
+    roledef_iterate_events (r->roledef, sends);
+    return true;
+  }
+
+  minlevel = INT_MAX;
+  iterateRoles (sys, itsends);
+
+  return minlevel;
+}
+
+//! hide level within initial knowledge
+unsigned int
+knowledgeHidelevel (const System sys, const Term t)
+{
+  unsigned int minlevel;
+  Termlist tl;
+
+  minlevel = INT_MAX;
+  tl = knowledgeSet (sys->know);
+  while (tl != NULL)
+    {
+      unsigned int l;
+
+      l = termHidelevel (t, tl->term);
+      if (l < minlevel)
+	{
+	  minlevel = l;
+	}
+      tl = tl->next;
+    }
+  termlistDelete (tl);
+
+  return minlevel;
+}
+
+//! Check hide levels
+void
+hidelevelCompute (const System sys)
+{
+  Termlist tl;
+
+  sys->hidden = NULL;
+  tl = sys->globalconstants;
+
+  // Add 'hidden' terms
+  tl = termlistAdd (tl, TERM_Hidden);
+
+#ifdef DEBUG
+  if (DEBUGL (4))
+    {
+      eprintf ("Global constants: ");
+      termlistPrint (tl);
+      eprintf ("\n");
+    }
+#endif
+
+  while (tl != NULL)
+    {
+      unsigned int l1, l2, l;
+
+      l1 = knowledgeHidelevel (sys, tl->term);
+      l2 = protocolHidelevel (sys, tl->term);
+      if (l1 < l2)
+	{
+	  l = l1;
+	}
+      else
+	{
+	  l = l2;
+	}
+
+      // Interesting only if higher than zero
+      if (l > 0)
+	{
+	  Hiddenterm ht;
+
+	  ht = (Hiddenterm) malloc (sizeof (struct hiddenterm));
+	  ht->term = tl->term;
+	  ht->hideminimum = l;
+	  ht->hideprotocol = l2;
+	  ht->hideknowledge = l1;
+	  ht->next = sys->hidden;
+	  sys->hidden = ht;
+
+#ifdef DEBUG
+	  if (DEBUGL (5))
+	    {
+	      eprintf ("Added possibly interesting term: ");
+	      termPrint (tl->term);
+	      eprintf ("; know %i, prot %i\n", l1, l2);
+	    }
+#endif
+	}
+
+      tl = tl->next;
+    }
+}
+
+//! Determine flag from parameters
+unsigned int
+hidelevelParamFlag (unsigned int l, unsigned int lmin, unsigned int lprot,
+		    unsigned int lknow)
+{
+  // Given the parameters, determine where the term with hidelevel l could be generated from.
+  if (l < lmin)
+    {
+      return HLFLAG_NONE;
+    }
+  else
+    {
+      // One should work (at least)
+      if (l < lprot)
+	{
+	  // Know should be possible
+	  return HLFLAG_KNOW;
+	}
+      else
+	{
+	  // Prot can, know also?
+	  if (l < lknow)
+	    {
+	      // Nope, just prot
+	      return HLFLAG_PROT;
+	    }
+	  else
+	    {
+	      // Both
+	      return HLFLAG_BOTH;
+	    }
+	}
+    }
+}
+
+//! Given a term, iterate over all factors
+int
+iterate_interesting (const System sys, const Term goalterm, int (*func) ())
+{
+  Hiddenterm ht;
+
+  ht = sys->hidden;
+  while (ht != NULL)
+    {
+      unsigned int l;
+      // Test the goalterm for occurrences of this
+
+      l = termHidelevel (ht->term, goalterm);
+      if (l < INT_MAX)
+	{
+	  if (!func (l, ht->hideminimum, ht->hideprotocol, ht->hideknowledge))
+	    {
+	      return false;
+	    }
+	}
+
+      ht = ht->next;
+    }
+  return true;
+}
+
+//! Determine whether a goal might be interesting from the viewpoint of hide levels (the highest minimum is best)
+int
+hidelevelInteresting (const System sys, const Term goalterm)
+{
+  int uninteresting (unsigned int l, unsigned int lmin, unsigned int lprot,
+		     unsigned int lknow)
+  {
+    if (lmin > 0)
+      {
+	// anything higher than usual is interesting :)
+	return false;
+      }
+    return true;
+  }
+
+  return !iterate_interesting (sys, goalterm, uninteresting);
+}
+
+//! Determine whether a goal is impossible to satisfy because of the hidelevel lemma.
+int
+hidelevelImpossible (const System sys, const Term goalterm)
+{
+  int possible (unsigned int l, unsigned int lmin, unsigned int lprot,
+		unsigned int lknow)
+  {
+    if (l < lmin)
+      {
+	// impossible, abort!
+	return false;
+      }
+    return true;
+  }
+
+  return !iterate_interesting (sys, goalterm, possible);
+}
+
+//! Return flag on the basis of the Hidelevel lemma
+unsigned int
+hidelevelFlag (const System sys, const Term goalterm)
+{
+  unsigned int flag;
+
+  int getflag (unsigned int l, unsigned int lmin, unsigned int lprot,
+	       unsigned int lknow)
+  {
+    // Determine new flag
+    flag = flag | hidelevelParamFlag (l, lmin, lprot, lknow);
+
+    // Should we proceed?
+    if (flag == HLFLAG_NONE)
+      {
+	// abort iteration: it cannot get worse
+	return false;
+      }
+    return true;
+  }
+
+  flag = HLFLAG_BOTH;
+  iterate_interesting (sys, goalterm, getflag);
+  return flag;
+}

gui/src/hidelevel.h

@@ -0,0 +1,27 @@
+#ifndef HIDELEVELS
+#define HIDELEVELS
+
+#include "term.h"
+#include "system.h"
+
+/*
+ * Flags for hidelevel lemma
+ *
+ * Use binary or (|) to compose results: by default, a term can be satisfied by
+ * both the protocol and the initial knowledge.
+ */
+#define HLFLAG_BOTH 0
+#define HLFLAG_KNOW 1
+#define HLFLAG_PROT 2
+#define HLFLAG_NONE 3
+
+/*
+ * The structure hiddenterm/Hiddenterm is defined in system.h
+ */
+
+void hidelevelCompute (const System sys);
+int hidelevelInteresting (const System sys, const Term goalterm);
+int hidelevelImpossible (const System sys, const Term goalterm);
+unsigned int hidelevelFlag (const System sys, const Term goalterm);
+
+#endif

gui/src/hidelevel.txt

@@ -0,0 +1,31 @@
+Implemented: 
+
+- scans
+- test functions (in hidelevel.c)
+
+TODO:
+
+- use test functions (impossible for pruning, interesting for goal selection heuristic)
+- state count display switch for comparisons
+- consider adding info for goal stuff (only from M_0, not by create)
+
+*******************************************************************
+
+roivas:~scyther% ./scyther ccitt509-1c.spdl
+Global constants: [te, ne, Eve, Bob, Alice, unhash, sk, hash, pk]
+
+Possibly interesting term: unhash; know 2147483647, prot 2147483647
+Possibly interesting term: sk; know 1, prot 2
+
+
+roivas:~scyther% ./scyther yahalom.spdl
+warning: variable T was declared in role yahalom,R but never used in a read event.
+Global constants: [Simon, Bob, Alice, Compromised, Fresh, k]
+
+Possibly interesting term: k; know 2147483647, prot 2
+
+
+roivas:~scyther% ./scyther ns3.spdl
+Global constants: [Eve, sk, pk]
+
+Possibly interesting term: sk; know 1, prot 2147483647

gui/src/intruderknowledge.c

@@ -0,0 +1,197 @@
+/**
+ * Initial intruder knowledge computation.
+ */
+
+#include "intruderknowledge.h"
+
+//! Add a (copy of) a term to the intruder knowledge
+void
+addSTerm (const System sys, Term t, Termlist fromlist, Termlist tolist)
+{
+  Term t2;
+
+  t2 = termLocal (t, fromlist, tolist);
+
+  if (switches.check)
+    {
+      globalError++;
+      eprintf ("[ Adding ");
+      termPrint (t2);
+      eprintf (" to the initial intruder knowledge]\n");
+      globalError--;
+    }
+}
+
+//! Unfold the term for all possible options
+void
+addEnumTerm (const System sys, Term t, Term actor, Termlist todo,
+	     Termlist fromlist, Termlist tolist)
+{
+  if (todo == NULL)
+    {
+      addSTerm (sys, t, fromlist, tolist);
+    }
+  else
+    {
+      if (termSubTerm (t, todo->term))
+	{
+	  // Occurs, we have to iterate
+	  void iterateThis (Term to)
+	  {
+	    tolist = termlistPrepend (tolist, to);
+
+	    addEnumTerm (sys, t, actor, todo->next, fromlist, tolist);
+
+	    tolist = termlistDelTerm (tolist);
+	  }
+
+	  fromlist = termlistPrepend (fromlist, todo->term);
+	  if (isTermEqual (todo->term, actor))
+	    {
+	      // Untrusted agents only
+	      Termlist tl;
+
+	      for (tl = sys->untrusted; tl != NULL; tl = tl->next)
+		{
+		  iterateThis (tl->term);
+		}
+	    }
+	  else
+	    {
+	      // any agents
+	      Termlist tl;
+
+	      for (tl = sys->agentnames; tl != NULL; tl = tl->next)
+		{
+		  iterateThis (tl->term);
+		}
+	    }
+	  fromlist = termlistDelTerm (fromlist);
+	}
+      else
+	{
+	  // Simply proceed to next
+	  addEnumTerm (sys, t, actor, todo->next, fromlist, tolist);
+	}
+    }
+}
+
+//! Does t contain any of sublist?
+int
+anySubTerm (Term t, Termlist sublist)
+{
+  while (sublist != NULL)
+    {
+      if (termSubTerm (t, sublist->term))
+	{
+	  return true;
+	}
+      sublist = sublist->next;
+    }
+  return false;
+}
+
+void
+initialIntruderKnowledge (const System sys)
+{
+  /*
+   * display initial role knowledge
+   */
+  int deriveFromRole (Protocol p, Role r)
+  {
+    void addListKnowledge (Termlist tl, Term actor)
+    {
+      void addTermKnowledge (Term t)
+      {
+	if (anySubTerm (t, p->rolenames))
+	  {
+	    Term f;
+	    // Has rolename subterms. We have to enumerate those.
+	    /**
+	     * Hack. Enumerating is not always good (or even desirable).
+	     * If some I knows sk(I), sk should not be in the intruder knowledge.
+	     * But for hash(I), we typically would have h; but if it is never used differently, it would suffice.
+	     * To summarize, the operational semantics definition is perfectly fine, but maybe a bit strict sometimes.
+	     *
+	     * The hack is that if function application:
+	    */
+	    f = getTermFunction (t);
+	    if (f != NULL)
+	      {
+		// it's a function, right. So we see whether it is public. It is if it does not contain the actor...
+		if (!termSubTerm (t, actor))
+		  {
+		    // no actor, then nothing secret I guess.
+		    addSTerm (sys, f, NULL, NULL);
+		    return;
+		  }
+		else
+		  {
+		    // has actor. but does it contain even more?
+
+		    int allagents (Term t)
+		    {
+		      if (!inTermlist (sys->agentnames, t))
+			{
+			  if (!inTermlist (p->rolenames, t))
+			    {
+			      return false;
+			    }
+			}
+		      return true;
+		    }
+
+		    if (!term_iterate_leaves (TermOp (t), allagents))
+		      {
+			// something else as well, so that probably means a hash or something like that.
+			addSTerm (sys, f, NULL, NULL);
+			return;
+		      }
+		  }
+	      }
+	    // otherwise, we enumerate
+	    addEnumTerm (sys, t, actor, p->rolenames, NULL, NULL);
+	  }
+	else
+	  {
+	    // No actor subterm. Simply add.
+	    addSTerm (sys, t, NULL, NULL);
+	  }
+      }
+
+      while (tl != NULL)
+	{
+	  addTermKnowledge (tl->term);
+	  tl = tl->next;
+	}
+    }
+
+    if (switches.check)
+      {
+	globalError++;
+	eprintf ("Role ");
+	termPrint (r->nameterm);
+	eprintf (" knows ");
+	termlistPrint (r->knows);
+	eprintf ("\n");
+	globalError--;
+      }
+    addListKnowledge (r->knows, r->nameterm);
+    return true;
+  }
+
+  if (switches.check)
+    {
+      globalError++;
+      eprintf ("Computing initial intruder knowledge.\n\n");
+      eprintf ("Agent names      : ");
+      termlistPrint (sys->agentnames);
+      eprintf ("\n");
+      eprintf ("Untrusted agents : ");
+      termlistPrint (sys->untrusted);
+      eprintf ("\n");
+      globalError--;
+    }
+
+  iterateRoles (sys, deriveFromRole);
+}

gui/src/intruderknowledge.h

@@ -0,0 +1,9 @@
+#ifndef INTRUDERKNOWLEDGE
+#define INTRUDERKNOWLEDGE
+
+#include "system.h"
+#include "switches.h"
+
+void initialIntruderKnowledge (const System sys);
+
+#endif

gui/src/knowledge.c

@@ -0,0 +1,550 @@
+/**
+ *@file knowledge.c
+ *\brief Procedures concerning knowledge structures.
+ *
+ * The main issue of this code is to maintain the minimal property of the knowledge set.
+ */
+#include <stdlib.h>
+#include <stdio.h>
+#include "termlist.h"
+#include "knowledge.h"
+#include "system.h"
+#include "debug.h"
+#include "error.h"
+
+/*
+ * Knowledge stuff
+ *
+ * Note that a really weird thing is going on involving unpropagated substitutions.
+ * Idea:
+ *
+ * 1. Substitute terms by filling in ->subst.
+ * Now, either:
+ * 2a. Undo this by knowledgeUndo.
+ * 2b. Propagate it, modifying the knowledge beyond repair by knowledgeSubstDo. Now inKnowledge works again.
+ * 2c. inKnowledge/knowledgeSet if something is in the knowledge: this does not consider the substitutions!, and 
+ *     they now have some overhead.
+ */
+
+//! Open knowledge code.
+void
+knowledgeInit (void)
+{
+  return;
+}
+
+//! Close knowledge code.
+void
+knowledgeDone (void)
+{
+}
+
+//! Allocate a fresh memory block the size of a knowledge struct.
+/**
+ * Memory will not be initialized.
+ *@return Pointer to a fresh memory block.
+ */
+Knowledge
+makeKnowledge ()
+{
+  return (Knowledge) malloc (sizeof (struct knowledge));
+}
+
+//! Create a new empty knowledge structure.
+/**
+ *@return Pointer to an empty knowledge structure.
+ */
+Knowledge
+emptyKnowledge ()
+{
+  Knowledge know;
+
+  know = makeKnowledge ();
+  know->basic = NULL;
+  know->encrypt = NULL;
+  know->inverses = NULL;
+  know->vars = NULL;
+  return know;
+}
+
+//! Duplicate a knowledge structure.
+/**
+ * Makes copies using termlistShallow() of knowledge::basic, knowledge::encrypt and 
+ * knowledge::vars.
+ * For the inverses, only the pointer is copied.
+ *@param know The knowledge structure to be copied.
+ *@return A pointer to a new memory struct.
+ *\sa termlistShallow(), knowledgeDelete()
+ */
+Knowledge
+knowledgeDuplicate (Knowledge know)
+{
+  Knowledge newknow;
+
+  if (know == NULL)
+    {
+      warning ("Trying to copy empty knowledge.");
+      return NULL;
+    }
+  newknow = makeKnowledge ();
+  newknow->basic = termlistShallow (know->basic);
+  newknow->encrypt = termlistShallow (know->encrypt);
+  newknow->vars = termlistShallow (know->vars);
+  newknow->inverses = know->inverses;
+  return newknow;
+}
+
+//! Delete a knowledge set.
+/**
+ * Typically used to destroy something made with knowledgeDuplicate().
+ *\sa knowledgeDuplicate()
+ */
+void
+knowledgeDelete (Knowledge know)
+{
+  if (know != NULL)
+    {
+      termlistDelete (know->basic);
+      termlistDelete (know->encrypt);
+      termlistDelete (know->vars);
+      free (know);
+    }
+}
+
+//! Destroy a knowledge set.
+/**
+ * Unlike knowledgeDelete(), uses termlistDestroy() to remove knowledge::basic, 
+ * knowledge::encrypt and knowledge::vars substructures.
+ *\sa knowledgeDelete()
+ */
+void
+knowledgeDestroy (Knowledge know)
+{
+  if (know != NULL)
+    {
+      termlistDestroy (know->basic);
+      termlistDestroy (know->encrypt);
+      termlistDestroy (know->vars);
+      // termlistDestroy(know->inverses);
+      free (know);
+    }
+}
+
+//! Add a term to a knowledge set.
+/**
+ *@param know The knowledge set.
+ *@param term The term to be added.
+ *@return True iff the term was actually new, and added.
+ */
+int
+knowledgeAddTerm (Knowledge know, Term term)
+{
+  if (know == NULL)
+    {
+      warning ("Trying to add term to uninitialised (NULL) Know pointer.");
+      return 1;
+    }
+  if (term == NULL)
+    return 0;
+
+  term = deVar (term);
+
+  /* for tuples, simply recurse for components */
+  if (isTermTuple (term))
+    {
+      int status;
+
+      status = knowledgeAddTerm (know, TermOp1 (term));
+      return knowledgeAddTerm (know, TermOp2 (term)) || status;
+    }
+
+  /* test whether we knew it before */
+  if (inKnowledge (know, term))
+    return 0;
+
+  /* adding variables? */
+  know->vars = termlistAddVariables (know->vars, term);
+
+  knowledgeSimplify (know, term);
+  if (isTermLeaf (term))
+    {
+      know->basic = termlistAdd (know->basic, term);
+    }
+  if (term->type == ENCRYPT)
+    {
+      Term invkey = inverseKey (know->inverses, TermKey (term));
+      if (inKnowledge (know, invkey))
+	{
+	  /* we can decrypt it */
+	  knowledgeAddTerm (know, TermOp (term));
+	  if (!inKnowledge (know, TermKey (term)))
+	    {
+	      /* we know the op now, but not the key, so add it anyway */
+	      know->encrypt = termlistAdd (know->encrypt, term);
+	    }
+	}
+      else
+	{
+	  /* we cannot decrypt it, and from the initial test we know we could not construct it */
+	  know->encrypt = termlistAdd (know->encrypt, term);
+	}
+      termDelete (invkey);
+    }
+  return 1;
+}
+
+
+//! Try to simplify knowledge based on a term.
+/**
+ *@param know A knowledge set.
+ *@param key A key, i.e. it can decrypt anything that was encrypted with term^{-1}.
+ */
+void
+knowledgeSimplify (Knowledge know, Term key)
+{
+  Termlist tldecrypts = NULL;
+  Termlist scan = know->encrypt;
+  Term invkey = inverseKey (know->inverses, key);
+
+  while (scan != NULL)
+    {
+      if (isTermEqual (TermKey (scan->term), invkey))
+	{
+	  tldecrypts = termlistAdd (tldecrypts, TermOp (scan->term));
+	  know->encrypt = termlistDelTerm (scan);
+	  scan = know->encrypt;
+	}
+      else
+	scan = scan->next;
+    }
+  termDelete (invkey);
+  knowledgeAddTermlist (know, tldecrypts);
+  termlistDelete (tldecrypts);
+}
+
+//! Add a termlist to the knowledge.
+/*
+ *@return True iff there was at least one new item.
+ *\sa knowledgeAddTerm()
+ */
+int
+knowledgeAddTermlist (Knowledge know, Termlist tl)
+{
+  int flag = 0;
+
+  while (tl != NULL)
+    {
+      flag = knowledgeAddTerm (know, tl->term) || flag;
+      tl = tl->next;
+    }
+  return flag;
+}
+
+//! Add an inverse pair to the knowledge
+void
+knowledgeAddInverse (Knowledge know, Term t1, Term t2)
+{
+  know->inverses = termlistAdd (know->inverses, t1);
+  know->inverses = termlistAdd (know->inverses, t2);
+  return;
+}
+
+//! Set an inverse pair list for the knowledge.
+/**
+ * List pointer is simply copied, so don't delete it later!
+ */
+void
+knowledgeSetInverses (Knowledge know, Termlist tl)
+{
+  know->inverses = tl;
+}
+
+//! Is a term a part of the knowledge?
+/**
+ *@param know The knowledge set.
+ *@param term The term to be inferred.
+ *@return True iff the term can be inferred from the knowledge set.
+ */
+int
+inKnowledge (const Knowledge know, Term term)
+{
+  mindwipe (know, inKnowledge (know, term));
+
+  /* if there is no term, then it's okay 'fur sure' */
+  if (term == NULL)
+    return 1;
+  /* if there is a term, but no knowledge, we're in trouble */
+  if (know == NULL)
+    return 0;
+
+  term = deVar (term);
+  if (isTermLeaf (term))
+    {
+      return inTermlist (know->basic, term);
+    }
+  if (term->type == ENCRYPT)
+    {
+      return inTermlist (know->encrypt, term) ||
+	(inKnowledge (know, TermKey (term))
+	 && inKnowledge (know, TermOp (term)));
+    }
+  if (term->type == TUPLE)
+    {
+      return (inTermlist (know->encrypt, term) ||
+	      (inKnowledge (know, TermOp1 (term)) &&
+	       inKnowledge (know, TermOp2 (term))));
+    }
+  return 0;			/* unrecognized term type, weird */
+}
+
+//! Compare two knowledge sets.
+/**
+ * This does not check currently for equivalence of inverse sets, which it should.
+ *@return True iff both knowledge sets are equal.
+ */
+int
+isKnowledgeEqual (Knowledge know1, Knowledge know2)
+{
+  if (know1 == NULL || know2 == NULL)
+    {
+      if (know1 == NULL && know2 == NULL)
+	return 1;
+      else
+	return 0;
+    }
+  if (!isTermlistEqual (know1->encrypt, know2->encrypt))
+    return 0;
+  return isTermlistEqual (know1->basic, know2->basic);
+}
+
+//! Print a knowledge set.
+void
+knowledgePrint (Knowledge know)
+{
+  indent ();
+  if (know == NULL)
+    {
+      eprintf ("Empty.\n");
+      return;
+    }
+  eprintf (" [Basic]: ");
+  termlistPrint (know->basic);
+  eprintf ("\n");
+  indent ();
+  eprintf (" [Encrp]: ");
+  termlistPrint (know->encrypt);
+  eprintf ("\n");
+  indent ();
+  eprintf (" [Vars]: ");
+  termlistPrint (know->vars);
+  eprintf ("\n");
+}
+
+//! Print a knowledge set, short version (no newline)
+void
+knowledgePrintShort (const Knowledge know)
+{
+  indent ();
+  if (know == NULL)
+    {
+      eprintf ("Empty");
+      return;
+    }
+
+  if (know->basic != NULL)
+    {
+      termlistPrint (know->basic);
+      if (know->encrypt != NULL);
+      {
+	eprintf (", ");
+      }
+    }
+  if (know->encrypt != NULL)
+    {
+      termlistPrint (know->encrypt);
+    }
+}
+
+//! Print the inverses list of a knowledge set.
+void
+knowledgeInversesPrint (Knowledge know)
+{
+  Termlist tl;
+  int after = 0;
+
+  if (know == NULL)
+    {
+      eprintf ("Empty knowledge.");
+      return;
+    }
+
+  tl = knowledgeGetInverses (know);
+  if (tl == NULL)
+    {
+      eprintf ("None.");
+    }
+  else
+    {
+      while (tl != NULL && tl->next != NULL)
+	{
+	  if (after)
+	    {
+	      eprintf (",");
+	    }
+	  eprintf ("(");
+	  termPrint (tl->term);
+	  eprintf (",");
+	  termPrint (tl->next->term);
+	  eprintf (")");
+	  after = 1;
+	  tl = tl->next->next;
+	}
+    }
+}
+
+//! Yield the set of representatives for the knowledge.
+/**
+ * Note: this is a shallow copy, and needs to be termlistDelete'd.
+ *\sa termlistDelete()
+ */
+Termlist
+knowledgeSet (const Knowledge know)
+{
+  Termlist tl1, tl2;
+
+  tl1 = termlistShallow (know->basic);
+  tl2 = termlistShallow (know->encrypt);
+  return termlistConcat (tl1, tl2);
+}
+
+//! Get the inverses pointer of the knowledge.
+/**
+ * Essentially the inverse function of knowledgeSetInverses()
+ */
+Termlist
+knowledgeGetInverses (const Knowledge know)
+{
+  if (know == NULL)
+    return NULL;
+  else
+    return know->inverses;
+}
+
+//! Get all basic elements in the knowledge
+/**
+ * This function is used by match_basic, to determine all basic elements in the knowledge set.
+ * Most of the time this doesn't even change, so it might become a parameter of knowledge.
+ * For now, this will have to do.
+ *
+ *@todo Investigate whether the basics in the knowledge set should be a parameter of knowledge, as it doesn't change very often.
+ */
+__inline__ Termlist
+knowledgeGetBasics (const Knowledge know)
+{
+  return termlistAddBasics (termlistAddBasics (NULL, know->basic),
+			    know->encrypt);
+}
+
+//! check whether any substitutions where made in a knowledge set.
+/**
+ * Typically, when a substitution is made, a knowledge set has to be reconstructed.
+ * This procedure detects this by checking knowledge::vars.
+ *@return True iff an open variable was later closed by a substitution.
+ *\sa knowledgeReconstruction()
+ */
+int
+knowledgeSubstNeeded (const Knowledge know)
+{
+  Termlist tl;
+
+  if (know == NULL)
+    return 0;
+  tl = know->vars;
+  while (tl != NULL)
+    {
+      if (tl->term->subst != NULL)
+	return 1;
+      tl = tl->next;
+    }
+  return 0;
+}
+
+//! Reconstruct a knowledge set.
+/**
+ * This is useful after e.g. substitutions.
+ * Just rebuilds the knowledge in a new (shallow) copy.
+ *@return The pointer to the new knowledge.
+ *\sa knowledgeSubstNeeded()
+ */
+Knowledge
+knowledgeReconstruction (const Knowledge know)
+{
+  Knowledge newknow = emptyKnowledge ();
+
+  newknow->inverses = know->inverses;
+  knowledgeAddTermlist (newknow, know->basic);
+  knowledgeAddTermlist (newknow, know->encrypt);
+  return newknow;
+}
+
+//! Propagate any substitutions just made.
+/**
+ * This usually involves reconstruction of the complete knowledge, which is
+ * 'cheaper' than a thorough analysis, so we always make a copy.
+ *\sa knowledgeReconstruction()
+ */
+Knowledge
+knowledgeSubstDo (const Knowledge know)
+{
+  /* otherwise a copy (for deletion) is returned. */
+  return knowledgeReconstruction (know);
+}
+
+//! Undo substitutions that were not propagated yet.
+/**
+ * Undo the substitutions just made. Note that this does not work anymore after knowledgeSubstDo()
+ */
+void
+knowledgeSubstUndo (const Knowledge know)
+{
+  Termlist tl;
+
+  tl = know->vars;
+  while (tl != NULL)
+    {
+      tl->term->subst = NULL;
+      tl = tl->next;
+    }
+}
+
+//! Yield the minimal set of terms that are in some knowledge, but not in some other set.
+/**
+ * Yield a termlist (or NULL) that represents the reduced items that are
+ * in the new set, but not in the old one.
+ *@param oldk The old knowledge.
+ *@param newk The new knowledge, possibly with new terms.
+ *@return A termlist of miminal terms in newk, but not in oldk.
+ */
+
+Termlist
+knowledgeNew (const Knowledge oldk, const Knowledge newk)
+{
+  Termlist newtl;
+
+  void addNewStuff (Termlist tl)
+  {
+    while (tl != NULL)
+      {
+	if (!inKnowledge (oldk, tl->term))
+	  {
+	    newtl = termlistAdd (newtl, tl->term);
+	  }
+	tl = tl->next;
+      }
+  }
+
+  newtl = NULL;
+  addNewStuff (newk->basic);
+  addNewStuff (newk->encrypt);
+  return newtl;
+}

gui/src/knowledge.h

@@ -0,0 +1,75 @@
+#ifndef KNOWLEDGE
+#define KNOWLEDGE
+
+#include "term.h"
+#include "termlist.h"
+
+//! Knowledge structure.
+/**
+ * Contains a miminal representation of a knowledge set.
+ */
+struct knowledge
+{
+  //! A list of non-encrypted terms.
+  Termlist basic;
+  //! A list of terms encrypted, such that the inverse is not in the knowledge set.
+  Termlist encrypt;
+  //! List of inverse pairs (thus length of list is even)
+  Termlist inverses;
+  //! List of open variables in the knowledge set.
+  /**
+   * This list is used to determine whether the knowledge needs to be rewritten.
+   * If a new substitution is done, one of the elements of this list will become closed,
+   * and we need to reconstruct the knowledge set.
+   */
+  Termlist vars;		// special: denotes unsubstituted variables
+};
+
+//! Shorthand for knowledge pointer.
+typedef struct knowledge *Knowledge;
+
+void knowledgeInit (void);
+void knowledgeDone (void);
+Knowledge makeKnowledge ();
+Knowledge emptyKnowledge ();
+Knowledge knowledgeDuplicate (Knowledge know);
+void knowledgeDelete (Knowledge know);
+void knowledgeDestroy (Knowledge know);
+int knowledgeAddTerm (Knowledge know, Term term);
+int knowledgeAddTermlist (Knowledge know, Termlist tl);
+void knowledgeAddInverse (Knowledge know, Term t1, Term t2);
+void knowledgeSetInverses (Knowledge know, Termlist tl);
+void knowledgeSimplify (Knowledge know, Term decryptkey);
+int inKnowledge (const Knowledge know, Term term);
+void knowledgePrint (Knowledge know);
+void knowledgePrintShort (const Knowledge know);
+void knowledgeInversesPrint (Knowledge know);
+int isKnowledgeEqual (Knowledge know1, Knowledge know2);
+Termlist knowledgeSet (const Knowledge know);
+Termlist knowledgeGetInverses (const Knowledge know);
+Termlist knowledgeGetBasics (const Knowledge know);
+int knowledgeSubstNeeded (const Knowledge know);
+Knowledge knowledgeSubstDo (const Knowledge know);
+void knowledgeSubstUndo (const Knowledge know);
+Termlist knowledgeNew (const Knowledge oldk, const Knowledge newk);
+
+//! Harnass macro for recursive procedures.
+#define mindwipe(k,recurse) \
+        Termlist tl; \
+	int flag; \
+	if (k != NULL && k->vars != NULL) { \
+		tl = k->vars; \
+		while (tl != NULL) { \
+			if (tl->term->subst != NULL) { \
+				Term oldsubst = tl->term->subst; \
+				tl->term->subst = NULL; \
+				flag = recurse; \
+				tl->term->subst = oldsubst; \
+				return flag; \
+			} \
+			tl = tl->next; \
+		} \
+	} \
+
+
+#endif

gui/src/label.c

@@ -0,0 +1,86 @@
+/**
+ * Label info
+ */
+
+#include <stdlib.h>
+#include "term.h"
+#include "label.h"
+#include "list.h"
+#include "system.h"
+
+//! Retrieve rightmost thing of label
+Term
+rightMostTerm (Term t)
+{
+  if (t != NULL)
+    {
+      t = deVar (t);
+      if (realTermTuple (t))
+	{
+	  return rightMostTerm (TermOp2 (t));
+	}
+    }
+  return t;
+}
+
+//! Create a new labelinfo node
+Labelinfo
+label_create (const Term label, const Protocol protocol)
+{
+  Labelinfo li;
+  Term tl;
+
+  li = (Labelinfo) malloc (sizeof (struct labelinfo));
+  li->label = label;
+  li->protocol = protocol;
+  li->sendrole = NULL;
+  li->readrole = NULL;
+  // Should we ignore it?
+  li->ignore = false;
+  tl = rightMostTerm (label);
+  if (tl != NULL)
+    {
+      if (TermSymb (tl)->text[0] == '!')
+	{
+	  li->ignore = true;
+	}
+    }
+  return li;
+}
+
+//! Destroy a labelinfo node
+void
+label_destroy (Labelinfo linfo)
+{
+  free (linfo);
+}
+
+//! Given a list of label infos, yield the correct one or NULL
+Labelinfo
+label_find (List labellist, const Term label)
+{
+  Labelinfo linfo;
+
+  int label_find_scan (void *data)
+  {
+    Labelinfo linfo_scan;
+
+    linfo_scan = (Labelinfo) data;
+    if (isTermEqual (label, linfo_scan->label))
+      {
+	linfo = linfo_scan;
+	return 0;
+      }
+    else
+      {
+	return 1;
+      }
+  }
+
+  linfo = NULL;
+  if (label != NULL)
+    {
+      list_iterate (labellist, label_find_scan);
+    }
+  return linfo;
+}

gui/src/label.h

@@ -0,0 +1,26 @@
+#ifndef LABEL
+#define LABEL
+
+#include "term.h"
+#include "list.h"
+#include "system.h"
+
+/*
+ * Structure to store label information
+ */
+struct labelinfo
+{
+  Term label;
+  int ignore;
+  Protocol protocol;
+  Term sendrole;
+  Term readrole;
+};
+
+typedef struct labelinfo *Labelinfo;
+
+Labelinfo label_create (const Term label, const Protocol protocol);
+void label_destroy (Labelinfo linfo);
+Labelinfo label_find (List labellist, const Term label);
+
+#endif

gui/src/language.txt

@@ -0,0 +1,46 @@
+Language
+--------
+
+language	:= (<def>)*
+def		:= (<directive> | <protocol> | <rundef> | <unstrusted>)
+
+//directive	:= <dir_require>
+//dir_require	:= require <filename>;
+
+protocol	:= protocol <protocolname> ( <rolelist> ) { <roledef>* } optsc
+protocolname	:= <id>
+
+intruderknow	:= public <termlist>;
+roledef		:= role <rolename> { <actions> } optsc
+rolename	:= <id> 
+actions		:= (<action>;)+
+action		:= (<read> | <send> | <claim>)
+decl		:= (<const> | <var>)+
+const		:= const <termlist> [ : <typeterm> ];
+var		:= var <termlist> [ : <typelist> ];
+
+read		:= read [_<label>]  (<term>,<term>,<term>);
+send		:= send [_<label>]  (<term>,<term>,<term>);
+claim		:= claim [_<label>] (<term>,<termlist>);
+label		:= <id>;
+
+rundef		:= <protocolname>.<rolename> ( <instancelist> ) ;
+instancelist	:= (<agent>|<typeterm>)*
+
+agent		:= <term>
+typeterm	:= <term>
+typelist	:= <termlist>
+
+untrusted	:= untrusted <termlist>;
+
+termlist	:= <term> [, <termlist>]
+term		:= (<baseterm> | <encterm> | <tupleterm> | <function>)
+encterm		:= { <term> } <term>
+function	:= <term> ( <term> )
+baseterm	:= (<variable> | <const>)
+variable	:= <id>
+const		:= <id>
+
+optsc		:= [ ; ]
+id		:= (<digit>|<uppercase>|<lowercase>)+
+

gui/src/license.txt

@@ -0,0 +1,3 @@
+- GNU getopt
+- GNU bison/flex
+- de rest (c) Cas

gui/src/list.c

@@ -0,0 +1,272 @@
+/**
+ *@file list.c
+ * Generic list type
+ *
+ * A doubly linked list with void* as data type.
+ */
+
+#include "list.h"
+#if !defined(__APPLE__)
+#include <malloc.h>
+#endif
+#include <stdlib.h>
+
+//! Make a node
+List
+list_create (const void *data)
+{
+  List newlist;
+
+  newlist = (List) malloc (sizeof (struct list_struct));
+  newlist->prev = NULL;
+  newlist->next = NULL;
+  newlist->data = (void *) data;
+  return newlist;
+}
+
+//! Rewind list
+List
+list_rewind (List list)
+{
+  if (list != NULL)
+    {
+      while (list->prev != NULL)
+	{
+	  list = list->prev;
+	}
+    }
+  return list;
+}
+
+//! Forward list
+List
+list_forward (List list)
+{
+  if (list == NULL)
+    {
+      return NULL;
+    }
+  else
+    {
+      while (list->next != NULL)
+	{
+	  list = list->next;
+	}
+      return list;
+    }
+}
+
+//! Add element to list, inserting it just before the current node.
+/**
+ * @returns the head of the list
+ */
+List
+list_insert (List list, const void *data)
+{
+  List newnode;
+
+  newnode = list_create (data);
+  if (list == NULL)
+    {
+      return newnode;
+    }
+  newnode->next = list;
+  newnode->prev = list->prev;
+  list->prev = newnode;
+  if (newnode->prev != NULL)
+    {
+      newnode->prev->next = newnode;
+      return list_rewind (newnode->prev);
+    }
+  else
+    {
+      return newnode;
+    }
+}
+
+//! Add element to list, inserting it just after the current node.
+/**
+ * @returns the head of the list
+ */
+List
+list_add (List list, const void *data)
+{
+  List newnode;
+
+  newnode = list_create (data);
+  if (list == NULL)
+    {
+      return newnode;
+    }
+  else
+    {
+      newnode->next = list->next;
+      newnode->prev = list;
+      list->next = newnode;
+      if (newnode->next != NULL)
+	{
+	  newnode->next->prev = newnode;
+	}
+      return list_rewind (list);
+    }
+}
+
+//! Add element to list, inserting it at the tail of the list.
+/**
+ * @returns the head of the list
+ */
+List
+list_append (List list, const void *data)
+{
+  List newnode;
+  List lastnode;
+
+  newnode = list_create (data);
+  if (list == NULL)
+    {
+      return newnode;
+    }
+  else
+    {
+      lastnode = list_forward (list);
+      newnode->prev = lastnode;
+      lastnode->next = newnode;
+      return list_rewind (list);
+    }
+}
+
+
+//! Destroy a node
+/**
+ * @returns the head of the list
+ */
+List
+list_delete (List list)
+{
+  if (list != NULL)
+    {
+      List prenode, postnode;
+
+      prenode = list->prev;
+      postnode = list->next;
+      free (list);
+      if (postnode != NULL)
+	{
+	  postnode->prev = prenode;
+	}
+      if (prenode != NULL)
+	{
+	  prenode->next = postnode;
+	  return list_rewind (prenode);
+	}
+      else
+	{
+	  return postnode;
+	}
+    }
+  else
+    {
+      return NULL;
+    }
+}
+
+//! Test if it's already in the list, using pointer equality.
+/**
+ *@warn Only scans forward, so make sure the list is rewound.
+ *@returns The boolean result.
+ */
+int
+in_list (List list, const void *compdata)
+{
+  while (list != NULL)
+    {
+      if (list->data == compdata)
+	{
+	  return 1;
+	}
+      list = list->next;
+    }
+  return 0;
+}
+
+//! Iterator
+/**
+ * Function used returns int; if non-zero (true), iteration continues.
+ * Function is called with data as argument, *not* the list node.
+ *
+ *@returns true iff domain empty or all applications true. If false, some iteration aborted the run.
+ */
+int
+list_iterate (List list, int (*func) ())
+{
+  while (list != NULL)
+    {
+      if (!func (list->data))
+	{
+	  return 0;
+	}
+      list = list->next;
+    }
+  return 1;
+}
+
+//! Duplicate (always shallow)
+List
+list_duplicate (List list)
+{
+  List newlist;
+
+  if (list == NULL)
+    {
+      return NULL;
+    }
+  list = list_forward (list);
+  newlist = NULL;
+  while (list != NULL)
+    {
+      newlist = list_insert (newlist, list->data);
+      list = list->prev;
+    }
+  return newlist;
+}
+
+//! Destroy (shallow)
+void
+list_destroy (List list)
+{
+  list = list_rewind (list);
+  while (list != NULL)
+    {
+      List node;
+
+      node = list;
+      list = list->next;
+      free (node);
+    }
+}
+
+//! Shift n positions to the right
+List
+list_shift (List list, int n)
+{
+  while (n > 0 && list != NULL)
+    {
+      list = list->next;
+      n--;
+    }
+  return list;
+}
+
+//! Determine length of list from this point onwards
+int
+list_length (List list)
+{
+  int n;
+
+  while (list != NULL)
+    {
+      n++;
+      list = list->next;
+    }
+  return n;
+}

gui/src/list.h

@@ -0,0 +1,28 @@
+#ifndef GENERICLIST
+#define GENERICLIST
+
+//! generic list structure node
+struct list_struct
+{
+  struct list_struct *next;	//!< pointer to next node
+  struct list_struct *prev;	//!< pointer to previous node
+  void *data;			//!< pointer to the actual data element (should be typecast)
+};
+
+typedef struct list_struct *List;	//!< pointer to generic list node
+
+List list_create (const void *data);
+List list_rewind (List list);
+List list_forward (List list);
+List list_insert (List list, const void *data);
+List list_add (List list, const void *data);
+List list_append (List list, const void *data);
+List list_delete (List list);
+int in_list (List list, const void *data);
+int list_iterate (List list, int (*func) ());
+List list_duplicate (List list);
+void list_destroy (List list);
+List list_shift (List list, int n);
+int list_length (List list);
+
+#endif

gui/src/main.c

@@ -0,0 +1,260 @@
+/**
+ *@file main.c
+ * \brief The main file.
+ *
+ * Contains the main switch handling, and passes everything to the core logic.
+ */
+
+/**
+ * \mainpage
+ *
+ * \section intro Introduction
+ *
+ * Scyther is a model checker for security protocols.
+ *
+ * \section install Installation
+ *
+ * How to install Scyther.
+ *
+ * \section exit Exit codes
+ *
+ * 0  Okay	No attack found, claims encountered
+ *
+ * 1  Error	Something went wrong (error) E.g. switch error, or scenario ran out.
+ *
+ * 2  Okay	No attack found (because) no claims encountered
+ *
+ * 3  Okay	Attack found
+ *
+ * \section coding Coding conventions
+ *
+ * Usually, each source file except main.c has an myfileInit() and myfileDone() function
+ * available. These allow any initialisation and destruction of required structures.
+ *
+ * GNU indent rules are used, but K&R derivatives are allowed as well. Conversion can
+ * be done for any style using the GNU indent program.
+ */
+
+#include <stdlib.h>
+#include <stdio.h>
+#include <time.h>
+#include <limits.h>
+#include "system.h"
+#include "debug.h"
+#include "symbol.h"
+#include "pheading.h"
+#include "symbol.h"
+#include "tac.h"
+#include "timer.h"
+#include "compiler.h"
+#include "binding.h"
+#include "switches.h"
+#include "specialterm.h"
+#include "color.h"
+#include "error.h"
+#include "claim.h"
+#include "arachne.h"
+#include "xmlout.h"
+
+//! The global system state pointer
+System sys;
+
+//! Pointer to the tac node container
+extern struct tacnode *spdltac;
+//! Match mode
+extern int mgu_match;
+
+void scanner_cleanup (void);
+void strings_cleanup (void);
+int yyparse (void);
+
+void MC_incRuns (const System sys);
+void MC_incTraces (const System sys);
+void MC_single (const System sys);
+int modelCheck (const System sys);
+
+//! The main body, as called by the environment.
+int
+main (int argc, char **argv)
+{
+  int exitcode = EXIT_NOATTACK;
+
+  /* initialize symbols */
+  termsInit ();
+  termmapsInit ();
+  termlistsInit ();
+  knowledgeInit ();
+  symbolsInit ();
+  tacInit ();
+
+  /*
+   * ------------------------------------------------
+   *     generate system 
+   * ------------------------------------------------
+   */
+
+  /* process any command-line switches */
+  switchesInit (argc, argv);
+
+  /* process colors */
+  colorInit ();
+
+  /* start system */
+  sys = systemInit ();
+
+  /* init compiler for this system */
+  compilerInit (sys);
+
+  sys->know = emptyKnowledge ();
+
+
+  /* parse input */
+
+  yyparse ();
+#ifdef DEBUG
+  if (DEBUGL (1))
+    tacPrint (spdltac);
+#endif
+
+  /* compile */
+
+  // Compile no runs for Arachne and preprocess
+  compile (spdltac, 0);
+  scanner_cleanup ();
+
+#ifdef DEBUG
+  if (DEBUGL (1))
+    {
+      printf ("\nCompilation yields:\n\n");
+      printf ("untrusted agents: ");
+      termlistPrint (sys->untrusted);
+      printf ("\n");
+      knowledgePrint (sys->know);
+      printf ("inverses: ");
+      knowledgeInversesPrint (sys->know);
+      printf ("\n");
+      locVarPrint (sys->locals);
+      protocolsPrint (sys->protocols);
+
+      printf ("\nInstantiated runs:\n\n");
+      runsPrint (sys);
+    }
+#endif
+
+  /* allocate memory for traces, based on runs */
+  systemStart (sys);
+  sys->traceKnow[0] = sys->know;	// store initial knowledge
+
+  /* add parameters to system */
+
+
+  /*
+   * ---------------------------------------
+   *  Switches consistency checking.
+   * ---------------------------------------
+   */
+
+#ifdef DEBUG
+  if (DEBUGL (4))
+    {
+      warning ("Selected output method is %i", switches.output);
+    }
+#endif
+
+  arachneInit (sys);
+
+  /*
+   * ---------------------------------------
+   *  Start real stuff
+   * ---------------------------------------
+   */
+
+  /* xml init */
+  if (switches.xml)
+    xmlOutInit ();
+
+  /* model check system */
+#ifdef DEBUG
+  if (DEBUGL (1))
+    warning ("Start modelchecking system.");
+#endif
+  MC_single (sys);
+
+  /*
+   * ---------------------------------------
+   *  After checking the system, results
+   * ---------------------------------------
+   */
+
+  /* Exitcodes are *not* correct anymore */
+
+  exitcode = EXIT_ATTACK;
+
+  /* xml closeup */
+  if (switches.xml)
+    xmlOutDone ();
+
+  /*
+   * Now we clean up any memory that was allocated.
+   */
+
+  arachneDone ();
+  knowledgeDestroy (sys->know);
+  systemDone (sys);
+  colorDone ();
+  compilerDone ();
+
+  /* done symbols */
+  tacDone ();
+  symbolsDone ();
+  knowledgeDone ();
+  termlistsDone ();
+  termmapsDone ();
+  termsDone ();
+
+  /* memory clean up? */
+  strings_cleanup ();
+
+  return exitcode;
+}
+
+//! Analyse the model
+/**
+ * Traditional handywork.
+ */
+
+void
+MC_single (const System sys)
+{
+  /*
+   * simple one-time check
+   */
+
+  systemReset (sys);		// reset any globals
+  systemRuns (sys);		// init runs data
+  modelCheck (sys);
+}
+
+//! Model check the system, given all parameters.
+/*
+ * Precondition: the system was reset with the corresponding parameters.
+ * Reports time and states traversed.
+ * Note that the return values doubles as the number of failed claims.
+ *@return True iff any claim failed, and thus an attack was found.
+ */
+
+int
+modelCheck (const System sys)
+{
+  int claimcount;
+
+  /* modelcheck the system */
+  claimcount = arachne ();
+
+  if (claimcount == 0)
+    {
+      warning ("No claims in system.");
+    }
+
+  return (sys->failed != STATES0);
+}

gui/src/mgu.c

@@ -0,0 +1,624 @@
+#include <stdlib.h>
+#include <stdio.h>
+#include "term.h"
+#include "termlist.h"
+#include "mgu.h"
+#include "type.h"
+#include "debug.h"
+#include "specialterm.h"
+#include "switches.h"
+
+/*
+   Most General Unifier
+
+   Unification etc.
+
+   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
+ * 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)
+{
+#ifdef DEBUG
+  if (!DEBUGL (5))
+    return;
+
+  indent ();
+  eprintf ("Substituting ");
+  termPrint (t);
+  eprintf (", typed ");
+  termlistPrint (t->stype);
+  if (realTermLeaf (t->subst))
+    {
+      eprintf ("->");
+      termlistPrint (t->subst->stype);
+    }
+  else
+    {
+      eprintf (", composite term");
+    }
+  if (t->type != VARIABLE)
+    {
+      eprintf (" (bound roleconstant)");
+    }
+  eprintf ("\n");
+#endif
+}
+
+//! See if this is preferred substitution
+/**
+ * By default, ta->tb will map. Returning 0 (false) will swap them.
+ */
+int
+preferSubstitutionOrder (Term ta, Term tb)
+{
+  if (termlistLength (ta->stype) == 1 && inTermlist (ta->stype, TERM_Agent))
+    {
+      /**
+       * If the first one is an agent type, we prefer swapping.
+       */
+      return 0;
+    }
+
+  // Per default, leave it as it is.
+  return 1;
+}
+
+//! See if a substitution is valid
+__inline__ int
+goodsubst (Term tvar, Term tsubst)
+{
+  Term tbuf;
+  int res;
+
+  tbuf = tvar->subst;
+  tvar->subst = tsubst;
+
+  res = checkTypeTerm (mgu_match, tvar);
+
+  tvar->subst = tbuf;
+  return res;
+}
+
+//! Undo all substitutions in a list of variables.
+/**
+ * The termlist should contain only variables.
+ */
+void
+termlistSubstReset (Termlist tl)
+{
+  while (tl != NULL)
+    {
+      tl->term->subst = NULL;
+      tl = tl->next;
+    }
+}
+
+//! Most general unifier iteration
+/**
+ * Try to determine the most general unifier of two terms, if so calls function.
+ *
+ * The callback receives a list of variables, that were previously open, but are now closed
+ * in such a way that the two terms unify. 
+ *
+ * The callback must return true for the iteration to proceed: if it returns false, a single call would abort the scan.
+ * The return value shows this: it is false if the scan was aborted, and true if not.
+ */
+int
+unify (Term t1, Term t2, Termlist tl, int (*callback) (Termlist))
+{
+  int callsubst (Termlist tl, Term t, Term tsubst)
+  {
+    int proceed;
+
+    t->subst = tsubst;
+#ifdef DEBUG
+    showSubst (t);
+#endif
+    tl = termlistAdd (tl, t);
+    proceed = callback (tl);
+    tl = termlistDelTerm (tl);
+    t->subst = NULL;
+    return proceed;
+  }
+
+  /* added for speed */
+  t1 = deVar (t1);
+  t2 = deVar (t2);
+  if (t1 == t2)
+    {
+      return callback (tl);
+    }
+
+  if (!(hasTermVariable (t1) || hasTermVariable (t2)))
+    {
+      // None has a variable
+      if (isTermEqual (t1, t2))
+	{
+	  // Equal!
+	  return callback (tl);
+	}
+      else
+	{
+	  // Can never be fixed, no variables
+	  return true;
+	}
+    }
+
+  /*
+   * Distinguish a special case where both are unbound variables that will be
+   * connected, and I want to give one priority over the other for readability.
+   *
+   * Because t1 and t2 have been deVar'd means that if they are variables, they
+   * are also unbound.
+   */
+
+  if (realTermVariable (t1) && realTermVariable (t2) && goodsubst (t1, t2))
+    {
+      /* Both are unbound variables. Decide.
+       *
+       * The plan: t1->subst will point to t2. But maybe we prefer the other
+       * way around?
+       */
+      if (preferSubstitutionOrder (t2, t1))
+	{
+	  Term t3;
+
+	  // Swappy.
+	  t3 = t1;
+	  t1 = t2;
+	  t2 = t3;
+	}
+      return callsubst (tl, t1, t2);
+    }
+
+  /* symmetrical tests for single variable.
+   */
+
+  if (realTermVariable (t2))
+    {
+      if (termSubTerm (t1, t2) || !goodsubst (t2, t1))
+	return true;
+      else
+	{
+	  return callsubst (tl, t2, t1);
+	}
+    }
+  if (realTermVariable (t1))
+    {
+      if (termSubTerm (t2, t1) || !goodsubst (t1, t2))
+	return true;
+      else
+	{
+	  return callsubst (tl, t1, t2);
+	}
+    }
+
+  /* left & right are compounds with variables */
+  if (t1->type != t2->type)
+    return true;
+
+  /* identical compound types */
+
+  /* encryption first */
+  if (realTermEncrypt (t1))
+    {
+      int unify_combined_enc (Termlist tl)
+      {
+	// now the keys are unified (subst in this tl)
+	// and we try the inner terms
+	return unify (TermOp (t1), TermOp (t2), tl, callback);
+      }
+
+      return unify (TermKey (t1), TermKey (t2), tl, unify_combined_enc);
+    }
+
+  /* tupling second
+     non-associative version ! TODO other version */
+  if (isTermTuple (t1))
+    {
+      int unify_combined_tup (Termlist tl)
+      {
+	// now the keys are unified (subst in this tl)
+	// and we try the inner terms
+	return unify (TermOp2 (t1), TermOp2 (t2), tl, callback);
+      }
+      return unify (TermOp1 (t1), TermOp1 (t2), tl, unify_combined_tup);
+    }
+
+  return true;
+}
+
+
+//! Subterm unification
+/**
+ * Try to unify (a subterm of) tbig with tsmall.
+ *
+ * Callback is called with a list of substitutions, and a list of terms that
+ * need to be decrypted in order for this to work.
+ *
+ * E.g. subtermUnify ( {{m}k1}k2, m ) yields a list : {{m}k1}k2, {m}k1 (where
+ * the {m}k1 is the last added node to the list)
+ *
+ * The callback should return true for the iteration to proceed, or false to abort.
+ * The final result is this flag.
+ */
+int
+subtermUnify (Term tbig, Term tsmall, Termlist tl, Termlist keylist,
+	      int (*callback) (Termlist, Termlist))
+{
+  int proceed;
+
+  int keycallback (Termlist tl)
+  {
+    return callback (tl, keylist);
+  }
+
+  proceed = true;
+
+  // Devar
+  tbig = deVar (tbig);
+  tsmall = deVar (tsmall);
+
+  // Three options:
+  // 1. simple unification
+  proceed = proceed && unify (tbig, tsmall, tl, keycallback);
+
+  // [2/3]: complex
+  if (switches.intruder)
+    {
+      // 2. interm unification
+      // Only if there is an intruder
+      if (realTermTuple (tbig))
+	{
+	  proceed = proceed
+	    && subtermUnify (TermOp1 (tbig), tsmall, tl, keylist, callback);
+	  proceed = proceed
+	    && subtermUnify (TermOp2 (tbig), tsmall, tl, keylist, callback);
+	}
+
+      // 3. unification with encryption needed
+      if (realTermEncrypt (tbig))
+	{
+	  // extend the keylist
+	  keylist = termlistAdd (keylist, tbig);
+	  proceed = proceed
+	    && subtermUnify (TermOp (tbig), tsmall, tl, keylist, callback);
+	  // remove last item again
+	  keylist = termlistDelTerm (keylist);
+	}
+    }
+  return proceed;
+}
+
+
+//! Most general unifier.
+/**
+ * Try to determine the most general unifier of two terms.
+ * Resulting termlist must be termlistDelete'd.
+ *
+ *@return Returns a list of variables, that were previously open, but are now closed
+ * in such a way that the two terms unify. Returns \ref MGUFAIL if it is impossible.
+ * The termlist should be deleted.
+ */
+Termlist
+termMguTerm (Term t1, Term t2)
+{
+  /* added for speed */
+  t1 = deVar (t1);
+  t2 = deVar (t2);
+  if (t1 == t2)
+    return NULL;
+
+  if (!(hasTermVariable (t1) || hasTermVariable (t2)))
+    {
+      if (isTermEqual (t1, t2))
+	{
+	  return NULL;
+	}
+      else
+	{
+	  return MGUFAIL;
+	}
+    }
+
+  /*
+   * Distinguish a special case where both are unbound variables that will be
+   * connected, and I want to give one priority over the other for readability.
+   *
+   * Because t1 and t2 have been deVar'd means that if they are variables, they
+   * are also unbound.
+   */
+
+  if (realTermVariable (t1) && realTermVariable (t2) && goodsubst (t1, t2))
+    {
+      /* Both are unbound variables. Decide.
+       *
+       * The plan: t1->subst will point to t2. But maybe we prefer the other
+       * way around?
+       */
+      if (preferSubstitutionOrder (t2, t1))
+	{
+	  Term t3;
+
+	  // Swappy.
+	  t3 = t1;
+	  t1 = t2;
+	  t2 = t3;
+	}
+      t1->subst = t2;
+#ifdef DEBUG
+      showSubst (t1);
+#endif
+      return termlistAdd (NULL, t1);
+    }
+
+  /* symmetrical tests for single variable.
+   */
+
+  if (realTermVariable (t2))
+    {
+      if (termSubTerm (t1, t2) || !goodsubst (t2, t1))
+	return MGUFAIL;
+      else
+	{
+	  t2->subst = t1;
+#ifdef DEBUG
+	  showSubst (t2);
+#endif
+	  return termlistAdd (NULL, t2);
+	}
+    }
+  if (realTermVariable (t1))
+    {
+      if (termSubTerm (t2, t1) || !goodsubst (t1, t2))
+	return MGUFAIL;
+      else
+	{
+	  t1->subst = t2;
+#ifdef DEBUG
+	  showSubst (t1);
+#endif
+	  return termlistAdd (NULL, t1);
+	}
+    }
+
+  /* left & right are compounds with variables */
+  if (t1->type != t2->type)
+    return MGUFAIL;
+
+  /* identical compounds */
+  /* encryption first */
+  if (realTermEncrypt (t1))
+    {
+      Termlist tl1, tl2;
+
+      tl1 = termMguTerm (TermKey (t1), TermKey (t2));
+      if (tl1 == MGUFAIL)
+	{
+	  return MGUFAIL;
+	}
+      else
+	{
+	  tl2 = termMguTerm (TermOp (t1), TermOp (t2));
+	  if (tl2 == MGUFAIL)
+	    {
+	      termlistSubstReset (tl1);
+	      termlistDelete (tl1);
+	      return MGUFAIL;
+	    }
+	  else
+	    {
+	      return termlistConcat (tl1, tl2);
+	    }
+	}
+    }
+
+  /* tupling second
+     non-associative version ! TODO other version */
+  if (isTermTuple (t1))
+    {
+      Termlist tl1, tl2;
+
+      tl1 = termMguTerm (TermOp1 (t1), TermOp1 (t2));
+      if (tl1 == MGUFAIL)
+	{
+	  return MGUFAIL;
+	}
+      else
+	{
+	  tl2 = termMguTerm (TermOp2 (t1), TermOp2 (t2));
+	  if (tl2 == MGUFAIL)
+	    {
+	      termlistSubstReset (tl1);
+	      termlistDelete (tl1);
+	      return MGUFAIL;
+	    }
+	  else
+	    {
+	      return termlistConcat (tl1, tl2);
+	    }
+	}
+    }
+  return MGUFAIL;
+}
+
+//! Most general interm unifiers of t1 interm t2
+/**
+ * Try to determine the most general interm unifiers of two terms.
+ *@returns Nothing. Iteration gets termlist of substitutions.
+ */
+int
+termMguInTerm (Term t1, Term t2, int (*iterator) (Termlist))
+{
+  Termlist tl;
+  int flag;
+
+  flag = 1;
+  t2 = deVar (t2);
+  if (t2 != NULL)
+    {
+      if (realTermTuple (t2))
+	{
+	  // t2 is a tuple, consider interm options as well.
+	  flag = flag && termMguInTerm (t1, TermOp1 (t2), iterator);
+	  flag = flag && termMguInTerm (t1, TermOp2 (t2), iterator);
+	}
+      // simple clause or combined
+      tl = termMguTerm (t1, t2);
+      if (tl != MGUFAIL)
+	{
+	  // Iterate
+	  flag = flag && iterator (tl);
+	  // Reset variables
+	  termlistSubstReset (tl);
+	  // Remove list
+	  termlistDelete (tl);
+	}
+    }
+  else
+    {
+      if (deVar (t1) != NULL)
+	{
+	  flag = 0;
+	}
+    }
+  return flag;
+}
+
+//! Most general subterm unifiers of smallterm subterm bigterm
+/**
+ * Try to determine the most general subterm unifiers of two terms.
+ *@returns Nothing. Iteration gets termlist of subst, and list of keys needed
+ *  to decrypt. This termlist does not need to be deleted, because it is handled
+ *  by the mguSubTerm itself.
+ */
+int
+termMguSubTerm (Term smallterm, Term bigterm,
+		int (*iterator) (Termlist, Termlist), Termlist inverses,
+		Termlist cryptlist)
+{
+  int flag;
+
+  flag = 1;
+  smallterm = deVar (smallterm);
+  bigterm = deVar (bigterm);
+  if (bigterm != NULL)
+    {
+      Termlist tl;
+
+      if (!realTermLeaf (bigterm))
+	{
+	  if (realTermTuple (bigterm))
+	    {
+	      // 'simple' tuple
+	      flag =
+		flag
+		&& termMguSubTerm (smallterm, TermOp1 (bigterm), iterator,
+				   inverses, cryptlist);
+	      flag = flag
+		&& termMguSubTerm (smallterm, TermOp2 (bigterm), iterator,
+				   inverses, cryptlist);
+	    }
+	  else
+	    {
+	      // Must be encryption
+	      Term keyneeded;
+
+	      keyneeded = inverseKey (inverses, TermKey (bigterm));
+	      // We can never produce the TERM_Hidden key, thus, this is not a valid iteration.
+	      if (!isTermEqual (keyneeded, TERM_Hidden))
+		{
+		  cryptlist = termlistAdd (cryptlist, bigterm);	// Append, so the last encrypted term in the list is the most 'inner' one, and the first is the outer one.
+
+		  // Recurse
+		  flag =
+		    flag
+		    && termMguSubTerm (smallterm, TermOp (bigterm), iterator,
+				       inverses, cryptlist);
+
+
+		  cryptlist = termlistDelTerm (cryptlist);
+		}
+	      termDelete (keyneeded);
+	    }
+	}
+      // simple clause or combined
+      tl = termMguTerm (smallterm, bigterm);
+      if (tl != MGUFAIL)
+	{
+	  // Iterate
+	  flag = flag && iterator (tl, cryptlist);
+	  // Reset variables
+	  termlistSubstReset (tl);
+	  // Remove list
+	  termlistDelete (tl);
+	}
+    }
+  else
+    {
+      if (smallterm != NULL)
+	{
+	  flag = 0;
+	}
+    }
+  return flag;
+}
+
+//! Check if role terms might match in some way
+/**
+ * Interesting case: role names are variables here, so they always match. We catch that case by inspecting the variable list.
+ */
+int
+checkRoletermMatch (const Term t1, const Term t2, const Termlist notmapped)
+{
+  Termlist tl;
+
+  // simple clause or combined
+  tl = termMguTerm (t1, t2);
+  if (tl == MGUFAIL)
+    {
+      return false;
+    }
+  else
+    {
+      int result;
+      Termlist vl;
+
+      result = true;
+      // Reset variables
+      termlistSubstReset (tl);
+      // Check variable list etc: should not contain mapped role names
+      vl = tl;
+      while (vl != NULL)
+	{
+	  // This term should not be in the notmapped list
+	  if (inTermlist (notmapped, vl->term))
+	    {
+	      result = false;
+	      break;
+	    }
+	  vl = vl->next;
+
+	}
+      // Remove list
+      termlistDelete (tl);
+      return result;
+    }
+}

gui/src/mgu.h

@@ -0,0 +1,30 @@
+#ifndef MGU
+#define MGU
+
+#include "term.h"
+#include "termlist.h"
+
+//! A special constant do denote failure.
+/**
+ * \c NULL already denotes equality, so an extra signal is needed to
+ * denote that a unification fails.
+ * \todo Find a portable solution for this \c MGUFAIL constant:
+ * maybe a pointer to some special constant.
+ */
+#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),
+		    Termlist inverses, Termlist keylist);
+void termlistSubstReset (Termlist tl);
+int checkRoletermMatch (const Term t1, const Term t2, const Termlist tl);
+
+// The new iteration methods
+int unify (Term t1, Term t2, Termlist tl, int (*callback) (Termlist));
+int
+subtermUnify (Term tbig, Term tsmall, Termlist tl, Termlist keylist,
+	      int (*callback) (Termlist, Termlist));
+
+#endif

gui/src/notes.txt

@@ -0,0 +1,17 @@
+- (!!) Are the Arachne rules for keys that are variables sane? E.g. what
+  is their inverse key? Check! Intuition: one cannot know what the
+  inverse is of a non-instantiated key variable, given the current
+  semantics, if asymmetric keys are allowed.
+  Consequence: the current implementation is just fine, because
+  asymmetric key variables cannot be defined in the language. Thus, the
+  rules are fine. Investigate for the other case.
+- If no attack/state output is needed, maybe the attack heuristic should
+  be simpler (which means just weighting the trace length etc.) in order
+  to avoid uneccesary continuation of the search. Maybe even stop
+  altogether after finding *an* attack.
+- For the TimeStamps etc, we can implement an 'auto-leak' of such local
+  constants. This should works also with a modifier of sorts (e.g.
+  'predictable') and such constants should be leaked to the intruder at
+  the start of the run, possibly by prefixing a send.
+- knowledgeAddTerm might be improved by scanning through key list only with
+  things that are newly added.

gui/src/parser.y

@@ -0,0 +1,325 @@
+%{
+#include "pheading.h"
+#include "tac.h"
+#include "error.h"
+
+struct tacnode*	spdltac;
+
+int yyerror(char *s);
+int yylex(void);
+
+%}
+
+%union{
+	char*  		str;
+	struct tacnode*	tac;
+	Symbol		symb;
+	int		value;
+}
+
+%token 	<symb>	ID
+%token 		PROTOCOL
+%token 		ROLE
+%token 		READT
+%token 		SENDT
+%token 		CLAIMT
+%token 		VAR
+%token 		CONST
+%token 		RUN
+%token 		SECRET
+%token 		COMPROMISED
+%token 		INVERSEKEYS
+%token 		UNTRUSTED
+%token 		USERTYPE
+%token		SINGULAR
+%token		FUNCTION
+%token 		HASHFUNCTION
+%token		KNOWS
+%token		TRUSTED
+
+%type	<tac>	spdlcomplete
+%type	<tac>	spdlrep
+%type	<tac>	spdl
+%type	<tac>	roles
+%type	<tac>	role
+%type	<tac>	roledef
+%type	<tac>	event
+%type	<tac>	declaration
+%type	<tac>	secretpref
+%type	<tac>	typeinfo1
+%type	<tac>	typeinfoN
+%type	<tac>	term
+%type	<tac>	basicterm
+%type	<tac>	termlist
+%type	<tac>	basictermlist
+%type	<tac>	key
+%type	<tac>	roleref
+%type	<tac>	knowsdecl
+
+%type   <value>	singular
+
+%type	<symb>	label
+%type	<symb>	optlabel
+
+%start spdlcomplete
+
+
+%%
+
+spdlcomplete	: spdlrep
+		  {	spdltac = $1; }
+		;
+
+spdlrep		: /* empty */
+		  {	$$ = NULL; }
+		| spdl spdlrep
+		  {	$$ = tacCat($1,$2); }
+		;
+
+spdl		: UNTRUSTED termlist ';'
+		  {	
+		  	Tac t = tacCreate(TAC_UNTRUSTED);
+		  	t->t1.tac = $2;
+			$$ = t;
+		  }
+		| RUN roleref '(' termlist ')' ';'
+		  {	
+		  	Tac t = tacCreate(TAC_RUN);
+		  	t->t1.tac = $2;
+			t->t2.tac = $4;
+			$$ = t;
+		  }
+		| PROTOCOL ID '(' termlist ')' '{' roles '}' optclosing
+	 	  {
+		  	Tac t = tacCreate(TAC_PROTOCOL);
+			t->t1.sym = $2;
+			t->t2.tac = $7;
+			t->t3.tac = $4;
+			$$ = t;
+		  }
+		| USERTYPE termlist ';'
+		  {
+			Tac t = tacCreate(TAC_USERTYPE);
+			t->t1.tac = $2;
+			$$ = t;
+		  }
+		| declaration
+		  {
+		  	$$ = $1;
+		  }
+		;
+
+roles		: /* empty */
+       		  {	$$ = NULL; }
+       		| role roles
+		  {	$$ = tacCat($1,$2); }
+		| declaration roles
+		  {	$$ = tacCat($1,$2); }
+		;
+
+role		: singular ROLE ID '{' roledef '}' optclosing
+      		  { 
+		  	// TODO process singular (0/1)
+		  	Tac t = tacCreate(TAC_ROLE);
+			t->t1.sym = $3;
+			t->t2.tac = $5;
+			t->t3.value = $1;
+			$$ = t;
+		  }
+		;
+
+singular	: /* empty */
+	 	  {	$$ = 0; }
+		| SINGULAR
+		  {	$$ = 1; }
+		;
+
+optclosing	: /* empty */
+		  { }
+		| ';'
+		  { }
+		;
+
+roledef		: /* empty */
+		  {	$$ = NULL; }
+		| event roledef
+		  {	$$ = tacCat($1,$2); }
+		| declaration roledef
+		  {	$$ = tacCat($1,$2); }
+		| knowsdecl roledef
+		  {	$$ = tacCat($1,$2); }
+		;
+
+event		: READT label '(' termlist ')' ';'
+		  {	Tac t = tacCreate(TAC_READ);
+		  	t->t1.sym = $2;
+			/* TODO test here: tac2 should have at least 3 elements */
+			t->t2.tac = $4;
+			$$ = t;
+		  }
+		| SENDT label '(' termlist ')' ';'
+		  {	Tac t = tacCreate(TAC_SEND);
+		  	t->t1.sym = $2;
+			/* TODO test here: tac2 should have at least 3 elements */
+			t->t2.tac = $4;
+			$$ = t;
+		  }
+		| CLAIMT optlabel '(' termlist ')' ';'
+		/* TODO maybe claims should be in the syntax */
+		  {	Tac t = tacCreate(TAC_CLAIM);
+		  	t->t1.sym = $2;
+			t->t2.tac = $4;
+			$$ = t;
+		  }
+		;
+
+roleref		: ID '.' ID
+		  {	Tac t = tacCreate(TAC_ROLEREF);
+		  	t->t1.sym = $1;
+			t->t2.sym = $3;
+			$$ = t;
+		  }
+		;
+
+knowsdecl	: KNOWS termlist ';'
+		  {	Tac t = tacCreate(TAC_KNOWS);
+		  	t->t1.tac = $2;
+			$$ = t;
+		  }
+		;
+
+declaration	: secretpref CONST basictermlist typeinfo1 ';'
+		  {	Tac t = tacCreate(TAC_CONST);
+		  	t->t1.tac = $3;
+			t->t2.tac = $4;
+			t->t3.tac = $1;
+			$$ = t;
+		  }
+		| secretpref VAR basictermlist typeinfoN ';'
+		  {	Tac t = tacCreate(TAC_VAR);
+		  	t->t1.tac = $3;
+			t->t2.tac = $4;
+			t->t3.tac = $1;
+			$$ = t;
+		  }
+		| SECRET basictermlist typeinfo1 ';'
+		  {	Tac t = tacCreate(TAC_SECRET);
+		  	t->t1.tac = $2;
+			t->t2.tac = $3;
+			$$ = t;
+		  }
+		| INVERSEKEYS '(' term ',' term ')' ';'
+		  {	Tac t = tacCreate(TAC_INVERSEKEYS);
+			t->t1.tac = $3;
+			t->t2.tac = $5;
+			$$ = t;
+		  }
+		| COMPROMISED termlist ';'
+		  {	Tac t = tacCreate(TAC_COMPROMISED);
+		  	t->t1.tac= $2;
+			$$ = t;
+		  }
+		;
+
+secretpref	: /* empty */
+		  {	
+			$$ = NULL;
+		  }
+		| SECRET
+		  {
+			Tac t = tacCreate(TAC_SECRET);
+			$$ = t;
+		  }
+		;
+
+typeinfo1	: /* empty */
+		  {
+		  	Tac t = tacCreate(TAC_UNDEF);
+			$$ = t;
+		  }
+		| ':' ID
+		  {	Tac t = tacCreate(TAC_STRING);
+		  	t->t1.sym = $2;
+			$$ = t;
+		  }
+		;
+
+typeinfoN	: /* empty */
+		  {
+		  	Tac t = tacCreate(TAC_UNDEF);
+			$$ = t;
+		  }
+		| ':' basictermlist
+		  {	
+		  	$$ = $2;
+		  }
+		;
+
+label		: '_' ID
+		  { $$ = $2; }
+		;
+
+optlabel        : /* empty */
+                 { $$ = NULL; }
+               | label
+		  { }
+                ;
+
+
+basicterm	: ID
+		  {
+		  	Tac t = tacCreate(TAC_STRING);
+			t->t1.sym = $1;
+			$$ = t;
+		  }
+		;
+
+term  		: basicterm
+	          { }
+		| ID '(' termlist ')'
+		  {
+		  	Tac t = tacCreate(TAC_STRING);
+			t->t1.sym = $1;
+			$$ = tacJoin(TAC_ENCRYPT,tacTuple($3),t,NULL);
+		  }
+		| '{' termlist '}' key
+		  {
+		  	$$ = tacJoin(TAC_ENCRYPT,tacTuple($2),$4,NULL);
+		  }
+		| '(' termlist ')'
+		  { 
+		  	$$ = tacTuple($2);
+		  }
+		;
+
+termlist	: term
+		  { }
+		| term ',' termlist
+		  {	$$ = tacCat($1,$3); }
+		;
+
+basictermlist	: basicterm
+		  { }
+		| basicterm ',' basictermlist
+		  {	$$ = tacCat($1,$3); }
+		;
+
+key		: term
+		  { }
+		;
+
+
+
+%%
+
+//! error handler routing
+int yyerror(char *s)
+{
+	extern int yylineno;	//!< defined and maintained in lex.c
+	extern char *yytext;	//!< defined and maintained in lex.c
+  
+	error ("[%i] %s at symbol '%s'.\n", yylineno, s, yytext);
+	return 0;
+}
+
+

gui/src/pheading.h

@@ -0,0 +1,13 @@
+#ifndef PHEADING
+#define PHEADING
+
+#define YY_NO_UNPUT
+
+#include <stdio.h>
+#include <stdlib.h>
+#include "term.h"
+#include "termlist.h"
+#include "symbol.h"
+#include "system.h"
+#include "tac.h"
+#endif

gui/src/problem.spdl

@@ -0,0 +1,25 @@
+// BAN modified version of the yahalom protocol
+// Type flaw
+
+usertype Server;
+
+const a,b,c : Agent;
+const s : Server;
+secret k : Function;
+
+protocol yahalomBan(A,B,S)
+{
+	role B
+	{
+		const nb;
+		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 );
+		claim_6(B, Secret,kab);
+	}
+}
+
+

gui/src/prune_bounds.c

@@ -0,0 +1,265 @@
+/**
+ *
+ *@file prune_bounds.c
+ *
+ * Prune stuff based on bounds
+ *
+ */
+
+#include <limits.h>
+
+#include "termlist.h"
+#include "list.h"
+#include "switches.h"
+#include "timer.h"
+#include "arachne.h"
+#include "system.h"
+#include "termmap.h"
+#include "cost.h"
+
+extern int attack_length;
+extern int attack_leastcost;
+extern Protocol INTRUDER;
+extern int proofDepth;
+extern int max_encryption_level;
+
+//! Forward declarations
+int tooManyOfRole (const System sys);
+
+//! Prune determination for bounds
+/**
+ * When something is pruned here, the state space is not complete anymore.
+ *
+ *@returns true iff this state is invalid for some reason
+ */
+int
+prune_bounds (const System sys)
+{
+  /* prune for time */
+  if (passed_time_limit ())
+    {
+      // Oh no, we ran out of time!
+      if (switches.output == PROOF)
+	{
+	  indentPrint ();
+	  eprintf ("Pruned: ran out of allowed time (-T %i switch)\n",
+		   get_time_limit ());
+	}
+      // Pruned because of time bound!
+      sys->current_claim->timebound = 1;
+      return 1;
+    }
+
+  /* prune for number of attacks if we are actually outputting them */
+  if (enoughAttacks (sys))
+    {
+      // Oh no, we ran out of possible attacks!
+      if (switches.output == PROOF)
+	{
+	  indentPrint ();
+	  eprintf
+	    ("Pruned: we already found the maximum number of attacks.\n");
+	}
+      return 1;
+    }
+
+  /* prune for proof depth */
+  if (proofDepth > switches.maxproofdepth)
+    {
+      // Hardcoded limit on proof tree depth
+      if (switches.output == PROOF)
+	{
+	  indentPrint ();
+	  eprintf ("Pruned: proof tree too deep: %i (-d %i switch)\n",
+		   proofDepth, switches.maxproofdepth);
+	}
+      return 1;
+    }
+
+  /* prune for trace length */
+  if (switches.maxtracelength < INT_MAX)
+    {
+      int tracelength;
+      int run;
+
+      /* compute trace length of current semistate */
+      tracelength = 0;
+      run = 0;
+      while (run < sys->maxruns)
+	{
+	  /* ignore intruder actions */
+	  if (sys->runs[run].protocol != INTRUDER)
+	    {
+	      tracelength = tracelength + sys->runs[run].step;
+	    }
+	  run++;
+	}
+      /* test */
+      if (tracelength > switches.maxtracelength)
+	{
+	  // Hardcoded limit on proof tree depth
+	  if (switches.output == PROOF)
+	    {
+	      indentPrint ();
+	      eprintf ("Pruned: trace too long: %i (-l %i switch)\n",
+		       tracelength, switches.maxtracelength);
+	    }
+	  return 1;
+	}
+    }
+
+  /* prune for runs */
+  if (sys->num_regular_runs > switches.runs)
+    {
+      // Hardcoded limit on runs
+      if (switches.output == PROOF)
+	{
+	  indentPrint ();
+	  eprintf ("Pruned: too many regular runs (%i).\n",
+		   sys->num_regular_runs);
+	}
+      return 1;
+    }
+
+  /* prune for role instances max */
+  if (tooManyOfRole (sys))
+    {
+      if (switches.output == PROOF)
+	{
+	  indentPrint ();
+	  eprintf ("Pruned: too many instances of a particular role.\n");
+	}
+      return 1;
+    }
+
+  // This needs some foundation. Probably * 2^max_encryption_level
+  //!@todo Remove later
+  /**
+   * This should be removed once the hidelevel lemma works correctly
+   */
+  if (switches.experimental & 1)
+    {
+      if ((switches.match < 2)
+	  && (sys->num_intruder_runs >
+	      ((double) switches.runs * max_encryption_level * 8)))
+	{
+	  // Hardcoded limit on iterations
+	  if (switches.output == PROOF)
+	    {
+	      indentPrint ();
+	      eprintf
+		("Pruned: %i intruder runs is too much. (max encr. level %i)\n",
+		 sys->num_intruder_runs, max_encryption_level);
+	    }
+	  return 1;
+	}
+    }
+
+  // Limit on exceeding any attack length
+  if (get_semitrace_length () >= attack_length)
+    {
+      if (switches.output == PROOF)
+	{
+	  indentPrint ();
+	  eprintf ("Pruned: attack length %i.\n", attack_length);
+	}
+      return 1;
+    }
+
+  /* prune for cheaper */
+  if (switches.prune != 0 && attack_leastcost <= attackCost (sys))
+    {
+      // We already had an attack at least this cheap.
+      if (switches.output == PROOF)
+	{
+	  indentPrint ();
+	  eprintf
+	    ("Pruned: attack cost exceeds a previously found attack.\n");
+	}
+      return 1;
+    }
+
+  // Limit on attack count
+  if (enoughAttacks (sys))
+    return 1;
+
+  // Pruning involving the number of intruder actions
+  {
+    // Count intruder actions
+    int actioncount;
+
+    actioncount = countIntruderActions ();
+
+    // Limit intruder actions in any case
+    if (!switches.intruder)
+      {
+	if (actioncount > 0)
+	  {
+	    if (switches.output == PROOF)
+	      {
+		indentPrint ();
+		eprintf
+		  ("Pruned: no intruder allowed.\n",
+		   switches.maxIntruderActions);
+	      }
+	    return 1;
+	  }
+      }
+
+    // Limit on intruder events count
+    if (actioncount > switches.maxIntruderActions)
+      {
+	if (switches.output == PROOF)
+	  {
+	    indentPrint ();
+	    eprintf
+	      ("Pruned: more than %i encrypt/decrypt events in the semitrace.\n",
+	       switches.maxIntruderActions);
+	  }
+	return 1;
+      }
+  }
+
+  // No pruning because of bounds
+  return 0;
+}
+
+//! Detect when there are too many instances of a certain role
+int
+tooManyOfRole (const System sys)
+{
+  int toomany;
+
+  toomany = false;
+  if (switches.maxOfRole > 0)
+    {
+      Termmap f;
+      int run;
+
+      f = NULL;
+      for (run = 0; run < sys->maxruns; run++)
+	{
+	  if (sys->runs[run].protocol != INTRUDER)
+	    {
+	      // maybe this conflicts with equal protocols...? TODO
+	      Term role;
+	      int count;
+
+	      role = sys->runs[run].role->nameterm;
+	      count = termmapGet (f, role);
+	      if (count == -1)
+		count = 1;
+	      else
+		count++;
+	      f = termmapSet (f, role, count);
+	      if (count > switches.maxOfRole)
+		{
+		  toomany = true;
+		  break;
+		}
+	    }
+	}
+      termmapDelete (f);
+    }
+  return toomany;
+}

gui/src/prune_bounds.h

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

gui/src/prune_theorems.c

@@ -0,0 +1,484 @@
+/**
+ *
+ *@file prune_theorems.c
+ *
+ * Prune stuff based on theorems.
+ * Pruning leaves complete results.
+ *
+ */
+
+#include "system.h"
+#include "list.h"
+#include "switches.h"
+#include "binding.h"
+#include "specialterm.h"
+#include "hidelevel.h"
+#include "depend.h"
+#include "arachne.h"
+#include "error.h"
+#include "type.h"
+
+extern Protocol INTRUDER;
+extern int proofDepth;
+extern int max_encryption_level;
+
+
+//! Check locals occurrence
+/*
+ * Returns true if the order is correct
+ */
+int
+correctLocalOrder (const System sys)
+{
+  int flag;
+
+  int checkRun (int r1)
+  {
+    int checkTerm (Term t)
+    {
+      if (!isTermVariable (t))
+	{
+	  int r2;
+	  int e1, e2;
+
+	  // t is a term from r2 that occurs in r1
+	  r2 = TermRunid (t);
+	  e1 = firstOccurrence (sys, r1, t, ANYEVENT);
+	  if (e1 >= 0)
+	    {
+	      if (roledef_shift (sys->runs[r1].start, e1)->type == READ)
+		{
+		  e2 = firstOccurrence (sys, r2, t, SEND);
+		  if (e2 >= 0)
+		    {
+		      // thus, it should not be the case that e1 occurs before e2
+		      if (isDependEvent (r1, e1, r2, e2))
+			{
+			  // That's not good!
+			  if (switches.output == PROOF)
+			    {
+			      indentPrint ();
+			      eprintf ("Pruned because ordering for term ");
+			      termSubstPrint (t);
+			      eprintf
+				(" cannot be correct: the first send r%ii%i occurs after the read r%ii%i.\n",
+				 r2, e2, r1, e1);
+			    }
+			  flag = false;
+			  return false;
+			}
+		    }
+		  else
+		    {
+		      globalError++;
+		      eprintf ("error: ");
+		      termPrint (sys->runs[r2].protocol->nameterm);
+		      eprintf (",");
+		      termPrint (sys->runs[r2].role->nameterm);
+		      eprintf (": term ");
+		      termSubstPrint (t);
+		      eprintf
+			(" from run %i should occur in run %i, but it doesn't.\n",
+			 r2, r2);
+		      globalError--;
+		      error ("Abort");
+		    }
+		}
+	      else
+		{
+		  // not a read first? That's definitely impossible (can be caused by choices 
+		  globalError++;
+		  eprintf ("error: term ");
+		  termSubstPrint (t);
+		  eprintf
+		    (" from run %i should occur in run %i first in a READ event, but it occurs first in event %i.\n",
+		     r2, r1, e1);
+		  eprintf ("It occurs first in ");
+		  roledefPrint (eventRoledef (sys, r1, e1));
+		  eprintf ("\n");
+		  eprintf ("which starts with ");
+		  roledefPrint (eventRoledef (sys, r1, 0));
+		  eprintf ("\n");
+		  globalError--;
+		  error ("Abort");
+		}
+	    }
+	  else
+	    {
+	      globalError++;
+	      eprintf ("error: term ");
+	      termSubstPrint (t);
+	      eprintf
+		(" from run %i should occur in run %i, but it doesn't.\n", r2,
+		 r1);
+	      globalError--;
+	      error ("Abort");
+	    }
+	}
+      return true;
+    }
+
+    return iterateLocalToOther (sys, r1, checkTerm);
+  }
+
+  flag = true;
+  iterateRegularRuns (sys, checkRun);
+
+  return flag;
+}
+
+//! Check initiator roles
+/**
+ * Returns false iff an agent type is wrong
+ */
+int
+initiatorAgentsType (const System sys)
+{
+  int run;
+
+  run = 0;
+  while (run < sys->maxruns)
+    {
+      // Only for initiators
+      if (sys->runs[run].role->initiator)
+	{
+	  Termlist agents;
+
+	  agents = sys->runs[run].rho;
+	  while (agents != NULL)
+	    {
+	      if (!goodAgentType (agents->term))
+		{
+		  return false;
+		}
+	      agents = agents->next;
+	    }
+	}
+      run++;
+    }
+  return true;			// seems to be okay
+}
+
+//! Prune determination because of theorems
+/**
+ * When something is pruned because of this function, the state space is still
+ * considered to be complete.
+ *
+ *@returns true iff this state is invalid because of a theorem
+ */
+int
+prune_theorems (const System sys)
+{
+  List bl;
+  int run;
+
+  // Check all types of the local agents according to the matching type
+  if (!checkAllSubstitutions (sys))
+    {
+      if (switches.output == PROOF)
+	{
+	  indentPrint ();
+	  eprintf
+	    ("Pruned because some local variable was incorrectly subsituted.\n");
+	}
+      return true;
+    }
+
+  // Check if all actors are agents for responders (initiators come next)
+  run = 0;
+  while (run < sys->maxruns)
+    {
+      if (!sys->runs[run].role->initiator)
+	{
+	  Term actor;
+
+	  actor = agentOfRun (sys, run);
+	  if (!goodAgentType (actor))
+	    {
+	      if (switches.output == PROOF)
+		{
+		  indentPrint ();
+		  eprintf ("Pruned because the actor ");
+		  termPrint (actor);
+		  eprintf (" of run %i is not of a compatible type.\n", run);
+		}
+	      return true;
+	    }
+	}
+      run++;
+    }
+
+  // Prune if any initiator run talks to itself
+  /**
+   * This effectively disallows Alice from talking to Alice, for all
+   * initiators. We still allow it for responder runs, because we assume the
+   * responder is not checking this.
+   */
+  if (switches.initUnique)
+    {
+      if (selfInitiators (sys) > 0)
+	{
+	  // XXX TODO
+	  // Still need to fix proof output for this
+	  //
+	  // Pruning because some agents are equal for this role.
+	  return true;
+	}
+    }
+
+  if (switches.respUnique)
+    {
+      if (selfResponders (sys) > 0)
+	{
+	  // XXX TODO
+	  // Still need to fix proof output for this
+	  //
+	  // Pruning because some agents are equal for this role.
+	  return true;
+	}
+    }
+
+  // Prune wrong agents type for initators
+  if (!initiatorAgentsType (sys))
+    {
+      if (switches.output == PROOF)
+	{
+	  indentPrint ();
+	  eprintf
+	    ("Pruned: an initiator role does not have the correct type for one of its agents.\n");
+	}
+      return true;
+    }
+
+  // Check if the actors of all other runs are not untrusted
+  if (sys->untrusted != NULL)
+    {
+      int run;
+
+      run = 1;
+      while (run < sys->maxruns)
+	{
+	  if (sys->runs[run].protocol != INTRUDER)
+	    {
+	      if (sys->runs[run].rho != NULL)
+		{
+		  Term actor;
+
+		  actor = agentOfRun (sys, run);
+		  if (actor == NULL)
+		    {
+		      error ("Agent of run %i is NULL", run);
+		    }
+		  if (!isAgentTrusted (sys, actor))
+		    {
+		      if (switches.output == PROOF)
+			{
+			  indentPrint ();
+			  eprintf
+			    ("Pruned because the actor of run %i is untrusted.\n",
+			     run);
+			}
+		      return true;
+		    }
+		}
+	      else
+		{
+		  Protocol p;
+
+		  globalError++;
+		  eprintf ("error: Run %i: ", run);
+		  role_name_print (run);
+		  eprintf (" has an empty agents list.\n");
+		  eprintf ("protocol->rolenames: ");
+		  p = (Protocol) sys->runs[run].protocol;
+		  termlistPrint (p->rolenames);
+		  eprintf ("\n");
+		  error ("Aborting.");
+		  globalError--;
+		  return true;
+		}
+	    }
+	  run++;
+	}
+    }
+
+  // Check for c-minimality
+  {
+    if (!bindings_c_minimal ())
+      {
+	if (switches.output == PROOF)
+	  {
+	    indentPrint ();
+	    eprintf ("Pruned because this is not <=c-minimal.\n");
+	  }
+	return true;
+      }
+  }
+
+  /*
+   * Check for correct orderings involving local constants
+   */
+  if (!(switches.experimental & 8))
+    {
+      if (!correctLocalOrder (sys))
+	{
+	  if (switches.output == PROOF)
+	    {
+	      indentPrint ();
+	      eprintf
+		("Pruned because this does not have the correct local order.\n");
+	    }
+	  return true;
+	}
+    }
+
+  /**
+   * Check whether the bindings are valid
+   */
+  bl = sys->bindings;
+  while (bl != NULL)
+    {
+      Binding b;
+
+      b = bl->data;
+
+      // Check for "Hidden" interm goals
+      //! @todo in the future, this can be subsumed by adding TERM_Hidden to the hidelevel constructs
+      if (termInTerm (b->term, TERM_Hidden))
+	{
+	  // Prune the state: we can never meet this
+	  if (switches.output == PROOF)
+	    {
+	      indentPrint ();
+	      eprintf ("Pruned because intruder can never construnct ");
+	      termPrint (b->term);
+	      eprintf ("\n");
+	    }
+	  return true;
+	}
+
+      if (switches.experimental & 4)
+	{
+	  // Check for SK-type function occurrences
+	  //!@todo Needs a LEMMA, although this seems to be quite straightforward to prove.
+	  // The idea is that functions are never sent as a whole, but only used in applications.
+	  //! @todo Subsumed by hidelevel lemma later
+	  if (isTermFunctionName (b->term))
+	    {
+	      if (!inKnowledge (sys->know, b->term))
+		{
+		  // Not in initial knowledge of the intruder
+		  if (switches.output == PROOF)
+		    {
+		      indentPrint ();
+		      eprintf ("Pruned because the function ");
+		      termPrint (b->term);
+		      eprintf (" is not known initially to the intruder.\n");
+		    }
+		  return true;
+		}
+	    }
+	}
+
+      // Check for encryption levels
+      /*
+       * if (switches.match < 2
+       *! @todo Doesn't work yet as desired for Tickets. Prove lemma first.
+       */
+      if (switches.experimental & 2)
+	{
+	  if (!hasTicketSubterm (b->term))
+	    {
+	      if (term_encryption_level (b->term) > max_encryption_level)
+		{
+		  // Prune: we do not need to construct such terms
+		  if (switches.output == PROOF)
+		    {
+		      indentPrint ();
+		      eprintf ("Pruned because the encryption level of ");
+		      termPrint (b->term);
+		      eprintf (" is too high.\n");
+		    }
+		  return true;
+		}
+	    }
+	}
+
+      // To be on the safe side, we currently limit the encryption level. 
+      /**
+       * This is not a problem for known attacks, but should be addressed more
+       * carefully at some point.  If there are variables that can contain
+       * encryptions, this is maybe not correct: make proof!
+       *
+       * @todo Fix untyped variables reasoning
+       */
+      if (term_encryption_level (b->term) > max_encryption_level)
+	{
+	  // Prune: we do not need to construct such terms
+	  if (switches.output == PROOF)
+	    {
+	      indentPrint ();
+	      eprintf ("Pruned because the encryption level of ");
+	      termPrint (b->term);
+	      eprintf (" is too high.\n");
+	    }
+	  return true;
+	}
+
+      /**
+       * Prune on the basis of hidelevel lemma
+       */
+      if (hidelevelImpossible (sys, b->term))
+	{
+	  // Prune: we do not need to construct such terms
+	  if (switches.output == PROOF)
+	    {
+	      indentPrint ();
+	      eprintf ("Pruned because the hidelevel of ");
+	      termPrint (b->term);
+	      eprintf (" is impossible to satisfy.\n");
+	    }
+	  return true;
+	}
+
+      bl = bl->next;
+    }
+
+  /* check for singular roles */
+  run = 0;
+  while (run < sys->maxruns)
+    {
+      if (sys->runs[run].role->singular)
+	{
+	  // This is a singular role: it therefore should not occur later on again.
+	  int run2;
+	  Term rolename;
+
+	  rolename = sys->runs[run].role->nameterm;
+	  run2 = run + 1;
+	  while (run2 < sys->maxruns)
+	    {
+	      Term rolename2;
+
+	      rolename2 = sys->runs[run2].role->nameterm;
+	      if (isTermEqual (rolename, rolename2))
+		{
+		  // This is not allowed: the singular role occurs twice in the semitrace.
+		  // Thus we prune.
+		  if (switches.output == PROOF)
+		    {
+		      indentPrint ();
+		      eprintf ("Pruned because the singular role ");
+		      termPrint (rolename);
+		      eprintf (" occurs more than once in the semitrace.\n");
+		    }
+		  return true;
+		}
+	      run2++;
+	    }
+	}
+      run++;
+    }
+
+  return false;
+}

gui/src/prune_theorems.h

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

gui/src/reindent.sh

@@ -0,0 +1,5 @@
+#!/bin/sh
+# 
+# Indent any changed files, ending in .c or .h
+#
+svn st | grep "^[MA].*\.[ch]$"| awk '{print $2}' | xargs indent

gui/src/releases.txt

@@ -0,0 +1,33 @@
+?		bonk
+	- New partial order reduction method.
+	Maybe CLP/t4
+	maybe MSC stuff
+
+2004-02-19	billionaire
+	- replace substitutions with implicit substitutions.
+	- many syntax updates.
+	- many speed improvements.
+
+2004-01-20	alpha1
+	teehee_valley with a couple of minor bugfixes.
+	- Shows error line correctly on parse.
+	- Allows for multi-line comments.
+
+2004-01-20	teehee_valley
+	Nicely working role-based release, can test stdin scenario files.
+	- Preliminary untrusted support.
+	- Public, inversekeys are working.
+	- No tickets yet.
+
+2004-01-19	amoxicillin	
+	Preliminary compiler test release.
+	- Compiler works in ptest, now we can integrate it into the main
+	  part, and throw out the scenarios.
+	  
+2003		dead_ringers
+	A first working release.
+	- -t0 through -t2 implemented.
+	- Typed matching matches all basic terms.
+	- CLP matching works (-m2), but is not compatible with -t2.
+	- Hard coded protocols, inclusion through Makefile.
+

gui/src/role.c

@@ -0,0 +1,515 @@
+/**
+ * @file role.c 
+ * \brief role related logic.
+ */
+#include <stdlib.h>
+#include <stdio.h>
+#include <string.h>
+#include <limits.h>
+#include "term.h"
+#include "termlist.h"
+#include "knowledge.h"
+#include "system.h"
+#include "debug.h"
+#include "error.h"
+#include "role.h"
+
+extern int protocolCount;	// from system.c
+
+//! Allocate memory the size of a roledef struct.
+Roledef
+makeRoledef ()
+{
+  return (Roledef) malloc (sizeof (struct roledef));
+}
+
+//! Print a role event.
+/**
+ * If print_actor is true, the actor is included (OS version), otherwise it is left out (short stuff)
+ */
+void
+roledefPrintGeneric (Roledef rd, int print_actor)
+{
+  if (rd == NULL)
+    {
+      eprintf ("[Empty roledef]");
+      return;
+    }
+  if (rd->type == READ && rd->internal)
+    {
+      /* special case: internal read == choose ! */
+      eprintf ("CHOOSE(");
+      termPrint (rd->message);
+      eprintf (")");
+      return;
+    }
+  if (rd->type == READ)
+    eprintf ("READ");
+  if (rd->type == SEND)
+    eprintf ("SEND");
+  if (rd->type == CLAIM)
+    eprintf ("CLAIM");
+  if (rd->label != NULL)
+    {
+      //! Print label
+      Term label;
+
+      /* Old version: sometimes prints protocol stuff (really unique labels)
+         label = deVar (rd->label);
+         if (protocolCount < 2 && realTermTuple (label))
+         {
+         // Only one protocol, so we don't need to show the extra label info
+         label = TermOp2 (label);
+         }
+       */
+      label = deVar (rd->label);
+      if (realTermTuple (label))
+	{
+	  label = TermOp2 (label);
+	}
+
+      eprintf ("_");
+      termPrint (label);
+    }
+  eprintf ("(");
+  if (!(rd->from == NULL && rd->to == NULL))
+    {
+      if (print_actor || rd->type == READ)
+	{
+	  termPrint (rd->from);
+	  eprintf (",");
+	}
+      if (rd->type == CLAIM)
+	eprintf (" ");
+      if (print_actor || rd->type != READ)
+	{
+	  termPrint (rd->to);
+	  eprintf (", ");
+	}
+    }
+  termPrint (rd->message);
+  eprintf (" )");
+}
+
+//! Print a roledef
+void
+roledefPrint (Roledef rd)
+{
+  roledefPrintGeneric (rd, 1);
+}
+
+//! Print a roledef, but shorten it
+void
+roledefPrintShort (Roledef rd)
+{
+  roledefPrintGeneric (rd, 0);
+}
+
+
+//! Duplicate a single role event node.
+/**
+ *\sa roledefDelete()
+ */
+Roledef
+roledefDuplicate1 (const Roledef rd)
+{
+  Roledef newrd;
+
+  if (rd == NULL)
+    return NULL;
+  newrd = makeRoledef ();
+  memcpy (newrd, rd, sizeof (struct roledef));
+  newrd->next = NULL;
+  return newrd;
+}
+
+//! Duplicate a role event list.
+/**
+ *\sa roledefDelete()
+ */
+Roledef
+roledefDuplicate (Roledef rd)
+{
+  Roledef newrd;
+
+  if (rd == NULL)
+    return NULL;
+  newrd = roledefDuplicate1 (rd);
+  newrd->next = roledefDuplicate (rd->next);
+  return newrd;
+}
+
+//! Delete a role event or event list.
+/**
+ *\sa roledefDuplicate()
+ */
+void
+roledefDelete (Roledef rd)
+{
+  if (rd == NULL)
+    return;
+  roledefDelete (rd->next);
+  free (rd);
+  return;
+}
+
+//! Destroy a role event or event list.
+void
+roledefDestroy (Roledef rd)
+{
+  if (rd == NULL)
+    return;
+  roledefDestroy (rd->next);
+  termDelete (rd->from);
+  termDelete (rd->to);
+  termDelete (rd->message);
+  free (rd);
+  return;
+}
+
+//! Make a new role event with the specified parameters.
+/**
+ *@return A pointer to a new role event with the given parameters.
+ */
+Roledef
+roledefInit (int type, Term label, Term from, Term to, Term msg, Claimlist cl)
+{
+  Roledef newEvent;
+
+  newEvent = makeRoledef ();
+  newEvent->internal = 0;
+  newEvent->type = type;
+  newEvent->label = label;
+  newEvent->from = from;
+  newEvent->to = to;
+  newEvent->message = msg;
+  newEvent->forbidden = NULL;	// no forbidden stuff
+  newEvent->knowPhase = -1;	// we haven't explored any knowledge yet
+  newEvent->claiminfo = cl;	// only for claims
+  if (type == READ)
+    newEvent->bound = 0;	// bound goal (Used for arachne only). Technically involves choose events as well.
+  else
+    newEvent->bound = 1;	// other stuff does not need to be bound
+  newEvent->next = NULL;
+  newEvent->lineno = 0;
+  return newEvent;
+}
+
+//! Add a role event to an existing list, with the given parameters.
+/**
+ *\sa roledefInit()
+ */
+Roledef
+roledefAdd (Roledef rd, int type, Term label, Term from, Term to, Term msg,
+	    Claimlist cl)
+{
+  Roledef scan;
+
+  if (rd == NULL)
+    return roledefInit (type, label, from, to, msg, cl);
+
+  scan = rd;
+  while (scan->next != NULL)
+    scan = scan->next;
+  scan->next = roledefInit (type, label, from, to, msg, cl);
+  return rd;
+}
+
+//! Create an empty role structure with a name.
+Role
+roleCreate (Term name)
+{
+  Role r;
+
+  r = malloc (sizeof (struct role));
+  r->nameterm = name;
+  r->roledef = NULL;
+  r->locals = NULL;
+  r->variables = NULL;
+  r->declaredvars = NULL;
+  r->declaredconsts = NULL;
+  r->initiator = 1;		//! Will be determined later, if a read is the first action (in compiler.c)
+  r->singular = false;		// by default, a role is not singular
+  r->next = NULL;
+  r->knows = NULL;
+  r->lineno = 0;
+  return r;
+}
+
+//! Print a role.
+void
+rolePrint (Role r)
+{
+  Roledef rd;
+
+  if (r == NULL)
+    return;
+
+  indent ();
+  eprintf ("[[Role : ");
+  termPrint (r->nameterm);
+  eprintf ("]]\n");
+  locVarPrint (r->locals);
+
+  rd = r->roledef;
+  while (rd != NULL)
+    {
+      roledefPrint (rd);
+      eprintf ("\n");
+      rd = rd->next;
+    }
+}
+
+//! Print a list of roles.
+void
+rolesPrint (Role r)
+{
+  if (r == NULL)
+    {
+      eprintf ("Empty role.");
+    }
+  else
+    {
+      while (r != NULL)
+	{
+	  rolePrint (r);
+	  r = r->next;
+	}
+    }
+}
+
+//! Iterate over the events in a roledef list
+/**
+ * Function gets roledef pointer
+ */
+int
+roledef_iterate_events (Roledef rd, int (*func) ())
+{
+  while (rd != NULL)
+    {
+      if (!func (rd))
+	return 0;
+      rd = rd->next;
+    }
+  return 1;
+}
+
+//! Roledef length
+/**
+ * Would be faster hard-coded,
+ * but this just shows the use of the iteration.
+ */
+int
+roledef_length (const Roledef rd)
+{
+  int count = 0;
+  int countplus (Roledef rd)
+  {
+    count++;
+    return 1;
+  }
+  roledef_iterate_events (rd, countplus);
+  return count;
+}
+
+//! Yield roledef pointer for a given index
+Roledef
+roledef_shift (Roledef rd, int i)
+{
+  while (i > 0 && rd != NULL)
+    {
+      rd = rd->next;
+      i--;
+    }
+  return rd;
+}
+
+//! Check whether a term is a subterm of a roledef
+int
+roledefSubTerm (Roledef rd, Term tsub)
+{
+  if (rd == NULL)
+    {
+      return false;
+    }
+  else
+    {
+      return (termSubTerm (rd->from, tsub) ||
+	      termSubTerm (rd->to, tsub) || termSubTerm (rd->message, tsub));
+    }
+}
+
+/*
+ * Some stuff directly from the semantics
+ */
+
+//! Is a term readable (from some knowledge set)
+/**
+ * Returns value of predicate
+ */
+int
+Readable (Knowledge know, Term t)
+{
+  if (isTermVariable (t))
+    {
+      // Variable pattern
+      return true;
+    }
+  if (!isTermLeaf (t))
+    {
+      if (isTermTuple (t))
+	{
+	  // Tuple pattern
+	  Knowledge knowalt;
+	  int both;
+
+	  both = false;
+	  knowalt = knowledgeDuplicate (know);
+	  knowledgeAddTerm (knowalt, TermOp2 (t));
+	  if (Readable (knowalt, TermOp1 (t)))
+	    {
+	      // Yes, left half works
+	      knowledgeDelete (knowalt);
+	      knowalt = knowledgeDuplicate (know);
+	      knowledgeAddTerm (knowalt, TermOp1 (t));
+	      if (Readable (knowalt, TermOp2 (t)))
+		{
+		  both = true;
+		}
+	    }
+	  knowledgeDelete (knowalt);
+	  return both;
+	}
+      else
+	{
+	  // Encryption pattern
+	  // But we exclude functions
+	  if (getTermFunction (t) == NULL)
+	    {
+	      // Real encryption pattern
+	      Term inv;
+	      int either;
+
+	      // Left disjunct
+	      if (inKnowledge (know, t))
+		{
+		  return true;
+		}
+	      // Right disjunct
+	      inv = inverseKey (know->inverses, TermKey (t));
+	      either = false;
+	      if (inKnowledge (know, inv))
+		{
+		  if (Readable (know, TermOp (t)))
+		    {
+		      either = true;
+		    }
+		}
+	      termDelete (inv);
+	      return either;
+	    }
+	}
+    }
+  return inKnowledge (know, t);
+}
+
+//! Well-formed error reporting.
+void
+wfeError (Knowledge know, Roledef rd, char *errorstring, Term was,
+	  Term shouldbe)
+{
+  globalError++;
+  eprintf ("Well-formedness error.\n");
+  roledefPrint (rd);
+  eprintf ("\nKnowing ");
+  knowledgePrintShort (know);
+  eprintf ("\n");
+  if (was != NULL || shouldbe != NULL)
+    {
+      eprintf ("while parsing ");
+      termPrint (was);
+      if (shouldbe != NULL)
+	{
+	  eprintf (" which should have been ");
+	  termPrint (shouldbe);
+	}
+      eprintf ("\n");
+    }
+  globalError--;
+  error (errorstring);
+}
+
+
+//! Is an event well-formed
+/**
+ * Returns the new knowledge or NULL if it was not well-formed.
+ */
+Knowledge
+WellFormedEvent (Term role, Knowledge know, Roledef rd)
+{
+  if (rd == NULL)
+    {
+      return know;
+    }
+  if (rd->type == READ)
+    {
+      // Read
+      if (!isTermEqual (role, rd->to))
+	{
+	  wfeError (know, rd, "Reading role incorrect.", rd->to, role);
+	  return NULL;
+	}
+      if (!inKnowledge (know, rd->from))
+	{
+	  wfeError (know, rd, "Unknown sender role.", rd->from, NULL);
+	  return NULL;
+
+	}
+      if (!Readable (know, rd->message))
+	{
+	  wfeError (know, rd, "Cannot read message pattern.", rd->message,
+		    NULL);
+	  return NULL;
+	}
+      knowledgeAddTerm (know, rd->message);
+      return know;
+    }
+  if (rd->type == SEND)
+    {
+      // Send
+      if (!isTermEqual (role, rd->from))
+	{
+	  wfeError (know, rd, "Sending role incorrect.", rd->from, role);
+	  return NULL;
+	}
+      if (!inKnowledge (know, rd->to))
+	{
+	  wfeError (know, rd, "Unknown reading role.", rd->to, NULL);
+	  return NULL;
+
+	}
+      if (!inKnowledge (know, rd->message))
+	{
+	  wfeError (know, rd, "Unable to construct message.", rd->message,
+		    NULL);
+	  return NULL;
+	}
+      return know;
+    }
+  if (rd->type == CLAIM)
+    {
+      // Claim
+      if (!isTermEqual (role, rd->from))
+	{
+	  wfeError (know, rd, "Claiming role incorrect.", rd->from, role);
+	  return NULL;
+	}
+      return know;
+    }
+  // Unknown, false
+  globalError++;
+  roledefPrint (rd);
+  globalError--;
+  error ("I don't know this event");
+  return NULL;
+}

gui/src/role.h

@@ -0,0 +1,174 @@
+#ifndef ROLES
+#define ROLES
+
+#include "term.h"
+#include "termmap.h"
+#include "termlist.h"
+#include "knowledge.h"
+#include "states.h"
+
+enum eventtype
+{ READ, SEND, CLAIM, ANYEVENT };
+
+//! The container for the claim info list
+/**
+ * Defaults are set in compiler.c (claimCreate)
+ */
+struct claimlist
+{
+  //! The type of claim
+  Term type;
+  //! The term element for this node.
+  Term label;
+  //! Any parameters
+  Term parameter;
+  //! The pointer to the protocol (not defined typically, because
+  //! at compile time of the claim the protocol structure is not known yet.)
+  void *protocol;
+  //! The name of the role in which it occurs.
+  Term rolename;
+  //! The pointer to the role structure
+  void *role;
+  //! The pointer to the roledef
+  void *roledef;
+  //! Number of occurrences in system exploration.
+  states_t count;
+  //! Number of occurrences that failed.
+  states_t failed;
+  //! Number of iterations traversed for this claim.
+  states_t states;
+  //! Whether the result is complete or not (failings always are!)
+  int complete;
+  //! If we ran into the time bound (incomplete, and bad for results)
+  int timebound;
+  //! Some claims are always true (shown by the initial scan)
+  int alwaystrue;
+  //! Warnings should tell you more
+  int warnings;
+
+  int r;			//!< role number for mapping
+  int ev;			//!< event index in role
+  //! Preceding label list
+  Termlist prec;
+  //! Roles that are involved (nameterms)
+  Termlist roles;
+  //! Next node pointer or NULL for the last element of the function.
+  struct claimlist *next;
+
+  int lineno;
+};
+
+//! Shorthand for claimlist pointers.
+typedef struct claimlist *Claimlist;
+
+//! Structure for a role event node or list.
+/**
+ *\sa role
+ */
+struct roledef
+{
+  //! flag for internal actions.
+  /**
+   * Typically, this is true to signify internal reads (e.g. variable choices)
+   * as opposed to a normal read.
+   */
+  int internal;
+  //! Type of event.
+  /**
+   *\sa READ, SEND, CLAIM
+   */
+  int type;
+  //! Event label.
+  Term label;
+  //! Event sender.
+  Term from;
+  //! Event target.
+  Term to;
+  //! Event message.
+  Term message;
+  //! Pointer to next roledef node.
+  struct roledef *next;
+
+  /*
+   * Substructure for reads
+   */
+  //! Illegal injections for this event.
+  /**
+   * For send this means that the send is allowed if it is NULL, otherwise it is blocked.
+   */
+  Knowledge forbidden;
+  //! knowledge transitions counter.
+  int knowPhase;
+
+  /*
+   * Substructure for claims
+   */
+  //! Pointer to claim type info
+  Claimlist claiminfo;
+
+  /*
+   * Bindings for Arachne engine
+   */
+  int bound;			//!< determines whether it is already bound
+
+  /* evt runid for synchronisation, but that is implied in the
+     base array */
+  int lineno;
+};
+
+//! Shorthand for roledef pointer.
+typedef struct roledef *Roledef;
+
+//! Role definition.
+/**
+ *\sa roledef
+ */
+struct role
+{
+  //! Name of the role encoded in a term.
+  Term nameterm;
+  //! List of role events.
+  Roledef roledef;
+  //! Local constants for this role.
+  Termlist locals;
+  //! Local variables for this role.
+  Termlist variables;
+  //! Declared constants for this role
+  Termlist declaredconsts;
+  //! Declared variables for this role
+  Termlist declaredvars;
+  //! Initial role knowledge
+  Termlist knows;
+  //! Flag for initiator roles
+  int initiator;
+  //! Flag for singular roles
+  int singular;
+  //! Pointer to next role definition.
+  struct role *next;
+  //! Line number
+  int lineno;
+};
+
+//! Shorthand for role pointer.
+typedef struct role *Role;
+
+void roledefPrint (Roledef rd);
+void roledefPrintShort (Roledef rd);
+Roledef roledefDuplicate1 (const Roledef rd);
+Roledef roledefDuplicate (Roledef rd);
+void roledefDelete (Roledef rd);
+void roledefDestroy (Roledef rd);
+Roledef roledefInit (int type, Term label, Term from, Term to, Term msg,
+		     Claimlist cl);
+Roledef roledefAdd (Roledef rd, int type, Term label, Term from, Term to,
+		    Term msg, Claimlist cl);
+Role roleCreate (Term nameterm);
+void rolePrint (Role r);
+void rolesPrint (Role r);
+int roledef_iterate_events (Roledef rd, int (*func) ());
+int roledef_length (const Roledef rd);
+Roledef roledef_shift (Roledef rd, int i);
+int roledefSubTerm (Roledef rd, Term tsub);
+Knowledge WellFormedEvent (Term role, Knowledge know, Roledef rd);
+
+#endif

gui/src/scanner.l

@@ -0,0 +1,227 @@
+%option yylineno
+
+%{
+/* scanner for security protocols language */
+
+#include <strings.h>
+#include "pheading.h"
+#include "tac.h"
+#include "switches.h"
+#include "error.h"
+
+/* tokens for language */
+#include "parser.h"
+
+void mkname(char *name);
+void mkval(void);
+void mktext(void);
+
+int yyerror(char *s);
+
+Symbol mkstring(char *name);
+
+struct stringlist {
+	char*			string;
+	struct stringlist*	next;
+};
+
+typedef struct stringlist* Stringlist;
+
+static Stringlist allocatedStrings = NULL;
+
+
+int mylineno = 0;
+
+%}
+
+comment1	"//".*
+comment2	"#".*
+delimiter	[ \t\r\n]
+whitespace	{delimiter}+
+uc_letter	[A-Z]
+lc_letter	[a-z]
+letter		{lc_letter}|{uc_letter}
+digit		[0-9]
+ascii_char	[^\"\n]
+escaped_char	\\n|\\\"
+integer		{digit}+
+text		\"({ascii_char}|{escaped_char})*\"
+id		@?({letter}|{digit}|[\^\-!'])+
+
+/* the "incl" state is used for picking up the name of an include file
+ */
+%x incl inclend
+
+%{
+#define MAX_INCLUDE_DEPTH 10
+YY_BUFFER_STATE include_stack[MAX_INCLUDE_DEPTH];
+int include_stack_ptr = 0;
+%}
+
+%%
+include		BEGIN(incl);
+<incl>[ \t]*\"	/* eat the whitespace */
+<incl>[^\"]+	{ /* got the include file name */
+	                 if ( include_stack_ptr >= MAX_INCLUDE_DEPTH )
+	                     {
+	                     printfstderr( "Includes nested too deeply" );
+	                     exit( 1 );
+	                     }
+	
+	                 include_stack[include_stack_ptr++] =
+	                     YY_CURRENT_BUFFER;
+	
+			 /* try to open, using scytherdirs environment variable as well. */
+			 yyin = openFileSearch (yytext, NULL);
+	
+			 if (! yyin)
+			 {
+			 	error ("could not open include file %s.", yytext);
+			 }
+	
+	                 yy_switch_to_buffer(
+	                     yy_create_buffer( yyin, YY_BUF_SIZE ) );
+	
+	                 BEGIN(INITIAL);
+		}
+
+<inclend>\";?	{ /* eat the closing things */
+			BEGIN(INITIAL);
+		}
+
+<INITIAL><<EOF>>	{
+                 if ( --include_stack_ptr < 0 )
+                     {
+                        yyterminate();
+                     }
+
+                 else
+                     {
+                     	yy_delete_buffer( YY_CURRENT_BUFFER );
+                     	yy_switch_to_buffer(
+                        include_stack[include_stack_ptr] );
+			BEGIN(inclend);
+                     }
+		}
+
+"/*"		{
+			register int c;
+
+			for ( ; ; )
+                        {
+                        	while ( (c = input()) != '*' && c != '\n' && c != EOF )
+                                      ;    /* eat up text of comment */
+
+                                if ( c == '*' )
+                                {
+                                	while ( (c = input()) == '*' )
+                                        	;
+                                      	if ( c == '/' )
+                                        	break;    /* found the end */
+                                }
+
+				if (c == '\n')
+					mylineno++;
+
+                                if ( c == EOF )
+                                {
+                                	yyerror( "EOF in comment" );
+                                	break;
+                        	}
+                	}
+                }
+
+\n		{ mylineno++; }
+{whitespace}	{ }
+{comment1}	{ }
+{comment2}	{ }
+
+protocol	{ return PROTOCOL; }
+role		{ return ROLE; }
+read		{ return READT; }
+send		{ return SENDT; }
+var		{ return VAR; }
+const		{ return CONST; }
+claim		{ return CLAIMT; }
+run		{ return RUN; }
+secret		{ return SECRET; }
+inversekeys	{ return INVERSEKEYS; }
+untrusted	{ return UNTRUSTED; }
+compromised	{ return COMPROMISED; }
+usertype	{ return USERTYPE; }
+singular	{ return SINGULAR; }
+function	{ return FUNCTION; }
+hashfunction	{ return HASHFUNCTION; }
+knows		{ return KNOWS; }
+trusted		{ return TRUSTED; }
+{id}		{	
+			yylval.symb = mkstring(yytext);
+			return ID;
+		}
+.		{ return yytext[0]; }
+
+
+
+%%
+
+Symbol mkstring(char *name)
+{
+	Symbol t;
+	char* s;
+	Stringlist sl;
+	int len;
+
+	if (( t = lookup(name)) != NULL)
+	{
+		return t;
+	}
+	// make new name
+	len = strlen(name);
+	s = (char *)malloc(len+1);
+	sl = (Stringlist) malloc(sizeof(struct stringlist));
+	strncpy(s,name,len);
+	sl->next = allocatedStrings;
+	allocatedStrings = sl;
+	sl->string = s;
+	s[len] = EOS;
+
+	t = get_symb();
+	t->lineno = yylineno;
+	t->type = T_UNDEF;
+	t->text = s;
+
+	insert(t);
+	return t;
+}
+
+void scanner_cleanup(void)
+{
+	yy_delete_buffer (YY_CURRENT_BUFFER);
+}
+
+void strings_cleanup(void)
+{
+	Stringlist sl;
+	while (allocatedStrings != NULL)
+	{
+		sl = allocatedStrings;
+		allocatedStrings = sl->next;
+		free(sl->string);
+		free(sl);
+	}
+}
+
+int yywrap (void)
+{
+  /* signal true to let lex know that nothing else is coming */
+  return 1;
+}
+
+
+/*
+void mkval(void);
+void mktext(void);
+*/
+
+
+// vim:ft=lex:

gui/src/scantags.py

@@ -0,0 +1,119 @@
+#!/usr/bin/python
+
+import commands
+import sys
+
+class Tag(object):
+    """
+    Object for tag (ctag line)
+    """
+
+    def __init__(self,tagline):
+        tl = tagline.strip().split('\t')
+        self.id = tl[0]
+        self.filename = tl[1]
+
+    def __str__(self):
+        return self.id
+
+class GrepRes(object):
+    """
+    Object for a result line from grep
+    """
+
+    def __init__(self,line):
+        self.line = line
+        x = line.find(":")
+        if x:
+            self.filename = line[:x]
+            self.text = line[x:].strip()
+        else:
+            self.filename = None
+            self.text = None
+
+    def __str__(self):
+        return self.line
+
+
+def outToRes(out,filter=[]):
+    """
+    filter grep output and make a list of GrepRes objects. Filter out
+    any that come from the filenames in the filter list. Also return the
+    count of all results (not taking the filter into account).
+    """
+
+    reslist = []
+    count = 0
+    for l in out.splitlines():
+        gr = GrepRes(l)
+        if gr.filename not in filter:
+            reslist.append(gr)
+        count = count+1
+    return (reslist,count)
+
+def gettags():
+    """
+    Get all the tags in a list
+    """
+
+    f = open("tags","r")
+    tags = []
+    for l in f.readlines():
+        if not l.startswith("!"):
+            tags.append(Tag(l))
+    f.close()
+    return tags
+
+def tagoccurs(problems,tag,filter=[]):
+    """
+    Check tag occurrences in certain files and show interesting ones.
+    """
+
+    cmd = "grep \"\\<%s\\>\" *.[chly]" % tag
+    (reslist,count) = outToRes(commands.getoutput(cmd),[tag.filename])
+    if (len(reslist) == 0) and (count < 2):
+        if tag.filename not in filter:
+            # this might be a problem, store it
+            if tag.filename not in problems.keys():
+                problems[tag.filename] = {}
+            problems[tag.filename][tag.id] = count
+
+    return problems
+
+
+def tagreport(problems):
+    for fn in problems.keys():
+        print "file: %s" % fn
+        for t in problems[fn].keys():
+            print "\t%i\t%s" % (problems[fn][t],t)
+
+
+def main():
+    # Generate tags
+    print "Generating tags using 'ctags'"
+    cmd = "ctags *.c *.h *.l *.y"
+    commands.getoutput(cmd)
+
+    # Analyze results
+    print "Analyzing results"
+    filter = ["scanner.c","parser.c"]
+    tags = gettags()
+    problems = {}
+    total = len(tags)
+    count = 0
+    steps = 20
+    print "_ " * (steps)
+
+    for t in tags:
+        problems = tagoccurs(problems,t,filter)
+        count = count + 1
+        if count % (total / steps) == 0:
+            print "^",
+            sys.stdout.flush()
+    print
+    print
+
+    tagreport (problems)
+
+main()
+

gui/src/specialterm.c

@@ -0,0 +1,97 @@
+#include <stdlib.h>
+#include <stdio.h>
+#include "term.h"
+#include "termlist.h"
+#include "compiler.h"
+#include "error.h"
+
+/*
+ * Some macros
+ */
+#define langhide(x,y) x = levelConst(symbolSysConst(" _" 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:
+ */
+
+Term TERM_Agent;
+Term TERM_Function;
+Term TERM_Hidden;
+Term TERM_Type;
+Term TERM_Nonce;
+Term TERM_Ticket;
+Term TERM_Data;
+
+Term TERM_Claim;
+Term CLAIM_Secret;
+Term CLAIM_Nisynch;
+Term CLAIM_Niagree;
+Term CLAIM_Empty;
+Term CLAIM_Reachable;
+
+Termlist CLAIMS_dep_prec;
+
+//! Init special terms
+/**
+ * This is called by compilerInit
+ */
+void
+specialTermInit (const System sys)
+{
+  /* Init system constants */
+
+  langhide (TERM_Type, "Type");
+  langhide (TERM_Hidden, "Hidden");
+  langhide (TERM_Claim, "Claim");
+
+  langcons (TERM_Agent, "Agent", TERM_Type);
+  langcons (TERM_Function, "Function", TERM_Type);
+  langcons (TERM_Nonce, "Nonce", TERM_Type);
+  langcons (TERM_Ticket, "Ticket", TERM_Type);
+  langcons (TERM_Data, "Data", TERM_Type);
+
+  langcons (CLAIM_Secret, "Secret", TERM_Claim);
+  langcons (CLAIM_Nisynch, "Nisynch", TERM_Claim);
+  langcons (CLAIM_Niagree, "Niagree", TERM_Claim);
+  langcons (CLAIM_Empty, "Empty", TERM_Claim);
+  langcons (CLAIM_Reachable, "Reachable", TERM_Claim);
+
+  /* Construct a list of claims that depend on prec being not-empty */
+  /* basically all authentication claims */
+  CLAIMS_dep_prec = termlistAdd (NULL, CLAIM_Niagree);
+  CLAIMS_dep_prec = termlistAdd (CLAIMS_dep_prec, CLAIM_Nisynch);
+
+}
+
+//! Determine whether this is a leaf construct with a ticket in it
+int
+isTicketTerm (Term t)
+{
+  if (t != NULL)
+    {
+      if (realTermLeaf (t))
+	{
+	  if (inTermlist (t->stype, TERM_Ticket))
+	    {
+	      return true;
+	    }
+	  else
+	    {
+	      if (realTermVariable (t))
+		{
+		  return isTicketTerm (t->subst);
+		}
+	    }
+	}
+    }
+  return false;
+}
+
+//! Determine whether this is a term with a Ticket in it
+int
+hasTicketSubterm (Term t)
+{
+  // Doesn't work yet
+  return true;
+}

gui/src/specialterm.h

@@ -0,0 +1,33 @@
+#ifndef SPECIALTERM
+#define SPECIALTERM
+
+#include "term.h"
+#include "termlist.h"
+#include "system.h"
+
+/*
+ * Some declarations in spercialterm.c
+ */
+
+extern Term TERM_Agent;
+extern Term TERM_Function;
+extern Term TERM_Hidden;
+extern Term TERM_Type;
+extern Term TERM_Nonce;
+extern Term TERM_Ticket;
+extern Term TERM_Data;
+
+extern Term TERM_Claim;
+extern Term CLAIM_Secret;
+extern Term CLAIM_Nisynch;
+extern Term CLAIM_Niagree;
+extern Term CLAIM_Empty;
+extern Term CLAIM_Reachable;
+
+extern Termlist CLAIMS_dep_prec;
+
+void specialTermInit (const System sys);
+int isTicketTerm (Term t);
+int hasTicketSubterm (Term t);
+
+#endif

gui/src/states.c

@@ -0,0 +1,38 @@
+#include "states.h"
+#include "symbol.h"
+
+/* States counter operations
+ *
+ * Note that these are also used for encountered claims and such.
+ */
+
+__inline__ states_t
+statesIncrease (const states_t states)
+{
+  return states + 1;
+}
+
+__inline__ double
+statesDouble (const states_t states)
+{
+  return (double) states;
+}
+
+__inline__ int
+statesSmallerThan (const states_t states, unsigned long int reflint)
+{
+  if (states < (states_t) reflint)
+    return 1;
+  else
+    return 0;
+}
+
+//! Sensible output for number of states/claims
+/**
+ * Acts like a modified form of %g
+ */
+__inline__ void
+statesFormat (const states_t states)
+{
+  eprintf ("%lu", states);
+}

gui/src/states.h

@@ -0,0 +1,21 @@
+#ifndef STATES
+#define STATES
+/**
+ * Header file for the states counter datatype.
+ *
+ * Previously, the states number was just a unsigned int, but that
+ * turned out to be insufficient.
+ */
+
+#include <stdio.h>
+
+typedef unsigned long int states_t;
+#define STATES0 0
+
+__inline__ states_t statesIncrease (const states_t states);
+__inline__ double statesDouble (const states_t states);
+__inline__ int statesSmallerThan (const states_t states,
+				  unsigned long int reflint);
+__inline__ void statesFormat (const states_t states);
+
+#endif

gui/src/subbuild-mac-universal.sh

@@ -0,0 +1,21 @@
+#!/bin/sh
+
+# Default flags
+CMFLAGS="-D CMAKE_BUILD_TYPE:STRING=Release"
+
+# Make for ppc and intel, and combine into universal binary
+cmake $CMFLAGS -D TARGETOS=MacPPC   . && make
+cmake $CMFLAGS -D TARGETOS=MacIntel . && make
+cmake $CMFLAGS                      . && make scyther-mac
+
+echo 
+echo
+echo "---------------------------------------------------------"
+echo "Built the Mac universal binary"
+
+# Copy to the correct locations
+cp scyther-mac ../gui/Scyther/Bin
+
+echo Copied the files to their respective locations
+echo "---------------------------------------------------------"
+

gui/src/subbuild-unix-both.sh

@@ -0,0 +1,24 @@
+#!/bin/sh
+
+# Default flags
+CMFLAGS="-D CMAKE_BUILD_TYPE:STRING=Release"
+
+# Make for windows and linux
+cmake $CMFLAGS -D TARGETOS=Win32 . && make
+cmake $CMFLAGS                   . && make
+
+echo
+echo
+echo "---------------------------------------------------------"
+echo "Built the Linux and Windows binaries"
+
+# Copy to the correct locations
+cp scyther-linux ../gui/Scyther/Bin
+cp scyther-w32.exe ../gui/Scyther/Bin
+
+# bonus...
+cp scyther-linux ~/bin
+
+echo Copied the files to their respective locations and \~/bin
+echo "---------------------------------------------------------"
+

gui/src/subbuild-version-information.sh

@@ -0,0 +1,19 @@
+#!/bin/sh
+#
+# Arguments:
+#
+# svnversion executable path
+#
+
+SVNVERSION=`svnversion`
+TAGVERSION=`awk 'BEGIN { FS="\""; } { print $2; }' ../gui/Gui/Version.py`
+
+echo $SVNVERSION
+echo $TAGVERSION
+
+# Fix svnversion information
+echo "#define SVNVERSION \"$SVNVERSION\"" >version.h
+# Fix version tag
+echo "#define TAGVERSION \"$TAGVERSION\"" >>version.h
+
+