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

- Got rid of a lot of garbage.

Browse Source
This commit is contained in:
Cas Cremers 2007-05-19 17:02:18 +02:00
parent f837d1b000
commit 76f0db6f13
106 changed files with 0 additions and 26075 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
gui/src/BuildMacIntel-MacPPC.cmake
View File

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

11
gui/src/BuildMacIntel.cmake
View File

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

8
gui/src/BuildMacPPC-MacIntel.cmake
View File

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

11
gui/src/BuildMacPPC.cmake
View File

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

36
gui/src/BuildPlatform.cmake
View File

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

15
gui/src/BuildUnix-Win32.cmake
View File

@ -1,15 +0,0 @@
################################################################
# Name: BuildUnix-Win32.cmake
# Purpose: Build Win32 binary on Unix
# Author: Cas Cremers
################################################################
message (STATUS "Building W32 version")
# This should work on win32 platform, but also when the compiler
# is available anyway under linux
set (CMAKE_C_COMPILER "i586-mingw32msvc-gcc")
set (CMAKE_CXX_COMPILER "i586-mingw32msvc-g++")
set (CMAKE_SHARED_LIBRARY_LINK_C_FLAGS) # to get rid of -rdynamic
set (scythername "scyther-w32.exe")
add_executable (${scythername} ${Scyther_sources})

12
gui/src/BuildUnix.cmake
View File

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

37
gui/src/CMakeLists.txt
View File

@ -1,37 +0,0 @@
################################################################
# Name: CMakeLists.txt
# Purpose: Input file for CMake for the Scyther tool
# Author: Cas Cremers
################################################################
# Scyther project
project (Scyther)
# I need 2.4 for flex/etc although it does not run yet
CMAKE_MINIMUM_REQUIRED(VERSION 2.4)
# List all the source files
set (Scyther_sources
arachne.c binding.c claim.c color.c compiler.c cost.c
debug.c depend.c dotout.c error.c heuristic.c hidelevel.c
intruderknowledge.c knowledge.c label.c list.c main.c mgu.c
prune_bounds.c prune_theorems.c role.c
specialterm.c states.c switches.c symbol.c system.c tac.c
termlist.c termmap.c term.c timer.c type.c warshall.c xmlout.c
parser.c scanner.c
)
# If we are in a debug mode we want to be strict
set (CMAKE_C_FLAGS_DEBUG "${CMAKE_C_FLAGS_DEBUG} -Wall -DDEBUG")
# Usual static
set (CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -static")
# Determine version number
include (SVNVersion.cmake)
# Make scanner and parser
include (ScannerParser.cmake)
# Set build target settings according to platform
include (BuildPlatform.cmake)

33
gui/src/FindBISON.cmake
View File

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

33
gui/src/FindFLEX.cmake
View File

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

43
gui/src/GetOS.cmake
View File

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

86
gui/src/Makefile-fallback
View File

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

58
gui/src/SVNVersion.cmake
View File

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

41
gui/src/ScannerParser.cmake
View File

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

789
gui/src/Scyther.dev
View File

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

42
gui/src/UniversalBinary.cmake
View File

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

2582
gui/src/arachne.c
View File

File diff suppressed because it is too large Load Diff

20
gui/src/arachne.h
View File

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

61
gui/src/attacktemplate.tex
View File

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

617
gui/src/binding.c
View File

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

53
gui/src/binding.h
View File

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

119
gui/src/bugs.txt
View File

@ -1,119 +0,0 @@
--+++ Crititcal Bugs
* soph segfaults at no switch or -r4 (-r3 is okay??) using non-debug version.
* './scyther -a ../spdl/nsl3.spdl --increment-runs' segfaults. The main reason is that the Archne engine uses runs in a different way.
Maybe it is best to disable --increment rules for non-ModelChecker verification.
---+++ Bugs
* Problem with goal bindings: instantiation of variable with a tuple might
introduce a tuple goal, which is forbidden. We must find a way to deal with this. This typically occurs in type flaw searches.
* Arachne seems to trip over claims with empty prec sets. Maybe we
simply should not test these.
* Splice/AS does not work well because priority key search stumbles over the
public key search stuff. That is a flaw in the heuristic: we should not look
for anything that is in the intruder knowledge already. In fact, it is a
problem with branching. We should not look for PK(X), even if X is a
variable. Priority should go to keys of which the constructor is not in M_0,
maybe that heuristic works.
However, there seems to be an infinite loop for this in the algorithm, which
I did not anticipate. Investigate!
<br>
Maybe self-loops are the problem. This has to do with tuple alternation
decoding. Consider re-introducing explicit intruder strands OR self-loop
pruning.
---+++ Would like to have
---++++ ArachneEngine
* There is no good test on the correct workings of
add_goals/destruction of these. We can test this if after
termination, we have 0 goals; for this we need to store the
initially added goals as well. Furthermore, we can generate an
error when <0 goals occur.
* Consider where in Arachne dependency graph is used. If this is only for
pruning states, we can construct it there only. However, the base 'role
defs/bindings' graph might be re-used.
* Add switch for arachne to prune encryption levels when using -m2.
* To store attacks for arachne, maybe the following is needed:
* The roles for each run
* The variable bindings for all (local) variables
* The goal bindings
* Agent terms must have keylevel 0; enforce this!
* Select_goal should consider, for singular variables, whether their
type can be found in M_0. If so, the goal can be ignored.
* Fix 'never sent secrets' list, that are e.g. secret keys of regular agents
and such. The intruder can never learn these, we need this for pruning.
If a goal is such a term, we prune. Investigate how this can be incorporated.
Investigate also whether this actually makes a difference.
* Make 'generate_trace_bindings' to create the bindings for a given trace.
Note that there can be multiple solutions; for now, simply try to take the
shortest one.
---++++ ModelChecker
* For secrecy, one trusted agent and one untrusted agent suffices.
Implement this in the modelchecker.
* Implement delayed protocol compiler (on run demand only) for the modelchecker?
---++++ Misc
* Make different error codes for compilation error/ other error. This can be
useful for scripts. However, it might shift some constants for the Elegast
scripts.
* Rewrite termMguTerm such that it iterates and adapt all functions
using it. This is to allow for associative tupling later.
* Fix constants in intruder knowledge. Auto add single one of each type,
when typed expl. Add single constant when untyped. Fix this also in
semantics, and add proof to establish sufficiency.
* Fix function handling (signatures).
* Move initial intruder knowledge maybe into the title of the MSC.
* Implement run knowledge, and use this in protocol compiler.
* Introduce 'Ticket' default type in the compiler, along with some
handling for that.
* The 'choose' operator must always be typed, I think. Yes.
* The woolam-ce is incorrect because it is illegal to have a variable
term in a key that is read, by CMV semantics. I don't know what it
means for CE semantics (yet).
* Idea: run bla.bla(params) [compromised <localterm> [,<localterm>] ];
1. These local terms are given to the intruder. Technically this
should only happen _after_ they are first sent in the run. Maybe add
this to send semantics: if termOccurs(sendterm, compromisedterm) then
add compromisedterm to M, remove compromisedterm from list of terms to
compromise.
1. All claims in the run are ignored (add untrusted flag to run)
Alternative: run x.x(x) untrusted; or just compromised, to give up
all constants.
Note this is not sufficient yet, because it does not consider any
partner runs. Maybe declare a 'compromised' section first; other runs
will only activate after these have completed. Note this is much more
expensive.
* Woolam-ce gives nothing. But then again, it's a wrong impl.
* Global/protocol variables should not exist in the current system.
* run nsl.initiator(alice, all Agent) constructs?
* 'all' would generate the roles with the corresponding type.
* or maybe for clarity/complexity control: use 'runs' for constructs
with 'all' in it.
* Maybe function application ought to be a different basic term type.
* After role construction, msc consistency can be checked.
* Reduce knowledge to a simple term list? That would simplify a number
of things, and also allow for easier addition of stuff.
* How is % notation handled in Casper?
* Vernam encryption?
---++++ ConstraintLogic (and thus obsolete)
* CLP: variables in keys must be branched: maybe even in three situations
(have key and contents, have inverse key and content, nothing)
* How should claims behave (trusted/untrusted) wrt uninstantiated
agents? Branch again? That's what is causing the nsl3-var problem.
* Constraints might be a part of a knowledge thing, because with we
might now have a number of local knowledge sets, each with their own
constraint sets. That doesn't make it easier though :( and will cause
some performance loss I suppose. Each local set has to remain
solveable as well.
* Issue: how do untrusted claims work in the context of an intruder?
Claim must be checked if it can be solved such that at least one of
the agents is trusted.

16
gui/src/build.sh
View File

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

1136
gui/src/claim.c
View File

File diff suppressed because it is too large Load Diff

18
gui/src/claim.h
View File

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

39
gui/src/color.c
View File

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

12
gui/src/color.h
View File

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

18
gui/src/compile.txt
View File

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

2164
gui/src/compiler.c
View File

File diff suppressed because it is too large Load Diff

26
gui/src/compiler.h
View File

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

11
gui/src/copy2gui.sh
View File

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

74
gui/src/cost.c
View File

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

6
gui/src/cost.h
View File

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

52
gui/src/debug.c
View File

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

10
gui/src/debug.h
View File

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

569
gui/src/depend.c
View File

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

44
gui/src/depend.h
View File

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

47
gui/src/design.txt
View File

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

1814
gui/src/dotout.c
View File

File diff suppressed because it is too large Load Diff

6
gui/src/dotout.h
View File

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

94
gui/src/error.c
View File

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

19
gui/src/error.h
View File

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

4
gui/src/git-test.txt
View File

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

399
gui/src/heuristic.c
View File

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

9
gui/src/heuristic.h
View File

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

261
gui/src/hidelevel.c
View File

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

27
gui/src/hidelevel.h
View File

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

31
gui/src/hidelevel.txt
View File

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

197
gui/src/intruderknowledge.c
View File

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

9
gui/src/intruderknowledge.h
View File

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

550
gui/src/knowledge.c
View File

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

75
gui/src/knowledge.h
View File

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

86
gui/src/label.c
View File

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

26
gui/src/label.h
View File

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

46
gui/src/language.txt
View File

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

3
gui/src/license.txt
View File

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

272
gui/src/list.c
View File

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

28
gui/src/list.h
View File

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

260
gui/src/main.c
View File

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

624
gui/src/mgu.c
View File

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

30
gui/src/mgu.h
View File

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

17
gui/src/notes.txt
View File

@ -1,17 +0,0 @@
- (!!) 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.

1012
gui/src/obsolete-switches.txt
View File

File diff suppressed because it is too large Load Diff

325
gui/src/parser.y
View File

@ -1,325 +0,0 @@
%{
#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;
}

13
gui/src/pheading.h
View File

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

25
gui/src/problem.spdl
View File

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

265
gui/src/prune_bounds.c
View File

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

6
gui/src/prune_bounds.h
View File

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

484
gui/src/prune_theorems.c
View File

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

6
gui/src/prune_theorems.h
View File

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

5
gui/src/reindent.sh
View File

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

33
gui/src/releases.txt
View File

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

515
gui/src/role.c
View File

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

174
gui/src/role.h
View File

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

227
gui/src/scanner.l
View File

@ -1,227 +0,0 @@
%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:

119
gui/src/scantags.py
View File

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

97
gui/src/specialterm.c
View File

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

33
gui/src/specialterm.h
View File

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

38
gui/src/states.c
View File

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

21
gui/src/states.h
View File

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

21
gui/src/subbuild-mac-universal.sh
View File

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

24
gui/src/subbuild-unix-both.sh
View File

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

19
gui/src/subbuild-version-information.sh
View File

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

1575
gui/src/switches.c
View File

File diff suppressed because it is too large Load Diff

74
gui/src/switches.h
View File

@ -1,74 +0,0 @@
#ifndef SWITCHES
#define SWITCHES
#include "term.h"
#include "system.h"
void switchesInit ();
void switchesDone ();
//! Command-line switches structure
struct switchdata
{
// Command-line
int argc;
char **argv;
// Methods
int match; //!< Matching type.
int tupling; //!< Tupling is by default 0: right-associative, optionally 1: left-associative.
// Pruning and Bounding
int prune; //!< Type of pruning.
int maxproofdepth; //!< Maximum proof depth
int maxtracelength; //!< Maximum trace length allowed
int runs; //!< The number of runs as in the switch
char *filterProtocol; //!< Which claim should be checked?
char *filterLabel; //!< Which claim should be checked?
int maxAttacks; //!< When not 0, maximum number of attacks
int maxOfRole; //!< When not 0, maximum number of instances of each unique (non intruder) role
// Arachne
int heuristic; //!< Goal selection method for Arachne engine
int maxIntruderActions; //!< Maximum number of intruder actions in the semitrace (encrypt/decrypt)
int agentTypecheck; //!< Check type of agent variables in all matching modes
int concrete; //!< Swap out variables at the end.
int initUnique; //!< Default allows duplicate terms in rho (init)
int respUnique; //!< Default allows duplicate terms in rho (resp)
int intruder; //!< Enable intruder actions (default)
int agentUnfold; //!< Explicitly unfold for N honest agents and 1 compromised iff > 0
int abstractionMethod; //!< 0 means none, others are specific modes
int useAttackBuffer; //!< Use temporary file for attack storage
// Misc
int switchP; //!< A multi-purpose integer parameter, passed to the partial order reduction method selected.
int experimental; //!< Experimental stuff goes here until it moves into main stuff.
int removeclaims; //!< Remove any claims in the spdl file
int addreachableclaim; //!< Adds 'reachable' claims to each role
int addallclaims; //!< Adds all sorts of claims to the roles
int check; //!< Check protocol correctness
int expert; //!< Expert mode
// Output
int output; //!< From enum outputs: what should be produced. Default ATTACK.
int report;
int reportClaims; //!< Enable claims report
int xml; //!< xml output
int dot; //!< dot output
int human; //!< human readable
int reportMemory; //!< Memory display switch.
int reportTime; //!< Time display switch.
int countStates; //!< Count states
int extendNonReads; //!< Show further events in arachne xml output.
int extendTrivial; //!< Show further events in arachne xml output, based on knowledge underapproximation. (Includes at least the events of the nonreads extension)
int plain; //!< Disable color output on terminal
int monochrome; //!< Disable colors in dot output
int lightness; //!< Lightness increment 0-100
int clusters; //!> Enable clusters in output
};
extern struct switchdata switches; //!< pointer to switchdata structure
FILE *openFileSearch (char *filename, FILE * reopener);
#endif

371
gui/src/symbol.c
View File

@ -1,371 +0,0 @@
#include <stdio.h>
#include <stdlib.h>
#include <stdarg.h>
#include <string.h>
#include <limits.h>
#include "symbol.h"
#include "debug.h"
#include "error.h"
/*
Symbol processor.
Stores symbols for the lexical scanner. Can later print them.
Implementation uses a hashtable, the size of which is defined in
symbols.h.
*/
/* accessible for externals */
int globalError; //!< If >0, stdout output goes to stderr (for e.g. terms)
char *globalStream; //!< Defaults to stdout
/* external declarations */
extern int yylineno;
/* global declarations */
//! Symbol hash table.
Symbol symbtab[HASHSIZE];
//! List of available (freed) symbol blocks.
Symbol symb_list;
//! List of all allocated symbol blocks.
Symbol symb_alloc;
/* main code */
//! Open symbols code.
void
symbolsInit (void)
{
int i;
for (i = 0; i < HASHSIZE; i++)
symbtab[i] = NULL;
symb_list = NULL;
symb_alloc = NULL;
globalError = 0;
globalStream = (char *) stdout;
}
//! Close symbols code.
void
symbolsDone (void)
{
Symbol s;
while (symb_alloc != NULL)
{
s = symb_alloc;
symb_alloc = s->allocnext;
free (s);
}
}
//! Create a memory block for a symbol.
/**
* Internal memory management is used.
*@return A pointer to a memory block of size struct.
*/
Symbol
get_symb (void)
{
Symbol t;
if (symb_list != NULL)
{
t = symb_list;
symb_list = symb_list->next;
}
else
{
t = (Symbol) malloc (sizeof (struct symbol));
t->allocnext = symb_alloc;
symb_alloc = t;
}
t->keylevel = INT_MAX;
return t;
}
//! Declare a symbol to be freed.
void
free_symb (const Symbol s)
{
if (s == NULL)
return;
s->next = symb_list;
symb_list = s;
}
//! Return the index in the hash table for the string.
int
hash (const char *s)
{
int hv = 0;
int i;
for (i = 0; s[i] != EOS; i++)
{
int v = (hv >> 28) ^ (s[i] & 0xf);
hv = (hv << 4) | v;
}
hv = hv & 0x7fffffff;
return hv % HASHSIZE;
}
//! Insert a string into the hash table.
void
insert (const Symbol s)
{
int hv;
if (s == NULL)
return; /* illegal insertion of empty stuff */
hv = hash (s->text);
s->next = symbtab[hv];
symbtab[hv] = s;
}
//! Find a string in the hash table.
Symbol
lookup (const char *s)
{
int hv;
Symbol t;
if (s == NULL)
return NULL;
hv = hash (s);
t = symbtab[hv];
while (t != NULL)
{
if (strcmp (t->text, s) == 0)
break;
else
t = t->next;
}
return t;
}
//! Print a symbol.
void
symbolPrint (const Symbol s)
{
if (s == NULL)
return;
/* TODO maybe action depending on type? */
eprintf ("%s", s->text);
}
//! Print all symbols
void
symbolPrintAll (void)
{
int i, count;
eprintf ("List of all symbols\n");
count = 0;
for (i = 0; i < HASHSIZE; i++)
{
Symbol sym;
sym = symbtab[i];
if (sym != NULL)
{
eprintf ("H%i:\t", i);
while (sym != NULL)
{
count++;
eprintf ("[%s]\t", sym->text);
sym = sym->next;
}
eprintf ("\n");
}
}
eprintf ("Total:\t%i\n", count);
}
//! Insert a string into the symbol table, if it wasn't there yet.
/**
* Also sets line numbers and type.
*\sa T_SYSCONST
*/
Symbol
symbolSysConst (const char *str)
{
Symbol symb;
symb = lookup (str);
if (symb == NULL)
{
symb = get_symb ();
symb->lineno = yylineno;
symb->type = T_SYSCONST;
symb->text = str;
insert (symb);
}
return symb;
}
//! Generate the first fresh free number symbol, prefixed by a certain symbol's string.
/**
* Note that there is an upper limit to this, to avoid some problems with buffer overflows etc.
*/
Symbol
symbolNextFree (Symbol prefixsymbol)
{
char *prefixstr;
int n;
int len;
if (prefixsymbol != NULL)
{
prefixstr = (char *) prefixsymbol->text;
len = strlen (prefixstr);
}
else
{
prefixstr = "";
len = 0;
}
n = 1;
while (n <= 9999)
{
/*
* The construction below (variable buffer length) is not allowed in ISO C90
*/
char buffer[len + 5]; // thus we must enforce a maximum of 9.999 (allowing for storage of \0 )
Symbol symb;
int slen;
slen = sprintf (buffer, "%s%i", prefixstr, n);
buffer[slen] = EOS;
symb = lookup (buffer);
if (symb == NULL)
{
char *newstring;
// Copy the buffer to something that will survive
/**
* Memory leak: although this routine should not be called recursively, it will never de-allocate this memory.
* Thus, some precaution is necessary.
* [x][CC]
*/
newstring = (char *) malloc (slen + 1);
memcpy (newstring, buffer, slen + 1);
/* This persistent string can be used to return a fresh symbol */
return symbolSysConst (newstring);
}
// Try next one
n++;
}
error ("We ran out of numbers (%i) when trying to generate a fresh symbol.",
n);
return NULL;
}
//! Fix all the unset keylevels
void
symbol_fix_keylevels (void)
{
int i;
for (i = 0; i < HASHSIZE; i++)
{
Symbol sym;
sym = symbtab[i];
while (sym != NULL)
{
#ifdef DEBUG
if (DEBUGL (5))
{
eprintf ("Symbol ");
symbolPrint (sym);
}
#endif
if (sym->keylevel == INT_MAX)
{
// Nothing currently, this simply does not originate on a strand.
#ifdef DEBUG
if (DEBUGL (5))
{
eprintf (" doesn't have a keylevel yet.\n");
}
#endif
}
#ifdef DEBUG
else
{
if (DEBUGL (5))
{
eprintf (" has keylevel %i\n", sym->keylevel);
}
}
#endif
sym = sym->next;
}
}
}
//! Get output stream pointer
FILE *
getOutputStream (void)
{
if (globalError == 0)
return (FILE *) globalStream;
else
#ifdef USESTDERR
return stderr;
#else
// we simply omit it
return NULL;
#endif
}
//! Print out according to globalError
/**
* Input is comparable to printf, only depends on globalError. This should be
* used by any function trying to do output.
*
* Furthermore, if globalError == 0, it can still be overriden by
* globalStream, which can be another stream pointer. If it is null, stdout
* is assumed.
*
*\sa globalError
*/
void
eprintf (char *fmt, ...)
{
va_list args;
FILE *stream;
va_start (args, fmt);
stream = getOutputStream ();
if (stream != NULL)
{
vfprintf (stream, fmt, args);
}
va_end (args);
}
// Variable list variant
void
veprintf (const char *fmt, va_list args)
{
FILE *stream;
stream = getOutputStream ();
if (stream != NULL)
{
vfprintf (stream, fmt, args);
}
}

58
gui/src/symbol.h
View File

@ -1,58 +0,0 @@
#ifndef SYMBOLS
#define SYMBOLS
#include <stdarg.h>
//! Size of symbol hashtable.
/** Optimistically large. Should be a prime, says theory.
*/
#define HASHSIZE 997
enum symboltypes
{ T_UNDEF = -1, T_PROTOCOL, T_CONST, T_VAR, T_SYSCONST };
#define EOS 0
//! Symbol structure
struct symbol
{
//! Type of symbol.
/**
*\sa T_UNDEF, T_PROTOCOL, T_CONST, T_VAR, T_SYSCONST
*/
int type;
//! Line number at which it occurred.
int lineno;
//! Level of occurrence in role nodes. 0 for as non-key, 1 for key only, 2 for key of key only, etc..
int keylevel;
//! Ascii string with name of the symbol.
const char *text;
//! Possible next pointer.
struct symbol *next;
//! Used for linking all symbol blocks, freed or in use.
struct symbol *allocnext;
};
typedef struct symbol *Symbol; //!< pointer to symbol structure
void symbolsInit (void);
void symbolsDone (void);
Symbol get_symb (void);
void free_symb (const Symbol s);
void insert (const Symbol s);
Symbol lookup (const char *s);
void symbolPrint (const Symbol s);
void symbolPrintAll (void);
Symbol symbolSysConst (const char *str);
void symbol_fix_keylevels (void);
Symbol symbolNextFree (Symbol prefixsymbol);
void eprintf (char *fmt, ...);
void veprintf (const char *fmt, va_list args);
extern int globalError;
extern char *globalStream;
#endif

1454
gui/src/system.c
View File

File diff suppressed because it is too large Load Diff

208
gui/src/system.h
View File

@ -1,208 +0,0 @@
#ifndef SYSTEM
#define SYSTEM
#include "term.h"
#include "termmap.h"
#include "termlist.h"
#include "knowledge.h"
#include "states.h"
#include "role.h"
#include "list.h"
#define runPointerGet(sys,run) sys->runs[run].index
#define runPointerSet(sys,run,newp) sys->runs[run].index = newp
enum outputs
{ EMPTY, ATTACK, STATESPACE, SUMMARY, PROOF };
//! Protocol definition.
struct protocol
{
//! Name of the protocol encoded in a term.
Term nameterm;
//! List of role definitions.
Role roles;
//! List of role names.
Termlist rolenames;
//! List of local terms for this protocol.
Termlist locals;
//! Pointer to next protocol.
struct protocol *next;
int lineno; //!< Line number of definition (for errors)?
};
//! Shorthand for protocol pointer.
typedef struct protocol *Protocol;
//! Run container.
struct run
{
Protocol protocol; //!< Protocol of this run.
Role role; //!< Role of this run.
int step; //!< Current execution point in the run (integer)
int rolelength; //!< Length of role
Roledef index; //!< Current execution point in the run (roledef pointer)
Roledef start; //!< Head of the run definition.
Knowledge know; //!< Current knowledge of the run.
Termlist rho; //!< As in semantics (copies in artefacts)
Termlist sigma; //!< As in semantics (copies in artefacts)
Termlist constants; //!< As in semantics (copies in artefacts)
Termlist locals; //!< Locals of the run (will be deprecated eventually)
Termlist artefacts; //!< Stuff created especially for this run, which can also include tuples (anything allocated)
Termlist substitutions; //!< The substitutions as they came from the roledef unifier
int prevSymmRun; //!< Used for symmetry reduction. Either -1, or the previous run with the same role def and at least a single parameter.
int firstNonAgentRead; //!< Used for symmetry reductions for equal agents runs; -1 if there is no candidate.
int firstReal; //!< 1 if a choose was inserted, otherwise 0
};
//! Shorthand for run pointer.
typedef struct run *Run;
//! Structure for information on special terms (cacheing)
struct hiddenterm
{
Term term;
unsigned int hideminimum;
unsigned int hideprotocol;
unsigned int hideknowledge;
struct hiddenterm *next;
};
//! Pointer shorthand
typedef struct hiddenterm *Hiddenterm;
//! The main state structure.
struct system
{
int step; //!< Step in trace during exploration. Can be managed globally
Knowledge know; //!< Knowledge in currect step of system.
struct parameters *parameters; // misc
/* static run info, maxruns */
Run runs;
/* global */
int maxruns; //!< Number of runs in the system.
/* properties */
Termlist secrets; //!< Integrate secrets list into system.
Termlist synchronising_labels; //!< List of labels that might synchronise.
int shortestattack; //!< Length of shortest attack trace.
int maxtracelength; //!< helps to remember the length of the last trace.
/* traversal */
int traverse; //!< Traversal method.
int explore; //!< Boolean: explore states after actions or not.
/* counters */
states_t states; //!< States traversed
states_t interval; //!< Used to update state printing at certain intervals
states_t claims; //!< Number of claims encountered.
states_t failed; //!< Number of claims failed.
int attackid; //!< Global counter of attacks (used for assigning identifiers) within this Scyther call.
int num_regular_runs; //!< Number of regular runs
int num_intruder_runs; //!< Number of intruder runs
/* protocol definition */
Protocol protocols; //!< List of protocols in the system
Termlist locals; //!< List of local terms
Termlist variables; //!< List of all variables
Termlist agentnames; //!< List of all agent names (trusted and untrusted)
Termlist untrusted; //!< List of untrusted agent names
Termlist globalconstants; //!< List of global constants
Hiddenterm hidden; //!< List of hiddenterm constructs for Hidelevel lemma
/* protocol preprocessing */
int rolecount; //!< Number of roles in the system
int roleeventmax; //!< Maximum number of events in a single role
int lastChooseRun; //!< Last run with a choose event
Claimlist claimlist; //!< List of claims in the system, with occurrence counts
List labellist; //!< List of labelinfo stuff
int knowledgedefined; //!< True if knowledge is defined for some role (which triggers well-formedness check etc.)
/* constructed trace pointers, static */
Roledef *traceEvent; //!< Trace roledefs: MaxRuns * maxRoledef
int *traceRun; //!< Trace run ids: MaxRuns * maxRoledef
Knowledge *traceKnow; //!< Trace intruder knowledge: Maxruns * maxRoledef
states_t *traceNode; //!< Trace node traversal: Maxruns * maxRoledef
/* Arachne assistance */
List bindings; //!< List of bindings
Claimlist current_claim; //!< The claim under current investigation
Termlist trustedRoles; //!< Roles that should be trusted for this claim (the default, NULL, means all)
};
typedef struct system *System;
System systemInit ();
void systemReset (const System sys);
void systemRuns (const System sys);
System systemDuplicate (const System fromsys);
void statesPrint (const System sys);
void statesPrintShort (const System sys);
void systemDestroy (const System sys);
void systemDone (const System sys);
void ensureValidRun (const System sys, int run);
void runPrint (Roledef rd);
void runsPrint (const System sys);
Term agentOfRunRole (const System sys, const int run, const Term role);
Term agentOfRun (const System sys, const int run);
void roleInstance (const System sys, const Protocol protocol, const Role role,
const Termlist paramlist, Termlist substlist);
void roleInstanceDestroy (const System sys);
void systemStart (const System sys);
void indentActivate ();
void indentSet (int i);
void indent ();
Protocol protocolCreate (Term nameterm);
void locVarPrint (Termlist tl);
void protocolPrint (Protocol p);
void protocolsPrint (Protocol p);
int untrustedAgent (const System sys, Termlist agents);
int getMaxTraceLength (const System sys);
void agentsOfRunPrint (const System sys, const int run);
void violatedClaimPrint (const System sys, int i);
void commandlinePrint (FILE * stream);
int compute_rolecount (const System sys);
int compute_roleeventmax (const System sys);
void scenarioPrint (const System sys);
int isAgentTrusted (const System sys, Term agent);
int isAgentlistTrusted (const System sys, Termlist agents);
int isRunTrusted (const System sys, const int run);
int iterateRuns (const System sys, int (*callback) (int r));
int iterateRegularRuns (const System sys, int (*callback) (int r));
int iterateEvents (const System sys, const int run,
int (*callback) (Roledef rd, int ev));
int iterateAllEvents (const System sys,
int (*callback) (int run, Roledef rd, int ev));
int iterateEventsType (const System sys, const int run, const int evtype,
int (*callback) (Roledef rd, int ev));
int iterateLocalToOther (const System sys, const int myrun,
int (*callback) (Term t));
int iterateRoles (const System sys, int (*callback) (Protocol p, Role r));
int firstOccurrence (const System sys, const int r, Term t, int evtype);
Roledef eventRoledef (const System sys, const int run, const int ev);
int countInitiators (const System sys);
int selfResponder (const System sys, const int run);
int selfResponders (const System sys);
int selfInitiator (const System sys, const int run);
int selfInitiators (const System sys);
int enoughAttacks (const System sys);
//! Equality for run structure naming
/**
* For the modelchecker, there was an index called step. In Strand Space
* terminology, something like that is the height of the strand.
*/
#define height step
#endif

337
gui/src/tac.c
View File

@ -1,337 +0,0 @@
#include <stdio.h>
#include <stdlib.h>
#include "tac.h"
#include "memory.h"
#include "switches.h"
#include "error.h"
extern int yylineno;
static Tac allocatedTacs;
//! Init segment
void
tacInit (void)
{
allocatedTacs = NULL;
}
//! Closing segment
void
tacDone (void)
{
Tac ts;
ts = allocatedTacs;
while (ts != NULL)
{
Tac tf;
tf = ts;
ts = ts->allnext;
free (tf);
}
}
//! Create a tac node of some type
Tac
tacCreate (int op)
{
/* maybe even store in scrapping list, so we could delete them
* all later */
Tac t = malloc (sizeof (struct tacnode));
t->allnext = allocatedTacs;
allocatedTacs = t;
t->lineno = yylineno;
t->op = op;
t->next = NULL;
t->prev = NULL;
t->t1.tac = NULL;
t->t2.tac = NULL;
t->t3.tac = NULL;
return t;
}
Tac
tacString (char *s)
{
Tac t;
t = tacCreate (TAC_STRING);
t->t1.str = s;
return t;
}
Tac
tacJoin (int op, Tac t1, Tac t2, Tac t3)
{
Tac t;
t = tacCreate (op);
t->t1.tac = t1;
t->t2.tac = t2;
t->t3.tac = t3;
return t;
}
Tac
tacCat (Tac t1, Tac t2)
{
Tac t1e;
if (t1 == NULL)
{
if (t2 == NULL)
return NULL;
else
return t2;
}
else
{
t1e = t1;
while (t1e->next != NULL)
t1e = t1e->next;
t1e->next = t2;
if (t2 != NULL)
{
t2->prev = t1e;
}
return t1;
}
}
//! List to right-associative tuple
Tac
tacTupleRa (Tac taclist)
{
Tac tc;
/* check for single node */
if (taclist->next == NULL)
{
/* just return */
tc = taclist;
}
else
{
/* otherwise, write as (x,(y,(z,..))) */
tc = tacCreate (TAC_TUPLE);
tc->t1.tac = taclist;
tc->t2.tac = tacTuple (taclist->next);
/* unlink list */
tc->t1.tac->next = NULL;
tc->t2.tac->prev = NULL;
}
return tc;
}
//! List to left-associative tuple
Tac
tacTupleLa (Tac taclist)
{
Tac tc;
/* initial node is simple the first item */
tc = taclist;
tc->prev = NULL;
/* add any other nodes (one is ensured) */
do
{
Tac tcnew;
taclist = taclist->next;
/* add a new node (taclist) to the existing thing by first making the old one into the left-hand side of a tuple */
tcnew = tacCreate (TAC_TUPLE);
tcnew->t1.tac = tc;
tcnew->t2.tac = taclist;
tc = tcnew;
/* unlink */
tc->t1.tac->next = NULL;
tc->t2.tac->prev = NULL;
}
while (taclist->next != NULL);
return tc;
}
//! Compile a list into a tuple
/* in: a list. out: a tuple (for e.g. associativity)
* Effectively, this defines how we interpret tuples with
* more than two components.
*/
Tac
tacTuple (Tac taclist)
{
if (taclist == NULL || taclist->next == NULL)
{
/* just return */
return taclist;
}
else
{
switch (switches.tupling)
{
case 0:
/* case 0: as well as */
/* DEFAULT behaviour */
/* right-associative */
return tacTupleRa (taclist);
case 1:
/* switch --la-tupling */
/* left-associative */
return tacTupleLa (taclist);
default:
error ("Unknown tupling mode (--tupling=%i)", switches.tupling);
}
}
// @TODO this should be considered an error
return NULL;
}
/*
* tacPrint
* Print the tac. Only for debugging purposes.
*/
void
tacPrint (Tac t)
{
if (t == NULL)
return;
switch (t->op)
{
case TAC_PROTOCOL:
printf ("protocol %s (", t->t1.sym->text);
tacPrint (t->t3.tac);
printf (")\n{\n");
tacPrint (t->t2.tac);
printf ("};\n");
break;
case TAC_ROLE:
printf ("role %s\n{\n", t->t1.sym->text);
tacPrint (t->t2.tac);
printf ("};\n");
break;
case TAC_READ:
printf ("read");
if (t->t1.sym != NULL)
{
printf ("_%s", t->t1.sym->text);
}
printf ("(");
tacPrint (t->t2.tac);
printf (");\n");
break;
case TAC_SEND:
printf ("send");
if (t->t1.sym != NULL)
{
printf ("_%s", t->t1.sym->text);
}
printf ("(");
tacPrint (t->t2.tac);
printf (");\n");
break;
case TAC_CLAIM:
printf ("claim");
if (t->t1.sym != NULL)
{
printf ("_%s", t->t1.sym->text);
}
printf ("(");
tacPrint (t->t2.tac);
printf (");\n");
break;
case TAC_CONST:
printf ("const ");
tacPrint (t->t1.tac);
if (t->t2.tac != NULL)
{
printf (" : ");
tacPrint (t->t2.tac);
}
printf (";\n");
break;
case TAC_VAR:
printf ("var ");
tacPrint (t->t1.tac);
if (t->t2.tac != NULL)
{
printf (" : ");
tacPrint (t->t2.tac);
}
printf (";\n");
break;
case TAC_UNDEF:
printf ("undefined");
if (t->next != NULL)
printf (",");
break;
case TAC_STRING:
printf ("%s", t->t1.sym->text);
if (t->next != NULL)
printf (",");
break;
case TAC_TUPLE:
printf ("(");
tacPrint (t->t1.tac);
printf (",");
tacPrint (t->t2.tac);
printf (")");
break;
case TAC_ENCRYPT:
printf ("{");
tacPrint (t->t1.tac);
printf ("}");
tacPrint (t->t2.tac);
if (t->next != NULL)
{
printf (",");
t = t->next;
tacPrint (t);
}
break;
case TAC_RUN:
printf ("run ");
tacPrint (t->t1.tac);
printf ("(");
tacPrint (t->t2.tac);
printf (");\n");
break;
case TAC_ROLEREF:
symbolPrint (t->t1.sym);
printf (".");
symbolPrint (t->t2.sym);
break;
case TAC_COMPROMISED:
printf ("compromised ");
tacPrint (t->t1.tac);
printf (";\n");
break;
case TAC_SECRET:
printf ("secret ");
tacPrint (t->t1.tac);
printf (";\n");
break;
case TAC_INVERSEKEYS:
printf ("inversekeys (");
tacPrint (t->t1.tac);
printf (",");
tacPrint (t->t2.tac);
printf (");\n");
break;
case TAC_UNTRUSTED:
printf ("untrusted ");
tacPrint (t->t1.tac);
printf (";\n");
break;
default:
printf ("[??]");
}
/* and any other stuff */
if (t->next != NULL)
{
tacPrint (t->next);
}
}

77
gui/src/tac.h
View File

@ -1,77 +0,0 @@
#ifndef TAC_H
#define TAC_H
#include "symbol.h"
/*
* TAC instructions
*/
enum tactypes
{
TAC_UNDEF,
TAC_SYM,
TAC_TUPLE,
TAC_ENCRYPT,
TAC_VAR,
TAC_CONST,
TAC_READ,
TAC_SEND,
TAC_CLAIM,
TAC_FUNC,
TAC_STRING,
TAC_ROLE,
TAC_PROTOCOL,
TAC_KNOWS,
TAC_RUN,
TAC_ROLEREF,
TAC_SECRET,
TAC_INVERSEKEYS,
TAC_UNTRUSTED,
TAC_COMPROMISED,
TAC_USERTYPE
};
//! Structure to hold the compilation tree nodes
struct tacnode
{
struct tacnode *next; //!< pointer to previous node
struct tacnode *prev; //!< pointer to next node
struct tacnode *allnext;
int op; //!< operator for this node
int lineno; //!< line number of parser location in the input file
union
{
Symbol sym;
struct tacnode *tac;
char *str;
int value;
} t1;
union
{
Symbol sym;
struct tacnode *tac;
char *str;
int value;
} t2;
union
{
Symbol sym;
struct tacnode *tac;
char *str;
int value;
} t3;
};
typedef struct tacnode *Tac;
void tacInit (void);
void tacDone (void);
Tac tacCreate (int op);
Tac tacSymb (char *s);
Tac tacJoin (int op, Tac t1, Tac t2, Tac t3);
Tac tacTuple (Tac taclist);
Tac tacCat (Tac t1, Tac t2);
void tacPrint (Tac t);
#endif

1483
gui/src/term.c
View File

File diff suppressed because it is too large Load Diff

196
gui/src/term.h
View File

@ -1,196 +0,0 @@
#ifndef TERMS
#define TERMS
#include "symbol.h"
#define false 0
#define true 1
// type <= LEAF means it's a leaf, nkay?
enum termtypes
{ GLOBAL, VARIABLE, LEAF, ENCRYPT, TUPLE };
//! The most basic datatype in the modelchecker.
/**
* Describes a single term.
*/
struct term
{
/* basic : name,runid
encrypt: op,key
tuple : op,next
*/
//! The type of term.
/**
* \sa GLOBAL, VARIABLE, LEAF, ENCRYPT, TUPLE
*/
int type;
//! Data Type termlist (e.g. agent or nonce)
/** Only for leaves. */
void *stype; // list of types
int roleVar; //!< only for leaf, arachne engine: role variable flag
//! Substitution term.
/**
* If this is non-NULL, this leaf term is apparently substituted by
* this term.
*/
struct term *subst; // only for variable/leaf, substitution term
union
{
//! Pointer to the symbol for leaves
Symbol symb;
//! Encrypted subterm.
struct term *op;
//! Left-hand side of tuple pair.
struct term *op1;
struct term *next; //!< for alternative memory management
} left;
union
{
//! run identifier for leaves
int runid;
//! Key used to encrypt subterm.
struct term *key;
//! Right-hand side of tuple pair.
struct term *op2;
} right;
};
//! Component macros (left)
#define TermSymb(t) (t->left.symb)
#define TermOp1(t) (t->left.op1)
#define TermOp(t) (t->left.op)
//! Component macros (right)
#define TermRunid(t) (t->right.runid)
#define TermOp2(t) (t->right.op2)
#define TermKey(t) (t->right.key)
//! Flag for term status
extern int rolelocal_variable;
//! Pointer shorthand.
typedef struct term *Term;
void termsInit (void);
void termsDone (void);
Term makeTermEncrypt (Term t1, Term t2);
Term makeTermTuple (Term t1, Term t2);
Term makeTermType (const int type, const Symbol symb, const int runid);
__inline__ Term deVarScan (Term t);
#define realTermLeaf(t) (t != NULL && t->type <= LEAF)
#define realTermTuple(t) (t != NULL && t->type == TUPLE)
#define realTermEncrypt(t) (t != NULL && t->type == ENCRYPT)
#define realTermVariable(t) (t != NULL && (t->type == VARIABLE || (t->type <= LEAF && rolelocal_variable && TermRunid(t) == -3)))
#define substVar(t) ((realTermVariable (t) && t->subst != NULL) ? 1 : 0)
#define deVar(t) ( substVar(t) ? deVarScan(t->subst) : t)
#define isTermLeaf(t) realTermLeaf(deVar(t))
#define isTermTuple(t) realTermTuple(deVar(t))
#define isTermEncrypt(t) realTermEncrypt(deVar(t))
#define isTermVariable(t) realTermVariable(deVar(t))
#ifdef DEBUG
#define isTermEqual(t1,t2) isTermEqualDebug(t1,t2)
int isTermEqualDebug (Term t1, Term t2);
#else
#define isTermEqual1(t1,t2) ((substVar(t1) || substVar(t2)) \
? isTermEqualFn(t1,t2) \
: ( \
(t1 == t2) \
? 1 \
: ( \
(t1 == NULL || t2 == NULL || t1->type != t2->type) \
? 0 \
: ( \
realTermLeaf(t1) \
? isTermEqualFn(t1,t2) \
: ( \
realTermEncrypt(t2) \
? (isTermEqualFn(TermKey(t1), TermKey(t2)) && \
isTermEqualFn(TermOp(t1), TermOp(t2))) \
: (isTermEqualFn(TermOp1(t1), TermOp1(t2)) && \
isTermEqualFn(TermOp2(t1), TermOp2(t2))) \
) \
) \
) \
) \
)
#define isTermEqual2(t1,t2) ((substVar(t1) || substVar(t2)) \
? isTermEqualFn(t1,t2) \
: ( \
(t1 == t2) \
? 1 \
: ( \
(t1 == NULL || t2 == NULL || t1->type != t2->type) \
? 0 \
: ( \
realTermLeaf(t1) \
? isTermEqualFn(t1,t2) \
: ( \
realTermEncrypt(t2) \
? (isTermEqual1(TermKey(t1), TermKey(t2)) && \
isTermEqual1(TermOp(t1), TermOp(t2))) \
: (isTermEqual1(TermOp1(t1), TermOp1(t2)) && \
isTermEqual1(TermOp2(t1), TermOp2(t2))) \
) \
) \
) \
) \
)
#define isTermEqual(t1,t2) isTermEqual2(t1,t2)
#endif
int hasTermVariable (Term term);
int isTermEqualFn (Term term1, Term term2);
int termSubTerm (Term t, Term tsub);
int termInTerm (Term t, Term tsub);
void termPrintCustom (Term term, char *leftvar, char *rightvar, char *lefttup,
char *righttup, char *leftenc, char *rightenc,
void (*callback) (const Term t));
void termPrint (Term term);
void termTuplePrintCustom (Term term, char *leftvar, char *rightvar,
char *lefttup, char *righttup, char *leftenc,
char *rightenc, void (*callback) (const Term t));
void termTuplePrint (Term term);
Term termDuplicate (const Term term);
Term termNodeDuplicate (const Term term);
Term termDuplicateDeep (const Term term);
Term termDuplicateUV (Term term);
void termDelete (const Term term);
void termNormalize (Term term);
Term termRunid (Term term, int runid);
int tupleCount (Term tt);
Term tupleProject (Term tt, int n);
int termSize (Term t);
float termDistance (Term t1, Term t2);
int termOrder (Term t1, Term t2);
int term_iterate (const Term term, int (*leaf) (Term t),
int (*nodel) (Term t), int (*nodem) (Term t),
int (*noder) (Term t));
int term_iterate_deVar (Term term, int (*leaf) (Term t),
int (*nodel) (Term t), int (*nodem) (Term t),
int (*noder) (Term t));
int term_iterate_leaves (const Term t, int (*func) (Term t));
int term_iterate_open_leaves (const Term term, int (*func) (Term t));
void term_rolelocals_are_variables ();
int term_encryption_level (const Term term);
float term_constrain_level (const Term term);
void term_set_keylevels (const Term term);
void termPrintDiff (Term t1, Term t2);
int isLeafNameEqual (Term t1, Term t2);
Term freshTermPrefix (Term prefixterm);
int isTermFunctionName (Term t);
Term getTermFunction (Term t);
unsigned int termHidelevel (const Term tsmall, Term tbig);
void termSubstPrint (Term t);
int iterateTermOther (const int myrun, Term t, int (*callback) (Term t));
extern char *RUNSEP; // by default, set to "#"
#endif

972
gui/src/termlist.c
View File

@ -1,972 +0,0 @@
#include <stdlib.h>
#include <stdio.h>
#include "termlist.h"
#include "specialterm.h"
#include "debug.h"
#include "error.h"
/*
* Shared stuff
*/
//! Termlist error thing (for global use)
Termlist TERMLISTERROR;
/*
* Forward declarations
*/
Termlist makeTermlist ();
//! Open termlists code.
void
termlistsInit (void)
{
TERMLISTERROR = makeTermlist ();
TERMLISTERROR->term = NULL;
TERMLISTERROR->prev = NULL;
TERMLISTERROR->next = NULL;
return;
}
//! Close termlists code.
void
termlistsDone (void)
{
termlistDelete (TERMLISTERROR);
return;
}
//! Allocate memory for a termlist node.
/**
*@return A pointer to uninitialised memory of the size of a termlist node.
*/
Termlist
makeTermlist ()
{
/* inline candidate */
return (Termlist) malloc (sizeof (struct termlist));
}
//! Duplicate a termlist.
/**
* Uses termDuplicate to copy the elements, and allocated new memory for the list nodes.
*\sa termDuplicate(), termlistShallow()
*/
Termlist
termlistDuplicate (Termlist tl)
{
Termlist newtl;
if (tl == NULL)
return NULL;
newtl = makeTermlist ();
newtl->term = termDuplicate (tl->term);
newtl->prev = NULL;
newtl->next = termlistDuplicate (tl->next);
if (newtl->next != NULL)
(newtl->next)->prev = newtl;
return newtl;
}
//! Shallow reverse copy of a termlist.
/**
* Just copies the element pointers. Allocates new memory for the list nodes.
* Note that it reverses the order of the list.
*\sa termlistDuplicate()
*/
Termlist
termlistShallow (Termlist tl)
{
Termlist newtl;
newtl = NULL;
while (tl != NULL)
{
newtl = termlistAdd (newtl, tl->term);
tl = tl->next;
}
return newtl;
}
//! Shallow deletion of a termlist.
/**
* Deletes the termlist nodes only. Elements are intact after exit.
*\sa termlistShallow()
*/
void
termlistDelete (Termlist tl)
{
if (tl == NULL)
return;
#ifdef DEBUG
if (tl == TERMLISTERROR)
{
static int count = 0;
count++;
if (count > 1)
{
// TERMLISTERROR should only be destroyed once (by the done function)
error ("Trying to delete TERMLISTERROR a second time, whazzup?");
}
}
#endif
termlistDelete (tl->next);
free (tl);
}
//! Deep deletion of a termlist.
/**
* Deletes the termlist nodes as well as the elements.
*\sa termlistDuplicate(), termDuplicate(), termDelete()
*/
void
termlistDestroy (Termlist tl)
{
if (tl == NULL)
return;
termlistDestroy (tl->next);
termDelete (tl->term);
free (tl);
}
//! Determine whether a term is an element of a termlist.
/**
* The NULL term is not an element of any list. (Not even of the NULL list)
*
*@return True iff the term is an element of the termlist.
*/
__inline__ int
inTermlist (Termlist tl, const Term term)
{
if (term == NULL)
{
return 0;
}
while (tl != NULL)
{
if (isTermEqual (tl->term, term))
{
return 1;
}
tl = tl->next;
}
return 0;
}
//! Determine whether a term is an element of a termlist: yield pointer
__inline__ Termlist
termlistFind (Termlist tl, const Term term)
{
#ifdef DEBUG
if (term == NULL)
{
error ("Trying to do inTermlist for a NULL term.");
}
#endif
while (tl != NULL)
{
if (isTermEqual (tl->term, term))
{
return tl;
}
tl = tl->next;
}
return NULL;
}
//! Equality of two term lists.
/**
* Are all elements of list 1 in list 2, and vice versa?
* Note that we assume unique elements!
*@return True iff every element of the list is in the other list.
*/
int
isTermlistEqual (Termlist tl1, Termlist tl2)
{
if (termlistLength (tl1) != termlistLength (tl2))
return 0;
while (tl2 != NULL)
{
if (!inTermlist (tl1, tl2->term))
return 0;
tl2 = tl2->next;
}
return 1;
}
//! Adds a term to the front of a termlist.
/**
* Duplicates are allowed.
*@return A new list pointer.
*\sa termlistAppend()
*/
Termlist
termlistAdd (Termlist tl, Term term)
{
Termlist newtl;
newtl = makeTermlist ();
newtl->term = term;
newtl->next = tl;
if (tl == NULL)
{
newtl->prev = NULL;
}
else
{
newtl->prev = tl->prev;
if (newtl->prev != NULL)
(newtl->prev)->next = newtl;
tl->prev = newtl;
}
return newtl;
}
//! Adds a term to the end of a termlist.
/**
* Duplicates are allowed.
*@return A new list pointer if the termlist was NULL.
*\sa termlistAdd()
*/
Termlist
termlistAppend (const Termlist tl, const Term term)
{
Termlist newtl;
Termlist scantl;
newtl = makeTermlist ();
newtl->term = term;
newtl->next = NULL;
if (tl == NULL)
{
newtl->prev = NULL;
return newtl;
}
else
{
scantl = tl;
while (scantl->next != NULL)
scantl = scantl->next;
scantl->next = newtl;
newtl->prev = scantl;
}
return tl;
}
//! Add a term only to a list if it wasn't in it before.
/**
* Mimics a basic set type behaviour.
*/
Termlist
termlistAddNew (const Termlist tl, const Term t)
{
if (t == NULL || inTermlist (tl, t))
return tl;
else
return termlistAdd (tl, t);
}
//! Concatenates two termlists.
/**
* The last pointer of the first list is made to point to the second list.
*@return The pointer to the concatenated list.
*/
Termlist
termlistConcat (Termlist tl1, Termlist tl2)
{
Termlist scan;
if (tl1 == NULL)
return tl2;
if (tl2 == NULL)
return tl1;
scan = tl1;
while (scan->next != NULL)
scan = scan->next;
scan->next = tl2;
return tl1;
}
//! Concatenates two termlists.
/**
* Creates a completely new list that can be deleted.
*
* Note that the order is not preserved currently.
*/
Termlist
termlistConcatStatic (Termlist tl1, Termlist tl2)
{
Termlist tl, tls;
tl = NULL;
for (tls = tl1; tls != NULL; tls = tls->next)
{
tl = termlistAdd (tl, tls->term);
}
for (tls = tl2; tls != NULL; tls = tls->next)
{
tl = termlistAdd (tl, tls->term);
}
return tl;
}
//! Remove the pointed at element from the termlist.
/**
* Easier because of the double linked list. Note: does not do termDelete on the term.
*
*@param tl The pointer to the termlist node to be deleted from the list.
*@return The possibly new head pointer to the termlist.
*/
Termlist
termlistDelTerm (Termlist tl)
{
Termlist newhead;
if (tl == NULL)
return NULL;
if (tl->prev != NULL)
{
(tl->prev)->next = tl->next;
newhead = tl->prev;
while (newhead->prev != NULL)
newhead = newhead->prev;
}
else
{
newhead = tl->next;
}
if (tl->next != NULL)
(tl->next)->prev = tl->prev;
free (tl);
return newhead;
}
//! Construct the conjunction of two termlists.
/**
*@return A new termlist containing the elements in both lists.
*/
Termlist
termlistConjunct (Termlist tl1, Termlist tl2)
{
Termlist newtl;
Termlist scan;
scan = tl1;
newtl = NULL;
while (scan != NULL)
{
if (inTermlist (tl2, scan->term))
newtl = termlistAdd (newtl, scan->term);
scan = scan->next;
}
return newtl;
}
//! Construct the conjunction of two termlists, and a certain type.
/**
*@return A new termlist containing the elements in both lists, that are also of the desired type.
*/
Termlist
termlistConjunctType (Termlist tl1, Termlist tl2, int termtype)
{
Termlist newtl;
Termlist scan;
scan = tl1;
newtl = NULL;
while (scan != NULL)
{
if (((scan->term)->type == termtype) && (inTermlist (tl2, scan->term)))
newtl = termlistAdd (newtl, scan->term);
scan = scan->next;
}
return newtl;
}
//! Construct the conjunction of a termlist and a certain type.
/**
*@return A new termlist containing the elements in the list that are of the desired type.
*/
Termlist
termlistType (Termlist tl, int termtype)
{
Termlist newtl;
Termlist scan;
scan = tl;
newtl = NULL;
while (scan != NULL)
{
if ((scan->term)->type == termtype)
newtl = termlistAdd (newtl, scan->term);
scan = scan->next;
}
return newtl;
}
//! Display a termlist.
/**
* Lists of terms are displayed between square brackets, and seperated by commas.
*/
void
termlistPrint (Termlist tl)
{
if (tl == NULL)
{
eprintf ("[Empty]");
return;
}
eprintf ("[");
while (tl != NULL)
{
termPrint (tl->term);
tl = tl->next;
if (tl != NULL)
eprintf (", ");
}
eprintf ("]");
}
//! Append all open variables in a term to a list.
/**
*@param tl The list to which to append to.
*@param t The term possibly containing open variables.
*@return The pointer to the extended list.
*\sa termlistAddRealVariables()
*/
Termlist
termlistAddVariables (Termlist tl, Term t)
{
if (t == NULL)
return tl;
t = deVar (t);
if (isTermLeaf (t))
{
if (isTermVariable (t) && !inTermlist (tl, t))
return termlistAdd (tl, t);
else
return tl;
}
else
{
if (isTermEncrypt (t))
return termlistAddVariables (termlistAddVariables (tl, TermOp (t)),
TermKey (t));
else
return
termlistAddVariables (termlistAddVariables (tl, TermOp1 (t)),
TermOp2 (t));
}
}
//! Append all variables in a term to a list.
/**
*@param tl The list to which to append to.
*@param t The term possibly containing open and closed variables.
*@return The pointer to the extended list.
*\sa termlistAddVariables()
*/
Termlist
termlistAddRealVariables (Termlist tl, Term t)
{
if (t == NULL)
return tl;
if (realTermLeaf (t))
{
if (realTermVariable (t))
{
Term tbuf = t->subst;
t->subst = NULL;
if (!inTermlist (tl, t))
{
tl = termlistAdd (tl, t);
}
t->subst = tbuf;
return termlistAddRealVariables (tl, t->subst);
}
else
{
return tl;
}
}
else
{
if (realTermEncrypt (t))
return termlistAddVariables (termlistAddVariables (tl, TermOp (t)),
TermKey (t));
else
return
termlistAddVariables (termlistAddVariables (tl, TermOp1 (t)),
TermOp2 (t));
}
}
//! Append all basic terms in a term to a list.
/**
*@param tl The list to which to append to.
*@param t The term containing basic terms.
*@return The pointer to the extended list.
*\sa termlistAddBasics()
*/
Termlist
termlistAddBasic (Termlist tl, Term t)
{
t = deVar (t);
if (t == NULL)
return tl;
if (!realTermLeaf (t))
{
if (realTermEncrypt (t))
return termlistAddBasic (termlistAddBasic (tl, TermOp (t)),
TermKey (t));
else
return termlistAddBasic (termlistAddBasic (tl, TermOp1 (t)),
TermOp2 (t));
}
else
{
if (!inTermlist (tl, t))
{
return termlistAdd (tl, t);
}
}
return tl;
}
//! Append all basic terms in a termlist to another list.
/**
*@param tl The list to which to append to.
*@param scan The termlist with terms containing basic terms.
*@return The pointer to the extended list.
*\sa termlistAddBasic()
*/
Termlist
termlistAddBasics (Termlist tl, Termlist scan)
{
while (scan != NULL)
{
tl = termlistAddBasic (tl, scan->term);
scan = scan->next;
}
return tl;
}
//! Remove a term from a termlist.
/**
* Removes the first occurrence of the term.
*@return A new termlist pointer.
*/
Termlist
termlistMinusTerm (Termlist tl, Term t)
{
Termlist scan;
scan = tl;
while (scan != NULL)
{
if (isTermEqual (scan->term, t))
return termlistDelTerm (scan);
else
scan = scan->next;
}
return tl;
}
//! Determine the length of a termlist.
int
termlistLength (Termlist tl)
{
int i = 0;
while (tl != NULL)
{
tl = tl->next;
i++;
}
return i;
}
//! Give the inverse key term of a term.
/**
* Gives a duplicate of the inverse Key of some term (which is used to encrypt something), as is defined
* by the termlist, which is a list of key1,key1inv, key2, key2inv, etc...
*@param inverses The list of inverses, typically from the knowledge.
*@param key Any term of which the inverse will be determined.
*@return A pointer to a duplicate of the inverse key term. Use termDelete to remove it.
*\sa termDuplicate(), knowledge::inverses
*/
Term
inverseKey (Termlist inverses, Term key)
{
key = deVar (key);
/* is this a function application? i.e. hash? */
if (isTermLeaf (key) && inTermlist (key->stype, TERM_Function))
{
/* functions cannot be inverted by default */
return termDuplicate (TERM_Hidden);
}
/* check for the special case first: when it is effectively a function application */
if (isTermEncrypt (key) && isTermLeaf (TermKey (key))
&& inTermlist (deVar (TermKey (key))->stype, TERM_Function))
{
/* we are scanning for functions */
/* scan the list */
/* key is function application kk(op), or {op}kk */
Term funKey (Term orig, Term newk)
{
/* in: {op}kk, nk
* out: {op'}nk */
return makeTermEncrypt (termDuplicate (TermOp (orig)),
termDuplicate (newk));
}
while (inverses != NULL && inverses->next != NULL)
{
if (isTermEqual (TermKey (key), inverses->term))
return funKey (key, inverses->next->term);
if (isTermEqual (TermKey (key), inverses->next->term))
return funKey (key, inverses->term);
inverses = inverses->next->next;
}
}
else
{
/* scanning for a direct inverse */
/* scan the list */
while (inverses != NULL && inverses->next != NULL)
{
if (isTermEqual (key, inverses->term))
return termDuplicate (inverses->next->term);
if (isTermEqual (key, inverses->next->term))
return termDuplicate (inverses->term);
inverses = inverses->next->next;
}
}
return termDuplicate (key); /* defaults to symmetrical */
}
//! Create a term local to a run.
/*
* We assume that at this point, no variables have been instantiated yet that occur in this term.
* We also assume that fromlist, tolist only hold real leaves.
*
* variable instantiations are not followed through.
*
*\sa termlistLocal()
*/
Term
termLocal (const Term t, Termlist fromlist, Termlist tolist)
{
if (t == NULL)
return NULL;
if (realTermLeaf (t))
{
while (fromlist != NULL && tolist != NULL)
{
if (isTermEqual (fromlist->term, t))
{
// matches!
return tolist->term;
}
fromlist = fromlist->next;
tolist = tolist->next;
}
return t;
}
else
{
Term newt = termNodeDuplicate (t);
if (realTermTuple (t))
{
TermOp1 (newt) = termLocal (TermOp1 (t), fromlist, tolist);
TermOp2 (newt) = termLocal (TermOp2 (t), fromlist, tolist);
}
else
{
TermOp (newt) = termLocal (TermOp (t), fromlist, tolist);
TermKey (newt) = termLocal (TermKey (t), fromlist, tolist);
}
return newt;
}
}
//! Create a list of instance terms.
/**
* We expand the termlocal concept to termlists.
*\sa termLocal()
*/
Termlist
termlistLocal (Termlist tl, const Termlist fromlist, const Termlist tolist)
{
Termlist newtl = NULL;
while (tl != NULL)
{
newtl = termlistAdd (newtl, termLocal (tl->term, fromlist, tolist));
tl = tl->next;
}
return newtl;
}
//! Check whether a termlist is contained in another.
/**
*@param tlbig The big list.
*@param tlsmall The list that is possibly contained in the big one.
*@return True iff tlsmall is contained in tlbig.
*/
int
termlistContained (const Termlist tlbig, Termlist tlsmall)
{
while (tlsmall != NULL)
{
if (!inTermlist (tlbig, tlsmall->term))
return 0;
tlsmall = tlsmall->next;
}
return 1;
}
//! Check substitution validity
/**
* Determine whether a variable has been substituted with something with
* the right type.
*@param matchmode The system matching mode, typically system::match
*@param term The closed variable term.
*@return True iff the substitution is valid in the current mode.
*\sa system::match
*/
int
validSubst (const int matchmode, const Term term)
{
if (!realTermVariable (term) || term->subst == NULL)
return 1;
else
{
switch (matchmode)
{
case 0: /* real type match */
return realTermLeaf (term->subst)
&& termlistContained (term->stype, term->subst->stype);
case 1: /* basic type match */
/* subst must be a leaf */
/* TODO: what about functions? */
return realTermLeaf (term->subst);
case 2: /* no type match */
/* anything goes */
return 1;
default:
return 0;
}
}
}
//! Yield the result of f(x)
/**
* This function interpretes two termlists as the domain and range of a function,
* and if the term occurs in the domain, returns the matching value from the range.
* Note that these functions cannot have NULL in the domain or the range.
*@param fromlist The domain list.
*@param tolist The range list, in a one-to-one correspondence with the fromlist.
*@param tx The point on which the function is to be evaluated.
*@return The result of the function application or NULL if the point is not within the domain.
*/
Term
termFunction (Termlist fromlist, Termlist tolist, Term tx)
{
while (fromlist != NULL && tolist != NULL)
{
if (isTermEqual (fromlist->term, tx))
{
return tolist->term;
}
fromlist = fromlist->next;
tolist = tolist->next;
}
return NULL;
}
//! Yield the last node of a termlist.
Termlist
termlistForward (Termlist tl)
{
if (tl == NULL)
{
return NULL;
}
else
{
while (tl->next != NULL)
{
tl = tl->next;
}
return tl;
}
}
/**
* Compare two termlists containing only basic terms, and yield ordering.
*/
int
termlistOrder (Termlist tl1, Termlist tl2)
{
int order;
order = 0;
while (order == 0 && tl1 != NULL && tl2 != NULL)
{
order = termOrder (tl1->term, tl2->term);
tl1 = tl1->next;
tl2 = tl2->next;
}
if (order != 0)
return order;
if (tl1 == NULL && tl2 == NULL)
return order;
if (tl1 == NULL)
return -1;
else
return 1;
}
//! Iterate over terms in termlist
/**
* Function gets terms
*/
int
termlist_iterate (Termlist tl, int (*func) ())
{
while (tl != NULL)
{
if (!func (tl->term))
return 0;
tl = tl->next;
}
return 1;
}
//! Create a tuple term from a termlist
Term
termlist_to_tuple (Termlist tl)
{
int width;
width = termlistLength (tl);
if (width > 1)
{
// 2 parts
// Make two termlists for each side.
Term tresult;
Termlist tl1, tl2;
int split, i;
/**
* This can be done much more efficiently by cutting
* the list temporarily, and reconnecting it afterwards.
*/
tl1 = NULL;
tl2 = NULL;
split = width / 2;
i = 0;
while (tl != NULL)
{
if (i < split)
tl1 = termlistAdd (tl1, tl->term);
else
tl2 = termlistAdd (tl2, tl->term);
tl = tl->next;
i++;
}
tresult =
makeTermTuple (termlist_to_tuple (tl1), termlist_to_tuple (tl2));
termlistDelete (tl1);
termlistDelete (tl2);
return tresult;
}
else
{
if (tl == NULL)
{
// W00t! Wtf?
error ("termlist_to_tuple called (internally?) with NULL");
}
else
{
// Single node, simple
return termDuplicate (tl->term);
}
}
// @TODO Should be considered an error
return NULL;
}
//! Split a tuple term into termlist components.
Termlist
tuple_to_termlist (Term t)
{
t = deVar (t);
if (t == NULL)
{
return NULL;
}
else
{
if (realTermTuple (t))
{
return termlistConcat (tuple_to_termlist (TermOp1 (t)),
tuple_to_termlist (TermOp2 (t)));
}
else
{
return termlistAdd (NULL, t);
}
}
}
//! Remove all items from tlbig that occur in tlsmall, and return the pointer to the new tlbig.
Termlist
termlistMinusTermlist (const Termlist tlbig, const Termlist tlsmall)
{
Termlist tl;
Termlist tlnewstart;
tl = tlbig;
tlnewstart = tlbig;
while (tl != NULL)
{
if (inTermlist (tlsmall, tl->term))
{
Termlist tlnext;
// Remember next node.
tlnext = tl->next;
// This node should be removed.
tlnewstart = termlistDelTerm (tl);
// Skip to next.
tl = tlnext;
}
else
{
// This item will remain in the list.
tl = tl->next;
}
}
return tlnewstart;
}

67
gui/src/termlist.h
View File

@ -1,67 +0,0 @@
#ifndef TERMLISTS
#define TERMLISTS
#include "term.h"
//! The list container for the term type.
/**
* Implemented as a double linked list to allow for element deletion.
*\sa term
*/
struct termlist
{
//! The term element for this node.
Term term;
//! Next node pointer or NULL for the tail of the list.
struct termlist *next;
//! Previous node pointer or NULL for the head of the list.
struct termlist *prev;
};
//! Shorthand for termlist pointers.
typedef struct termlist *Termlist;
void termlistsInit (void);
void termlistsDone (void);
Termlist termlistDuplicate (Termlist tl);
Termlist termlistShallow (Termlist tl);
void termlistDelete (Termlist tl);
void termlistDestroy (Termlist tl);
void termlistPrint (Termlist tl);
__inline__ int inTermlist (Termlist tl, const Term term);
__inline__ Termlist termlistFind (Termlist tl, const Term term);
int isTermlistEqual (Termlist tl1, Termlist tl2);
Termlist termlistAdd (Termlist tl, Term term);
#define termlistPrepend(tl,t) termlistAdd(tl,t)
Termlist termlistAppend (const Termlist tl, const Term term);
Termlist termlistAddNew (const Termlist tl, const Term t);
Termlist termlistConcat (Termlist tl1, Termlist tl2);
Termlist termlistConcatStatic (Termlist tl1, Termlist tl2);
Termlist termlistDelTerm (Termlist tl);
Termlist termlistConjunct (Termlist tl1, Termlist tl2);
Termlist termlistConjunctType (Termlist tl1, Termlist tl2, int termtype);
Termlist termlistType (Termlist tl, int termtype);
Termlist termlistAddVariables (Termlist tl, Term t);
Termlist termlistAddRealVariables (Termlist tl, Term t);
Termlist termlistAddBasic (Termlist tl, Term t);
Termlist termlistAddBasics (Termlist tl, Termlist scan);
Termlist termlistMinusTerm (Termlist tl, Term t);
int termlistLength (Termlist tl);
Term inverseKey (Termlist inverses, Term key);
Term termLocal (const Term t, Termlist fromlist, Termlist tolist);
Termlist termlistLocal (Termlist tl, const Termlist fromlist,
const Termlist tolist);
int termlistContained (const Termlist tlbig, Termlist tlsmall);
int validSubst (const int matchmode, const Term term);
Term termFunction (Termlist fromlist, Termlist tolist, Term tx);
Termlist termlistForward (Termlist tl);
int termlistOrder (Termlist tl1, Termlist tl2);
int termlist_iterate (Termlist tl, int (*func) ());
Term termlist_to_tuple (Termlist tl);
Termlist tuple_to_termlist (Term t);
Termlist termlistMinusTermlist (const Termlist tlbig, const Termlist tlsmall);
#define TERMLISTADD(l,t) l = termlistAdd (l,t)
#define TERMLISTAPPEND(l,t) l = termlistAppend (l,t)
#endif

123
gui/src/termmap.c
View File

@ -1,123 +0,0 @@
#include <stdlib.h>
#include <stdio.h>
#include "termmap.h"
#include "debug.h"
//! Open termmaps code.
void
termmapsInit (void)
{
return;
}
//! Close termmaps code.
void
termmapsDone (void)
{
return;
}
//! Allocate memory for a termmap node.
/**
*@return A pointer to uninitialised memory of the size of a termmap node.
*/
Termmap
makeTermmap (void)
{
/* inline candidate */
return (Termmap) malloc (sizeof (struct termmap));
}
//! Get function result
/**
*@return Yields f(x), or -1 when it is not present.
*/
int
termmapGet (Termmap f, const Term x)
{
while (f != NULL)
{
if (isTermEqual (x, f->term))
return f->result;
f = f->next;
}
return -1;
}
//! Add a value to a function.
/**
*@return Adds f(x)=y to an existing function f. If f is NULL, a function is created. If x is already in the domain, the value is replaced.
*/
Termmap
termmapSet (const Termmap f, const Term x, const int y)
{
Termmap fscan;
//! Determine whether term already occurs
fscan = f;
while (fscan != NULL)
{
if (isTermEqual (x, fscan->term))
{
//! Is the result correct already?
if (fscan->result != y)
fscan->result = y;
return f;
}
fscan = fscan->next;
}
//! Not occurred yet, make new node
fscan = makeTermmap ();
fscan->term = x;
fscan->result = y;
fscan->next = f;
return fscan;
}
//! Duplicate a function
Termmap
termmapDuplicate (const Termmap f)
{
if (f != NULL)
{
Termmap g;
g = makeTermmap ();
g->term = f->term;
g->result = f->result;
g->next = termmapDuplicate (f->next);
return g;
}
else
{
return NULL;
}
}
//! Delete a function
void
termmapDelete (const Termmap f)
{
if (f != NULL)
{
termmapDelete (f->next);
free (f);
}
}
//! Print a function
void
termmapPrint (Termmap f)
{
if (f != NULL)
{
eprintf ("\"");
termPrint (f->term);
eprintf ("\" -> %i", f->result);
if (f->next != NULL)
{
eprintf (", ");
termmapPrint (f->next);
}
}
}

31
gui/src/termmap.h
View File

@ -1,31 +0,0 @@
#ifndef TERMMAPS
#define TERMMAPS
#include "term.h"
//! The function container for the term to integer function type.
/**
*\sa term
*/
struct termmap
{
//! The term element for this node.
Term term;
//! Next node pointer or NULL for the last element of the function.
struct termmap *next;
//! Function result
int result;
};
//! Shorthand for termmap pointers.
typedef struct termmap *Termmap;
void termmapsInit (void);
void termmapsDone (void);
int termmapGet (Termmap f, const Term x);
Termmap termmapSet (const Termmap f, const Term x, const int y);
Termmap termmapDuplicate (const Termmap f);
void termmapDelete (const Termmap f);
void termmapPrint (Termmap f);
#endif

69
gui/src/timer.c
View File

@ -1,69 +0,0 @@
#include "timer.h"
/*
* Timer functions
*
* Currently, this only works under linux (where the linux macro is defined by the compiler). Otherwise, it simply assumes the timer is never passed.
*/
#ifdef linux
#include <time.h>
#include <sys/times.h>
static clock_t endwait = 0;
#endif
static int time_max_seconds = 0;
//! Set initial time limit.
/**
* <= 0 means none.
*/
void
set_time_limit (int seconds)
{
if (seconds > 0)
{
time_max_seconds = seconds;
#ifdef linux
endwait = seconds * CLOCKS_PER_SEC;
#endif
}
else
{
time_max_seconds = 0;
#ifdef linux
endwait = 0;
#endif
}
}
//! Retrieve time limit
int
get_time_limit ()
{
return time_max_seconds;
}
//! Check whether time limit has passed.
int
passed_time_limit ()
{
#ifdef linux
if (endwait <= 0)
{
return 0;
}
else
{
struct tms t;
times (&t);
if (t.tms_utime > endwait)
return 1;
else
return 0;
}
#else
return 0;
#endif
}

8
gui/src/timer.h
View File

@ -1,8 +0,0 @@
#ifndef TIMER
#define TIMER
void set_time_limit (int seconds);
int get_time_limit ();
int passed_time_limit ();
#endif

51
gui/src/todo.txt
View File

@ -1,51 +0,0 @@
- Error should have an additional line number parameter (that might be
-1 to ignore it) forcing people to use numbers :)
Format: "error: [%i] %s\n"
- Nested functions should be avoided: their implementation requires an
executable stack, which is bad for security purposes. However, many of
the iterator functions need to pass a function and possibly some
variables. Currently, the variables are handled by the nested function
mechanism (the iterated nested function and address variables of the
function it is part of), which would not work anymore. A possible
solution seems variable argument count functions, but this is fairly
cumbersome and might impact on performance. Alternatively, iterators
can be implemented as macros, which is probably the fastest, but maybe
less readable.
- --check is slightly f***ed up because there is no good semantics for
the --disable intruder check. As a result, it is now too strict can
cause correct protocols to fail. Fix.
- When *not* asking for attack output, maybe we should default to
--prune = 1. Then, if we ask for --xml output or --dot, we do:
if --prune == 1 then --prune == 2 now :) unless otherwise specified.
(This should be done after switch checking)
- Old version enforced some extra orders:
1. M_0 roles were ordered before any other roles.
2. Local constants order: if a run has a local variable instantiated by
somebody else's variable, that should occur then after the initial sending
of that value...
- Test 'sk(x)' in goals, somewhere before assessing a state (dus at the
beginning of iterate), immediately reduce to 'sk(Eve)'. Test with
--experimental. To that end, reintroduce a state-reporting switch.
- It is currently not well-defined to define inversekeys within a role:
this requires some work at instantiation, because instantiated term
couples should be added to the inverses list, and removed at
descruction.
- Simple timestamps could be added by prefixing send message before the
role, sending any timestamp constants out first to the intruder. These
should of course be hidden in the output somehow.
- Notes on the new attack group displays:
* We want to group runs into consistent protocol runs.
* Minimal req. for protocol run: equal \rho.
* If two runs are candidates for a role in a protocol run,
use a metric based on order and data. Maybe data is more important:
if equal data, than order might be irrelevant.
* Maybe we should refactor the xmlOut code first. In an extreme case,
we first factor out all logic, and ranking, and grouping, in to a
prepareAttackOutput structure; with a separate source file. Later we
can convert this to either ASCII or DOT or XML or something.
Now that I think of it; XML should be a plain state probably, and we
could add a switch to also output more detailed attack things (is
that relevant?)
- SConstruct file should check whether ctags actually exists (avoiding
errors)
- Proof output should be XML, with an external converter to dot format.

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