diff --git a/AUTHORS b/AUTHORS deleted file mode 100644 index 19960d4..0000000 --- a/AUTHORS +++ /dev/null @@ -1,31 +0,0 @@ -================== -# Scyther README # -================== - ----------------- -1. About Scyther ----------------- - -Scyther bla Cas andsoforth, bla Lutger, yada yada yada. - ---------------- -2. Requirements ---------------- - -Scyther compilation depends on a few external items: - -- A C compiler (gcc or anything modern *nixy will do) -- The Flex and Bison scanner/compiler generation tools. - -These two requirements are usually met by default by any modern *nix -variant, such as GNU/Linux. - -If you want LaTeX output we need - -- LaTeX -- The MSC macro package msc.sty - -For the documentation generation, optionally with graphs. -- Doxygen: http://www.doxygen.org/ -- Dot: http://www.research.att.com/sw/tools/graphviz/ - diff --git a/Mac-installation-notes.txt b/Mac-installation-notes.txt deleted file mode 100644 index 51e54d2..0000000 --- a/Mac-installation-notes.txt +++ /dev/null @@ -1,13 +0,0 @@ -Mac - -MacPorts (Martijn) - -- Easy - -Fink (Christoph) - -- Lots of stuff problematic, probably easiest to install elementtree locally into the Scyther directory. (package-rev/elementtree into Scyther) - -- Leave Python version as is, install dot/graphviz, wx seems to be there already. - -- pythonw needed to start for screen access diff --git a/Design/bikewheel-improved.jpg b/design/bikewheel-improved.jpg similarity index 100% rename from Design/bikewheel-improved.jpg rename to design/bikewheel-improved.jpg diff --git a/Design/characterize-button.png b/design/characterize-button.png similarity index 100% rename from Design/characterize-button.png rename to design/characterize-button.png diff --git a/Design/characterize-button.svg b/design/characterize-button.svg similarity index 100% rename from Design/characterize-button.svg rename to design/characterize-button.svg diff --git a/Design/new-angles-reference.svg b/design/new-angles-reference.svg similarity index 100% rename from Design/new-angles-reference.svg rename to design/new-angles-reference.svg diff --git a/Design/scyther-button-beta6-angle.svg b/design/scyther-button-beta6-angle.svg similarity index 100% rename from Design/scyther-button-beta6-angle.svg rename to design/scyther-button-beta6-angle.svg diff --git a/Design/scyther-button-beta6.svg b/design/scyther-button-beta6.svg similarity index 100% rename from Design/scyther-button-beta6.svg rename to design/scyther-button-beta6.svg diff --git a/Design/scyther-button.svg b/design/scyther-button.svg similarity index 100% rename from Design/scyther-button.svg rename to design/scyther-button.svg diff --git a/Design/scyther-logo.svg b/design/scyther-logo.svg similarity index 100% rename from Design/scyther-logo.svg rename to design/scyther-logo.svg diff --git a/Design/scyther-splash.eps b/design/scyther-splash.eps similarity index 100% rename from Design/scyther-splash.eps rename to design/scyther-splash.eps diff --git a/Design/scyther-splash.png b/design/scyther-splash.png similarity index 100% rename from Design/scyther-splash.png rename to design/scyther-splash.png diff --git a/Design/scyther-splash.svg b/design/scyther-splash.svg similarity index 100% rename from Design/scyther-splash.svg rename to design/scyther-splash.svg diff --git a/Design/scyther-splash.xcf b/design/scyther-splash.xcf similarity index 100% rename from Design/scyther-splash.xcf rename to design/scyther-splash.xcf diff --git a/Design/verify-button.png b/design/verify-button.png similarity index 100% rename from Design/verify-button.png rename to design/verify-button.png diff --git a/Design/verify-button.svg b/design/verify-button.svg similarity index 100% rename from Design/verify-button.svg rename to design/verify-button.svg diff --git a/gui/src/BuildMacIntel-MacPPC.cmake b/gui/src/BuildMacIntel-MacPPC.cmake new file mode 100644 index 0000000..7532732 --- /dev/null +++ b/gui/src/BuildMacIntel-MacPPC.cmake @@ -0,0 +1,8 @@ +################################################################ +# Name: BuildMacIntel-MacPPC.cmake +# Purpose: Build MacPPC binary on MacIntel +# Author: Cas Cremers +################################################################ + +include (BuildMacPPC.cmake) + diff --git a/gui/src/BuildMacIntel.cmake b/gui/src/BuildMacIntel.cmake new file mode 100644 index 0000000..f8ce918 --- /dev/null +++ b/gui/src/BuildMacIntel.cmake @@ -0,0 +1,11 @@ +################################################################ +# Name: BuildMacIntel.cmake +# Purpose: Build MacIntel binary +# Author: Cas Cremers +################################################################ + +message (STATUS "Building Apple Mac Intel version") +set (scythername "scyther-macintel") +add_executable (${scythername} ${Scyther_sources}) +set (CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -fnested-functions -arch i386") + diff --git a/gui/src/BuildMacPPC-MacIntel.cmake b/gui/src/BuildMacPPC-MacIntel.cmake new file mode 100644 index 0000000..dc6a827 --- /dev/null +++ b/gui/src/BuildMacPPC-MacIntel.cmake @@ -0,0 +1,8 @@ +################################################################ +# Name: BuildMacPPC-MacIntel.cmake +# Purpose: Build MacIntel binary on MacPPC +# Author: Cas Cremers +################################################################ + +include (BuildMacIntel.cmake) + diff --git a/gui/src/BuildMacPPC.cmake b/gui/src/BuildMacPPC.cmake new file mode 100644 index 0000000..8fe87a0 --- /dev/null +++ b/gui/src/BuildMacPPC.cmake @@ -0,0 +1,11 @@ +################################################################ +# Name: BuildMacPPC.cmake +# Purpose: Build MacPPC binary +# Author: Cas Cremers +################################################################ + +message (STATUS "Building Apple Mac PPC version") +set (scythername "scyther-macppc") +add_executable (${scythername} ${Scyther_sources}) +set (CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -fnested-functions -arch ppc") + diff --git a/gui/src/BuildPlatform.cmake b/gui/src/BuildPlatform.cmake new file mode 100644 index 0000000..f54a5eb --- /dev/null +++ b/gui/src/BuildPlatform.cmake @@ -0,0 +1,36 @@ +################################################################ +# Name: BuildPlatform.cmake +# Purpose: Make platform-dependant decisions +# Author: Cas Cremers +################################################################ + +# Add target for Universal Binary when needed +if (APPLE) + include (UniversalBinary.cmake) +endif (APPLE) + +# Retrieve Source_OS, Destination_OS (from -DTARGET) +include (GetOS.cmake) + +# From source_os and destination_os make a new name for the build script +if (Source_OS STREQUAL Destination_OS) + set (BuildScriptName "Build${Source_OS}.cmake") +else (Source_OS STREQUAL Destination_OS) + set (BuildScriptName "Build${Source_OS}-${Destination_OS}.cmake") +endif (Source_OS STREQUAL Destination_OS) +message (STATUS "Locating platform specific file ${BuildScriptName}") + +# Locate the file. If it exists, start it +if (EXISTS ${BuildScriptName}) + # Execute the build script + include (${BuildScriptName}) +else (EXISTS ${BuildScriptName}) + # Could not find it! + message (STATUS "Could not find ${BuildScriptName}") + if (Source_OS STREQUAL Destination_OS) + message (FATAL_ERROR "Don't know how to build on ${Source_OS}") + else (Source_OS STREQUAL Destination_OS) + message (FATAL_ERROR "Don't know how to build for ${Destination_OS} on ${Source_OS}") + endif (Source_OS STREQUAL Destination_OS) +endif (EXISTS ${BuildScriptName}) + diff --git a/gui/src/BuildUnix-Win32.cmake b/gui/src/BuildUnix-Win32.cmake new file mode 100644 index 0000000..ba4a26f --- /dev/null +++ b/gui/src/BuildUnix-Win32.cmake @@ -0,0 +1,15 @@ +################################################################ +# Name: BuildUnix-Win32.cmake +# Purpose: Build Win32 binary on Unix +# Author: Cas Cremers +################################################################ + +message (STATUS "Building W32 version") +# This should work on win32 platform, but also when the compiler +# is available anyway under linux +set (CMAKE_C_COMPILER "i586-mingw32msvc-gcc") +set (CMAKE_CXX_COMPILER "i586-mingw32msvc-g++") +set (CMAKE_SHARED_LIBRARY_LINK_C_FLAGS) # to get rid of -rdynamic +set (scythername "scyther-w32.exe") +add_executable (${scythername} ${Scyther_sources}) + diff --git a/gui/src/BuildUnix.cmake b/gui/src/BuildUnix.cmake new file mode 100644 index 0000000..8985f42 --- /dev/null +++ b/gui/src/BuildUnix.cmake @@ -0,0 +1,12 @@ +################################################################ +# Name: BuildUnix.cmake +# Purpose: Build Unix binary on self +# Author: Cas Cremers +################################################################ + +# We call it linux, because that is what de-facto is the case. + +message (STATUS "Building Linux version") +set (scythername "scyther-linux") +add_executable (${scythername} ${Scyther_sources}) + diff --git a/gui/src/CMakeLists.txt b/gui/src/CMakeLists.txt new file mode 100644 index 0000000..dc4b53c --- /dev/null +++ b/gui/src/CMakeLists.txt @@ -0,0 +1,37 @@ +################################################################ +# Name: CMakeLists.txt +# Purpose: Input file for CMake for the Scyther tool +# Author: Cas Cremers +################################################################ + +# Scyther project +project (Scyther) +# I need 2.4 for flex/etc although it does not run yet +CMAKE_MINIMUM_REQUIRED(VERSION 2.4) + +# List all the source files +set (Scyther_sources + arachne.c binding.c claim.c color.c compiler.c cost.c + debug.c depend.c dotout.c error.c heuristic.c hidelevel.c + intruderknowledge.c knowledge.c label.c list.c main.c mgu.c + prune_bounds.c prune_theorems.c role.c + specialterm.c states.c switches.c symbol.c system.c tac.c + termlist.c termmap.c term.c timer.c type.c warshall.c xmlout.c + parser.c scanner.c + ) + +# If we are in a debug mode we want to be strict +set (CMAKE_C_FLAGS_DEBUG "${CMAKE_C_FLAGS_DEBUG} -Wall -DDEBUG") + +# Usual static +set (CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -static") + +# Determine version number +include (SVNVersion.cmake) + +# Make scanner and parser +include (ScannerParser.cmake) + +# Set build target settings according to platform +include (BuildPlatform.cmake) + diff --git a/gui/src/FindBISON.cmake b/gui/src/FindBISON.cmake new file mode 100644 index 0000000..e07dd04 --- /dev/null +++ b/gui/src/FindBISON.cmake @@ -0,0 +1,33 @@ +# - Try to find Bison +# Once done this will define +# +# BISON_FOUND - system has Bison +# BISON_EXECUTABLE - path of the bison executable +# BISON_VERSION - the version string, like "2.5.31" +# + + +FIND_PROGRAM(BISON_EXECUTABLE NAMES bison) +mark_as_advanced(BISON_DIR Bison_DIR) + +#INCLUDE(MacroEnsureVersion) + +IF(BISON_EXECUTABLE) + SET(BISON_FOUND TRUE) + + EXECUTE_PROCESS(COMMAND ${BISON_EXECUTABLE} --version + OUTPUT_VARIABLE _BISON_VERSION + ) + string (REGEX MATCH "[0-9]+\\.[0-9]+\\.[0-9]+" BISON_VERSION "${_bison_VERSION}") +ENDIF(BISON_EXECUTABLE) + +IF(BISON_FOUND) + IF(NOT Bison_FIND_QUIETLY) + MESSAGE(STATUS "Found Bison: ${BISON_EXECUTABLE}") + ENDIF(NOT Bison_FIND_QUIETLY) +ELSE(BISON_FOUND) + IF(Bison_FIND_REQUIRED) + MESSAGE(FATAL_ERROR "Could not find Bison") + ENDIF(Bison_FIND_REQUIRED) +ENDIF(BISON_FOUND) + diff --git a/gui/src/FindFLEX.cmake b/gui/src/FindFLEX.cmake new file mode 100644 index 0000000..34312e6 --- /dev/null +++ b/gui/src/FindFLEX.cmake @@ -0,0 +1,33 @@ +# - Try to find Flex +# Once done this will define +# +# FLEX_FOUND - system has Flex +# FLEX_EXECUTABLE - path of the flex executable +# FLEX_VERSION - the version string, like "2.5.31" +# + + +FIND_PROGRAM(FLEX_EXECUTABLE NAMES flex) +mark_as_advanced(FLEX_DIR Flex_DIR) + +#INCLUDE(MacroEnsureVersion) + +IF(FLEX_EXECUTABLE) + SET(FLEX_FOUND TRUE) + + EXECUTE_PROCESS(COMMAND ${FLEX_EXECUTABLE} --version + OUTPUT_VARIABLE _FLEX_VERSION + ) + string (REGEX MATCH "[0-9]+\\.[0-9]+\\.[0-9]+" FLEX_VERSION "${_FLEX_VERSION}") +ENDIF(FLEX_EXECUTABLE) + +IF(FLEX_FOUND) + IF(NOT Flex_FIND_QUIETLY) + MESSAGE(STATUS "Found Flex: ${FLEX_EXECUTABLE}") + ENDIF(NOT Flex_FIND_QUIETLY) +ELSE(FLEX_FOUND) + IF(Flex_FIND_REQUIRED) + MESSAGE(FATAL_ERROR "Could not find Flex") + ENDIF(Flex_FIND_REQUIRED) +ENDIF(FLEX_FOUND) + diff --git a/gui/src/GetOS.cmake b/gui/src/GetOS.cmake new file mode 100644 index 0000000..d1b023f --- /dev/null +++ b/gui/src/GetOS.cmake @@ -0,0 +1,43 @@ +################################################################ +# Name: GetOS.cmake +# Purpose: Determine Source_OS and Destination_OS (-DTARGETOS) +# Author: Cas Cremers +################################################################ + +# Supported types: +# +# Win32 +# Unix +# MacPPC +# MacIntel + +# First we find out the current operating system +set (Source_OS) +if (WIN32) + # Windows + set (Source_OS "Win32") +else (WIN32) + # Not windows, is it a mac? + if (APPLE) + # TODO: A mac, but what architecture? + # For now we assume intel (Christoph Sprenger's machine) + set (Source_OS "MacIntel") + else (APPLE) + # Not a mac, not windows + if (UNIX) + set (Source_OS "Unix") + else (UNIX) + message (FATAL "Unrecognized source platform.") + endif (UNIX) + endif (APPLE) +endif (WIN32) +#message (STATUS "Source platform: ${Source_OS}") + +# Destination? If target is unset, we just take the source +if (TARGETOS) + set (Destination_OS "${TARGETOS}") +else (TARGETOS) + set (Destination_OS "${Source_OS}") +endif (TARGETOS) +#message (STATUS "Destination platform: ${Destination_OS}") + diff --git a/gui/src/Makefile-fallback b/gui/src/Makefile-fallback new file mode 100644 index 0000000..22694f2 --- /dev/null +++ b/gui/src/Makefile-fallback @@ -0,0 +1,86 @@ +# +# Scyther Makefile +# + +# +# DEBUG or optimization settings: uncomment a single line: +# +CFLAGS = -g3 -D DEBUG # default usage, for e.g. with valgrind +#CFLAGS = -g3 -D DEBUG -pg # for code profiling with gprof +#CFLAGS = -O3 -static -finline-functions -fomit-frame-pointer + +# +# Compiler and linkage +# +CC = gcc +# Note that these paths must include the path to the argtable library. +CPPFLAGS = -I/scratch/ccremers/include -I/usr/local/include -Wall +LDFLAGS = -L/scratch/ccremers/lib -L/usr/local/lib +LOADLIBS = -lfl +LDLIBS = -largtable2 +OPTIONS = ${CPPFLAGS} ${CFLAGS} ${LDFLAGS} + +# +# Module set for the modelchecker +# +MODULES=memory.o terms.o termlists.o symbols.o knowledge.o runs.o modelchecker.o \ +report.o debug.o mgu.o substitutions.o \ +match_basic.o \ +match_clp.o constraints.o \ +output.o latex.o \ +varbuf.o tracebuf.o attackminimize.o \ +tac.o parser.o compiler.o + +# +# Dependencies +# +MODELCHECKER = ${MODULES} main.o + +all: scyther tags + +${Target}.o: ${Target}.c + $(CC) $(OPTIONS) ${Target}.c -c + +scanner.c: scanner.lex + flex scanner.lex + cp lex.yy.c scanner.c + +tok.h: parser.c + +parser.c: parser.y + bison -d -v parser.y + cp parser.tab.c parser.c + cmp -s parser.tab.h tok.h || cp parser.tab.h tok.h + +tags: *.c *.h + ctags *.c *.h + +modules: $(MODULES) + +scyther: scanner.o $(MODELCHECKER) + $(CC) $(OPTIONS) $(MODELCHECKER) -o scyther $(LOADLIBS) $(LDLIBS) + +ptestmain.o scanner.o : tok.h + +# +# Cleanup +# +clean: + rm -f *.o + rm -f scyther + rm -f scanner.c + rm -f parser.c + rm -f tok.h +# +# Clean and rebuild: 'make new' +# +new: + make clean + make all + +# +# Make doxygen reference manuals. (in ../refman) +# +refman: doxyconfig + doxygen doxyconfig + diff --git a/gui/src/SVNVersion.cmake b/gui/src/SVNVersion.cmake new file mode 100644 index 0000000..a8350af --- /dev/null +++ b/gui/src/SVNVersion.cmake @@ -0,0 +1,58 @@ +################################################################ +# Name: SVNVersion.cmake +# Purpose: Determine subversion revision id for Scyther +# and write it into a macro in version.h +# Author: Cas Cremers +################################################################ + +# Technically, this only needs to be redone each time a file +# changes, so this is a target with dependencies on all files. + +# Checkout version info +find_program (SVNVERSION_EXECUTABLE NAMES svnversion) +mark_as_advanced (SVNVERSION_EXECUTABLE) +mark_as_advanced (SVNVERSION_DYNAMIC) +set (SVNVERSION_DYNAMIC false) +if (SVNVERSION_EXECUTABLE) + # test whether svnversion gives useful info + execute_process ( + COMMAND ${SVNVERSION_EXECUTABLE} --no-newline + OUTPUT_VARIABLE SVN_Result + ) + mark_as_advanced (SVN_Result) + if (NOT ${SVN_Result} STREQUAL "exported") + # svnversion gives useful stuff + ## write to file + #file (WRITE version.h "#define SVNVERSION \"${SVN_Result}\"\n") + set (SVNVERSION_DYNAMIC true) + endif (NOT ${SVN_Result} STREQUAL "exported") + mark_as_advanced (SVNDIR) +endif (SVNVERSION_EXECUTABLE) + +# If dynamic generation is required, this means another target in the +# makefile +if (SVNVERSION_DYNAMIC) + # add a command to generate version.h + message (STATUS "Generating version.h dynamically using svnversion command") + add_custom_command ( + OUTPUT version.h + # The version number depends on all the files; if they + # don't change, neither should the version number + # (although this might be incorrect when updating the + # current directory) + DEPENDS ${Scyther_sources} + DEPENDS .svn + COMMAND ./subbuild-version-information.sh + COMMENT "Generating subversion and tag version information in version.h using svnversion command" + ) +else (SVNVERSION_DYNAMIC) + # Don't dynamically generate, simply empty every time + file (WRITE version.h "#define SVNVERSION \"Unknown\"\n#define TAGVERSION \"Unknown\"") +endif (SVNVERSION_DYNAMIC) + +# add the version number to the sources +set_source_files_properties(version.h + PROPERTIES + GENERATED true) +set (Scyther_sources ${Scyther_sources} version.h) + diff --git a/gui/src/ScannerParser.cmake b/gui/src/ScannerParser.cmake new file mode 100644 index 0000000..a778c3f --- /dev/null +++ b/gui/src/ScannerParser.cmake @@ -0,0 +1,41 @@ +################################################################ +# Name: ScannerParser.cmake +# Purpose: If flex/bison are available, generate parser and scanner +# Author: Cas Cremers +################################################################ + +# Make the scanner using flex, if it can be found +include(FindFLEX.cmake) +if (FLEX_FOUND) + set_source_files_properties(scanner.c PROPERTIES GENERATED true) + ADD_CUSTOM_COMMAND ( + OUTPUT scanner.c + DEPENDS scanner.l + COMMAND ${FLEX_EXECUTABLE} + # TODO: I should look up from which version the -o + # switch works, might not be portable. + ARGS -oscanner.c scanner.l + COMMENT "Building scanner.c from scanner.l using flex" + ) +else (FLEX_FOUND) + message (STATUS "Because flex is not found, we will use the existing scanner.c") +endif (FLEX_FOUND) + +# Make the parser using bison, if it can be found +include(FindBISON.cmake) +if (BISON_FOUND) + set_source_files_properties(parser.c PROPERTIES GENERATED true) + ADD_CUSTOM_COMMAND ( + OUTPUT parser.c + DEPENDS parser.y + COMMAND ${BISON_EXECUTABLE} + # TODO: I should look up from which version the -o + # switch works, might not be portable. + ARGS -d -oparser.c parser.y + COMMENT "Building parser.c from parser.y using bison" + ) +else (BISON_FOUND) + message (STATUS "Because bison is not found, we will use the existing parser.c") +endif (BISON_FOUND) + + diff --git a/gui/src/Scyther.dev b/gui/src/Scyther.dev new file mode 100644 index 0000000..c50735f --- /dev/null +++ b/gui/src/Scyther.dev @@ -0,0 +1,789 @@ +[Project] +FileName=Scyther.dev +Name=Scyther +UnitCount=72 +Type=1 +Ver=1 +ObjFiles= +Includes= +Libs= +PrivateResource= +ResourceIncludes= +MakeIncludes= +Compiler= +CppCompiler= +Linker= +IsCpp=0 +Icon= +ExeOutput=..\gui\Scyther +ObjectOutput= +OverrideOutput=0 +OverrideOutputName=Scyther.exe +HostApplication= +Folders= +CommandLine= +UseCustomMakefile=0 +CustomMakefile= +IncludeVersionInfo=0 +SupportXPThemes=0 +CompilerSet=0 +CompilerSettings=0000000000000000000000 + +[Unit1] +FileName=xmlout.h +CompileCpp=0 +Folder=Scyther +Compile=1 +Link=1 +Priority=1000 +OverrideBuildCmd=0 +BuildCmd= + +[Unit2] +FileName=arachne.c +CompileCpp=0 +Folder=Scyther +Compile=1 +Link=1 +Priority=1000 +OverrideBuildCmd=0 +BuildCmd= + +[Unit3] +FileName=arachne.h +CompileCpp=0 +Folder=Scyther +Compile=1 +Link=1 +Priority=1000 +OverrideBuildCmd=0 +BuildCmd= + +[Unit4] +FileName=binding.c +CompileCpp=0 +Folder=Scyther +Compile=1 +Link=1 +Priority=1000 +OverrideBuildCmd=0 +BuildCmd= + +[Unit5] +FileName=binding.h +CompileCpp=0 +Folder=Scyther +Compile=1 +Link=1 +Priority=1000 +OverrideBuildCmd=0 +BuildCmd= + +[Unit6] +FileName=claim.c +CompileCpp=0 +Folder=Scyther +Compile=1 +Link=1 +Priority=1000 +OverrideBuildCmd=0 +BuildCmd= + +[Unit7] +FileName=claim.h +CompileCpp=0 +Folder=Scyther +Compile=1 +Link=1 +Priority=1000 +OverrideBuildCmd=0 +BuildCmd= + +[Unit8] +FileName=color.c +CompileCpp=0 +Folder=Scyther +Compile=1 +Link=1 +Priority=1000 +OverrideBuildCmd=0 +BuildCmd= + +[Unit9] +FileName=color.h +CompileCpp=0 +Folder=Scyther +Compile=1 +Link=1 +Priority=1000 +OverrideBuildCmd=0 +BuildCmd= + +[Unit10] +FileName=compiler.c +CompileCpp=0 +Folder=Scyther +Compile=1 +Link=1 +Priority=1000 +OverrideBuildCmd=0 +BuildCmd= + +[Unit11] +FileName=compiler.h +CompileCpp=0 +Folder=Scyther +Compile=1 +Link=1 +Priority=1000 +OverrideBuildCmd=0 +BuildCmd= + +[Unit12] +FileName=cost.c +CompileCpp=0 +Folder=Scyther +Compile=1 +Link=1 +Priority=1000 +OverrideBuildCmd=0 +BuildCmd= + +[Unit13] +FileName=cost.h +CompileCpp=0 +Folder=Scyther +Compile=1 +Link=1 +Priority=1000 +OverrideBuildCmd=0 +BuildCmd= + +[Unit14] +FileName=debug.c +CompileCpp=0 +Folder=Scyther +Compile=1 +Link=1 +Priority=1000 +OverrideBuildCmd=0 +BuildCmd= + +[Unit15] +FileName=debug.h +CompileCpp=0 +Folder=Scyther +Compile=1 +Link=1 +Priority=1000 +OverrideBuildCmd=0 +BuildCmd= + +[Unit16] +FileName=depend.c +CompileCpp=0 +Folder=Scyther +Compile=1 +Link=1 +Priority=1000 +OverrideBuildCmd=0 +BuildCmd= + +[Unit17] +FileName=depend.h +CompileCpp=0 +Folder=Scyther +Compile=1 +Link=1 +Priority=1000 +OverrideBuildCmd=0 +BuildCmd= + +[Unit18] +FileName=dotout.c +CompileCpp=0 +Folder=Scyther +Compile=1 +Link=1 +Priority=1000 +OverrideBuildCmd=0 +BuildCmd= + +[Unit19] +FileName=dotout.h +CompileCpp=0 +Folder=Scyther +Compile=1 +Link=1 +Priority=1000 +OverrideBuildCmd=0 +BuildCmd= + +[Unit20] +FileName=error.c +CompileCpp=0 +Folder=Scyther +Compile=1 +Link=1 +Priority=1000 +OverrideBuildCmd=0 +BuildCmd= + +[Unit21] +FileName=error.h +CompileCpp=0 +Folder=Scyther +Compile=1 +Link=1 +Priority=1000 +OverrideBuildCmd=0 +BuildCmd= + +[Unit22] +FileName=heuristic.c +CompileCpp=0 +Folder=Scyther +Compile=1 +Link=1 +Priority=1000 +OverrideBuildCmd=0 +BuildCmd= + +[Unit23] +FileName=heuristic.h +CompileCpp=0 +Folder=Scyther +Compile=1 +Link=1 +Priority=1000 +OverrideBuildCmd=0 +BuildCmd= + +[Unit24] +FileName=hidelevel.c +CompileCpp=0 +Folder=Scyther +Compile=1 +Link=1 +Priority=1000 +OverrideBuildCmd=0 +BuildCmd= + +[Unit25] +FileName=hidelevel.h +CompileCpp=0 +Folder=Scyther +Compile=1 +Link=1 +Priority=1000 +OverrideBuildCmd=0 +BuildCmd= + +[Unit26] +FileName=intruderknowledge.c +CompileCpp=0 +Folder=Scyther +Compile=1 +Link=1 +Priority=1000 +OverrideBuildCmd=0 +BuildCmd= + +[Unit27] +FileName=intruderknowledge.h +CompileCpp=0 +Folder=Scyther +Compile=1 +Link=1 +Priority=1000 +OverrideBuildCmd=0 +BuildCmd= + +[Unit28] +FileName=knowledge.c +CompileCpp=0 +Folder=Scyther +Compile=1 +Link=1 +Priority=1000 +OverrideBuildCmd=0 +BuildCmd= + +[Unit29] +FileName=knowledge.h +CompileCpp=0 +Folder=Scyther +Compile=1 +Link=1 +Priority=1000 +OverrideBuildCmd=0 +BuildCmd= + +[Unit30] +FileName=label.c +CompileCpp=0 +Folder=Scyther +Compile=1 +Link=1 +Priority=1000 +OverrideBuildCmd=0 +BuildCmd= + +[Unit31] +FileName=label.h +CompileCpp=0 +Folder=Scyther +Compile=1 +Link=1 +Priority=1000 +OverrideBuildCmd=0 +BuildCmd= + +[Unit32] +FileName=list.c +CompileCpp=0 +Folder=Scyther +Compile=1 +Link=1 +Priority=1000 +OverrideBuildCmd=0 +BuildCmd= + +[Unit33] +FileName=list.h +CompileCpp=0 +Folder=Scyther +Compile=1 +Link=1 +Priority=1000 +OverrideBuildCmd=0 +BuildCmd= + +[Unit35] +FileName=mgu.h +CompileCpp=0 +Folder=Scyther +Compile=1 +Link=1 +Priority=1000 +OverrideBuildCmd=0 +BuildCmd= + +[Unit36] +FileName=pheading.h +CompileCpp=0 +Folder=Scyther +Compile=1 +Link=1 +Priority=1000 +OverrideBuildCmd=0 +BuildCmd= + +[Unit37] +FileName=prune_bounds.c +CompileCpp=0 +Folder=Scyther +Compile=1 +Link=1 +Priority=1000 +OverrideBuildCmd=0 +BuildCmd= + +[Unit38] +FileName=prune_bounds.h +CompileCpp=0 +Folder=Scyther +Compile=1 +Link=1 +Priority=1000 +OverrideBuildCmd=0 +BuildCmd= + +[Unit39] +FileName=prune_theorems.c +CompileCpp=0 +Folder=Scyther +Compile=1 +Link=1 +Priority=1000 +OverrideBuildCmd=0 +BuildCmd= + +[Unit40] +FileName=prune_theorems.h +CompileCpp=0 +Folder=Scyther +Compile=1 +Link=1 +Priority=1000 +OverrideBuildCmd=0 +BuildCmd= + +[Unit41] +FileName=role.c +CompileCpp=0 +Folder=Scyther +Compile=1 +Link=1 +Priority=1000 +OverrideBuildCmd=0 +BuildCmd= + +[Unit42] +FileName=role.h +CompileCpp=0 +Folder=Scyther +Compile=1 +Link=1 +Priority=1000 +OverrideBuildCmd=0 +BuildCmd= + +[Unit43] +FileName=specialterm.c +CompileCpp=0 +Folder=Scyther +Compile=1 +Link=1 +Priority=1000 +OverrideBuildCmd=0 +BuildCmd= + +[Unit44] +FileName=specialterm.h +CompileCpp=0 +Folder=Scyther +Compile=1 +Link=1 +Priority=1000 +OverrideBuildCmd=0 +BuildCmd= + +[Unit45] +FileName=states.c +CompileCpp=0 +Folder=Scyther +Compile=1 +Link=1 +Priority=1000 +OverrideBuildCmd=0 +BuildCmd= + +[Unit46] +FileName=states.h +CompileCpp=0 +Folder=Scyther +Compile=1 +Link=1 +Priority=1000 +OverrideBuildCmd=0 +BuildCmd= + +[Unit48] +FileName=switches.h +CompileCpp=0 +Folder=Scyther +Compile=1 +Link=1 +Priority=1000 +OverrideBuildCmd=0 +BuildCmd= + +[Unit49] +FileName=symbol.c +CompileCpp=0 +Folder=Scyther +Compile=1 +Link=1 +Priority=1000 +OverrideBuildCmd=0 +BuildCmd= + +[Unit50] +FileName=symbol.h +CompileCpp=0 +Folder=Scyther +Compile=1 +Link=1 +Priority=1000 +OverrideBuildCmd=0 +BuildCmd= + +[Unit51] +FileName=system.c +CompileCpp=0 +Folder=Scyther +Compile=1 +Link=1 +Priority=1000 +OverrideBuildCmd=0 +BuildCmd= + +[Unit52] +FileName=system.h +CompileCpp=0 +Folder=Scyther +Compile=1 +Link=1 +Priority=1000 +OverrideBuildCmd=0 +BuildCmd= + +[Unit53] +FileName=tac.c +CompileCpp=0 +Folder=Scyther +Compile=1 +Link=1 +Priority=1000 +OverrideBuildCmd=0 +BuildCmd= + +[Unit54] +FileName=tac.h +CompileCpp=0 +Folder=Scyther +Compile=1 +Link=1 +Priority=1000 +OverrideBuildCmd=0 +BuildCmd= + +[Unit55] +FileName=term.c +CompileCpp=0 +Folder=Scyther +Compile=1 +Link=1 +Priority=1000 +OverrideBuildCmd=0 +BuildCmd= + +[Unit56] +FileName=term.h +CompileCpp=0 +Folder=Scyther +Compile=1 +Link=1 +Priority=1000 +OverrideBuildCmd=0 +BuildCmd= + +[Unit57] +FileName=termlist.c +CompileCpp=0 +Folder=Scyther +Compile=1 +Link=1 +Priority=1000 +OverrideBuildCmd=0 +BuildCmd= + +[Unit58] +FileName=termlist.h +CompileCpp=0 +Folder=Scyther +Compile=1 +Link=1 +Priority=1000 +OverrideBuildCmd=0 +BuildCmd= + +[Unit59] +FileName=termmap.c +CompileCpp=0 +Folder=Scyther +Compile=1 +Link=1 +Priority=1000 +OverrideBuildCmd=0 +BuildCmd= + +[Unit60] +FileName=termmap.h +CompileCpp=0 +Folder=Scyther +Compile=1 +Link=1 +Priority=1000 +OverrideBuildCmd=0 +BuildCmd= + +[Unit61] +FileName=timer.c +CompileCpp=0 +Folder=Scyther +Compile=1 +Link=1 +Priority=1000 +OverrideBuildCmd=0 +BuildCmd= + +[Unit62] +FileName=timer.h +CompileCpp=0 +Folder=Scyther +Compile=1 +Link=1 +Priority=1000 +OverrideBuildCmd=0 +BuildCmd= + +[Unit63] +FileName=type.c +CompileCpp=0 +Folder=Scyther +Compile=1 +Link=1 +Priority=1000 +OverrideBuildCmd=0 +BuildCmd= + +[Unit64] +FileName=type.h +CompileCpp=0 +Folder=Scyther +Compile=1 +Link=1 +Priority=1000 +OverrideBuildCmd=0 +BuildCmd= + +[Unit65] +FileName=warshall.c +CompileCpp=0 +Folder=Scyther +Compile=1 +Link=1 +Priority=1000 +OverrideBuildCmd=0 +BuildCmd= + +[Unit66] +FileName=warshall.h +CompileCpp=0 +Folder=Scyther +Compile=1 +Link=1 +Priority=1000 +OverrideBuildCmd=0 +BuildCmd= + +[Unit67] +FileName=xmlout.c +CompileCpp=0 +Folder=Scyther +Compile=1 +Link=1 +Priority=1000 +OverrideBuildCmd=0 +BuildCmd= + +[Unit68] +FileName=main.c +CompileCpp=0 +Folder=Scyther +Compile=1 +Link=1 +Priority=1000 +OverrideBuildCmd=0 +BuildCmd= + +[Unit69] +FileName=version.h +CompileCpp=0 +Folder= +Compile=1 +Link=1 +Priority=1000 +OverrideBuildCmd=0 +BuildCmd= + +[Unit70] +FileName=parser.h +CompileCpp=0 +Folder=Scyther +Compile=1 +Link=1 +Priority=1000 +OverrideBuildCmd=0 +BuildCmd= + +[Unit71] +FileName=scanner.c +CompileCpp=0 +Folder=Scyther +Compile=1 +Link=1 +Priority=1000 +OverrideBuildCmd=0 +BuildCmd= + +[VersionInfo] +Major=0 +Minor=1 +Release=1 +Build=1 +LanguageID=1033 +CharsetID=1252 +CompanyName= +FileVersion= +FileDescription=Developed using the Dev-C++ IDE +InternalName= +LegalCopyright= +LegalTrademarks= +OriginalFilename= +ProductName= +ProductVersion= +AutoIncBuildNr=0 + +[Unit34] +FileName=mgu.c +CompileCpp=0 +Folder=Scyther +Compile=1 +Link=1 +Priority=1000 +OverrideBuildCmd=0 +BuildCmd= + +[Unit72] +FileName=parser.c +CompileCpp=0 +Folder=Scyther +Compile=1 +Link=1 +Priority=1000 +OverrideBuildCmd=0 +BuildCmd= + +[Unit73] +FileName=scanner.c +CompileCpp=0 +Folder=Scyther +Compile=1 +Link=1 +Priority=1000 +OverrideBuildCmd=0 +BuildCmd= + +[Unit74] +FileName=parser.c +CompileCpp=0 +Folder=Scyther +Compile=1 +Link=1 +Priority=1000 +OverrideBuildCmd=0 +BuildCmd= + +[Unit47] +FileName=switches.c +CompileCpp=0 +Folder=Scyther +Compile=1 +Link=1 +Priority=1000 +OverrideBuildCmd=0 +BuildCmd= + diff --git a/gui/src/UniversalBinary.cmake b/gui/src/UniversalBinary.cmake new file mode 100644 index 0000000..1dd17d2 --- /dev/null +++ b/gui/src/UniversalBinary.cmake @@ -0,0 +1,42 @@ +################################################################ +# Name: UniversalBinary.cmake +# Purpose: Add target to make a Mac universal binary +# Needs pre-build mac versions first! +# Author: Cas Cremers +################################################################ + +find_program(lipoexecutable lipo) +if (lipoexecutable) + # Check whether we already have the binaries + set (UBrequiredfiles FALSE) + set (ppcfile "scyther-macppc") + set (intelfile "scyther-macintel") + if (EXISTS "${ppcfile}") + if (EXISTS "${intelfile}") + set (UBrequiredfiles TRUE) + else (EXISTS "${intelfile}") + message (STATUS "Could not find scyther-macintel.") + endif (EXISTS "${intelfile}") + else (EXISTS "${ppcfile}") + message (STATUS "Could not find scyther-macppc.") + endif (EXISTS "${ppcfile}") + + # Use information to proceed + if (UBrequiredfiles) + message (STATUS "Adding target for Mac universal binary") + add_custom_target (scyther-mac + COMMAND lipo -create "${ppcfile}" "${intelfile}" -output scyther-mac + COMMENT "Generating Mac universal binary" + DEPENDS scyther-macintel + DEPENDS scyther-macppc + ) + else (UBrequiredfiles) + message (STATUS "No universal binary possible yet. Please do the following:") + message (STATUS " cmake -DTARGETOS=MacPPC . && make") + message (STATUS " cmake -DTARGETOS=MacIntel . && make") + message (STATUS " cmake . && make scyther-mac") + endif (UBrequiredfiles) +else (lipoexecutable) + message (FATAL_ERROR "Cannot find the 'lipo' program that is required for creating universal binaries") +endif (lipoexecutable) + diff --git a/gui/src/arachne.c b/gui/src/arachne.c new file mode 100644 index 0000000..7b98005 --- /dev/null +++ b/gui/src/arachne.c @@ -0,0 +1,2582 @@ +/** + * + *@file arachne.c + * + * Introduces a method for proofs akin to the Athena modelchecker + * http://www.ece.cmu.edu/~dawnsong/athena/ + * + */ + +#include +#include +#include +#include +#if !defined(__APPLE__) +#ifdef DEBUG +#include +#endif +#endif + +#include "term.h" +#include "termlist.h" +#include "role.h" +#include "system.h" +#include "knowledge.h" +#include "compiler.h" +#include "states.h" +#include "mgu.h" +#include "arachne.h" +#include "error.h" +#include "claim.h" +#include "debug.h" +#include "binding.h" +#include "warshall.h" +#include "timer.h" +#include "type.h" +#include "switches.h" +#include "specialterm.h" +#include "cost.h" +#include "dotout.h" +#include "prune_bounds.h" +#include "prune_theorems.h" +#include "arachne.h" +#include "hidelevel.h" +#include "depend.h" +#include "xmlout.h" +#include "heuristic.h" + +extern int *graph; +extern int nodes; +extern int graph_uordblks; + +static System sys; //!< local buffer for the system pointer + +int attack_length; //!< length of the attack +int attack_leastcost; //!< cost of the best attack sofar \sa cost.c + +Protocol INTRUDER; //!< intruder protocol +Role I_M; //!< Initial knowledge role of the intruder +Role I_RRS; //!< Encrypt role of the intruder +Role I_RRSD; //!< Decrypt role of the intruder + +int proofDepth; //!< Current depth of the proof +int max_encryption_level; //!< Maximum encryption level of any term + +static int indentDepth; +static int prevIndentDepth; +static int indentDepthChanges; +static FILE *attack_stream; + +/* + * Forward declarations + */ + +int iterate (); + +/* + * Program code + */ + +//! Init Arachne engine +void +arachneInit (const System mysys) +{ + Roledef rd; + + void add_event (int event, Term message) + { + rd = roledefAdd (rd, event, NULL, NULL, NULL, message, NULL); + } + + Role add_role (const char *rolenamestring) + { + Role r; + Term rolename; + + rolename = makeGlobalConstant (rolenamestring); + r = roleCreate (rolename); + r->roledef = rd; + rd = NULL; + r->next = INTRUDER->roles; + INTRUDER->roles = r; + // compute_role_variables (sys, INTRUDER, r); + return r; + } + + sys = mysys; // make sys available for this module as a global + + /** + * Very important: turn role terms that are local to a run, into variables. + */ + term_rolelocals_are_variables (); + + /* + * Add intruder protocol roles + */ + + INTRUDER = protocolCreate (makeGlobalConstant (" INTRUDER ")); + + // Initially empty roledef + rd = NULL; + + add_event (SEND, NULL); + I_M = add_role ("I_M: Atomic message"); + + add_event (READ, NULL); + add_event (READ, NULL); + add_event (SEND, NULL); + I_RRS = add_role ("I_E: Encrypt"); + + add_event (READ, NULL); + add_event (READ, NULL); + add_event (SEND, NULL); + I_RRSD = add_role ("I_D: Decrypt"); + + sys->num_regular_runs = 0; + sys->num_intruder_runs = 0; + max_encryption_level = 0; + + indentDepth = 0; + prevIndentDepth = 0; + indentDepthChanges = 0; + + return; +} + +//! Close Arachne engine +void +arachneDone () +{ + return; +} + +//------------------------------------------------------------------------ +// Detail +//------------------------------------------------------------------------ + +//! Just a defined integer for invalid +#define INVALID -1 +//! can this roledef constitute a read Goal? +#define isGoal(rd) (rd->type == READ && !rd->internal) +//! is this roledef already bound? +#define isBound(rd) (rd->bound) + +//! Indent prefix print +void +indentPrefixPrint (const int annotate, const int jumps) +{ + void counterPrint () + { + statesFormat (sys->current_claim->states); + eprintf ("\t"); + eprintf ("%i", annotate); + eprintf ("\t"); + } + + if (switches.output == ATTACK && globalError == 0) + { + // Arachne, attack, not an error + // We assume that means DOT output + eprintf ("// "); + counterPrint (); + } + else + { + // If it is not to stdout, or it is not an attack... + int i; + + counterPrint (); + for (i = 0; i < jumps; i++) + { + if (i % 3 == 0) + eprintf ("|"); + else + eprintf (" "); + eprintf (" "); + } + } +} + +//! Indent print +/** + * More subtle than before. Indentlevel changes now cause a counter to be increased, which is printed. Nice to find stuff in attacks. + */ +void +indentPrint () +{ + if (indentDepth != prevIndentDepth) + { + indentDepthChanges++; + while (indentDepth != prevIndentDepth) + { + if (prevIndentDepth < indentDepth) + { + indentPrefixPrint (indentDepthChanges, prevIndentDepth); + eprintf ("{\n"); + prevIndentDepth++; + } + else + { + prevIndentDepth--; + indentPrefixPrint (indentDepthChanges, prevIndentDepth); + eprintf ("}\n"); + } + } + } + indentPrefixPrint (indentDepthChanges, indentDepth); +} + +//! Print indented binding +void +binding_indent_print (const Binding b, const int flag) +{ + indentPrint (); + if (flag) + eprintf ("!! "); + binding_print (b); + eprintf ("\n"); +} + +//! Keylevel tester: can this term ever be sent at this keylevel? +int +isKeylevelRight (Term t, const int kl) +{ + t = deVar (t); + if (realTermLeaf (t)) + { + // Leaf + if (isTermVariable (t)) + { + // Variables are okay + return 1; + } + else + { + // Constant, does it have a keylevel? + int mykl; + + mykl = TermSymb (t)->keylevel; + if (mykl < INT_MAX) + { + // Sensible keylevel, so it must be possible + return (mykl <= kl); + } + else + { + // Never sent? + // So we can not expect it to come from that + return 0; + } + } + } + else + { + // Node + if (realTermTuple (t)) + { + // Tuple + return isKeylevelRight (TermOp1 (t), kl) + && isKeylevelRight (TermOp2 (t), kl); + } + else + { + // Crypt + return isKeylevelRight (TermOp1 (t), kl) + && isKeylevelRight (TermOp2 (t), kl + 1); + } + } +} + +//! Keylevel tester: can this term ever be sent at this keylevel? +/** + * Depends on the keylevel lemma (so this will not be called when those lemmas + * are disabled) and the keylevel constructors in symbol.c The idea is that + * certain terms will never be sent. + */ +int +isPossiblySent (Term t) +{ + return isKeylevelRight (t, 0); +} + +//! Wrapper for roleInstance +/** + *@return Returns the run number + */ +int +semiRunCreate (const Protocol p, const Role r) +{ + int run; + + if (p == INTRUDER) + sys->num_intruder_runs++; + else + sys->num_regular_runs++; +#ifdef DEBUG + if (DEBUGL (5)) + { + globalError++; + eprintf ("Adding a run %i with semiRunCreate, ", sys->maxruns); + termPrint (p->nameterm); + eprintf (", "); + termPrint (r->nameterm); + eprintf ("\n"); + globalError--; + } +#endif + roleInstance (sys, p, r, NULL, NULL); + run = sys->maxruns - 1; + sys->runs[run].height = 0; + return run; +} + +//! Wrapper for roleDestroy +void +semiRunDestroy () +{ + if (sys->maxruns > 0) + { + Protocol p; + + p = sys->runs[sys->maxruns - 1].protocol; + roleInstanceDestroy (sys); + if (p == INTRUDER) + sys->num_intruder_runs--; + else + sys->num_regular_runs--; + } +} + +//! Fix the keylevels of any agents +/** + * We simply extract the agent names from m0 (ugly hack) + */ +void +fixAgentKeylevels (void) +{ + Termlist tl, m0tl; + + m0tl = knowledgeSet (sys->know); + tl = m0tl; + while (tl != NULL) + { + Term t; + + t = deVar (tl->term); + if (realTermLeaf (t)) + { + { + // a real agent type thing + if (TermSymb (t)->keylevel == INT_MAX) + { + // Fix the keylevel + TermSymb (t)->keylevel = 0; + } + } + } + tl = tl->next; + } + termlistDelete (m0tl); +} + + +//! After a role instance, or an extension of a run, we might need to add some goals +/** + * From old to new. Sets the new height to new. + *@returns The number of goals added (for destructions) + */ +int +add_read_goals (const int run, const int old, const int new) +{ + if (new <= sys->runs[run].height) + { + return 0; + } + else + { + int count; + int i; + Roledef rd; + + sys->runs[run].height = new; + i = old; + rd = eventRoledef (sys, run, i); + count = 0; + while (i < new && rd != NULL) + { + if (rd->type == READ) + { + if (switches.output == PROOF) + { + if (count == 0) + { + indentPrint (); + eprintf ("Thus, we must also produce "); + } + else + { + eprintf (", "); + } + termPrint (rd->message); + } + count = count + goal_add (rd->message, run, i, 0); + } + rd = rd->next; + i++; + } + if ((count > 0) && switches.output == PROOF) + { + eprintf ("\n"); + } + return count; + } +} + +//! Determine trace length +int +get_semitrace_length () +{ + int run; + int length; + + run = 0; + length = 0; + while (run < sys->maxruns) + { + if (sys->runs[run].protocol != INTRUDER) + { + // Non-intruder run: count length + // Subtract 'firstReal' to ignore chooses. + length = length + sys->runs[run].height - sys->runs[run].firstReal; + } + run++; + } + return length; +} + +//! Count intruder events +int +countIntruderActions () +{ + int count; + int run; + + count = 0; + run = 0; + while (run < sys->maxruns) + { + if (sys->runs[run].protocol == INTRUDER) + { + // Only intruder roles + if (sys->runs[run].role != I_M) + { + // The M_0 (initial knowledge) events don't count. + count++; + } + } + run++; + } + return count; +} + +//------------------------------------------------------------------------ +// Proof reporting +//------------------------------------------------------------------------ + +//! Protocol/role name of a run +void +role_name_print (const int run) +{ + eprintf ("protocol "); + termPrint (sys->runs[run].protocol->nameterm); + eprintf (", role "); + termPrint (sys->runs[run].role->nameterm); +} + +//! Adding a run/extending a run +void +proof_suppose_run (const int run, const int oldlength, const int newlength) +{ + if (switches.output == PROOF) + { + int reallength; + + indentPrint (); + eprintf ("Suppose "); + if (oldlength == 0) + eprintf ("there is a "); + else + eprintf ("we extend "); + reallength = roledef_length (sys->runs[run].start); + if (reallength > newlength) + eprintf ("semi-"); + eprintf ("run #%i of ", run); + role_name_print (run); + if (reallength > newlength) + { + if (oldlength == 0) + eprintf (" of"); + else + eprintf (" to"); + eprintf (" length %i", newlength); + } + eprintf ("\n"); + } +} + +//! Select a goal +void +proof_select_goal (Binding b) +{ + if (switches.output == PROOF) + { + Roledef rd; + + rd = roledef_shift (sys->runs[b->run_to].start, b->ev_to); + indentPrint (); + eprintf ("Selected goal: Where does term "); + termPrint (b->term); + eprintf (" occur first as an interm?\n"); + indentPrint (); + eprintf ("* It is required for "); + roledefPrint (rd); + eprintf (" at index %i in run %i\n", b->ev_to, b->run_to); + } +} + +//! Cannot bind because of cycle +void +proof_cannot_bind (const Binding b, const int run, const int index) +{ + if (switches.output == PROOF) + { + indentPrint (); + eprintf + ("Cannot bind this to run %i, index %i because that introduces a cycle.\n", + run, index); + } +} + +//! Test a binding +void +proof_suppose_binding (Binding b) +{ + if (switches.output == PROOF) + { + Roledef rd; + + indentPrint (); + rd = roledef_shift (sys->runs[b->run_from].start, b->ev_from); + eprintf ("Suppose it originates in run %i, at index %i\n", b->run_from, + b->ev_from); + indentPrint (); + eprintf ("* I.e. event "); + roledefPrint (rd); + eprintf ("\n"); + indentPrint (); + eprintf ("* from "); + role_name_print (b->run_from); + eprintf ("\n"); + } +} + +//! Create a new temporary file and return the pointer. +FILE * +scyther_tempfile (void) +{ + return tmpfile (); +} + +//------------------------------------------------------------------------ +// Sub +//------------------------------------------------------------------------ + +//! Iterate over all events in the roles (including the intruder ones) +/** + * Function is called with (protocol pointer, role pointer, roledef pointer, index) + * and returns an integer. If it is false, iteration aborts. + */ +int +iterate_role_events (int (*func) ()) +{ + Protocol p; + + p = sys->protocols; + while (p != NULL) + { + Role r; + + r = p->roles; + while (r != NULL) + { + Roledef rd; + int index; + + rd = r->roledef; + index = 0; + while (rd != NULL) + { + if (!func (p, r, rd, index)) + return 0; + index++; + rd = rd->next; + } + r = r->next; + } + p = p->next; + } + return 1; +} + +//! Iterate over all send types in the roles (including the intruder ones) +/** + * Function is called with (protocol pointer, role pointer, roledef pointer, index) + * and returns an integer. If it is false, iteration aborts. + */ +int +iterate_role_sends (int (*func) ()) +{ + int send_wrapper (Protocol p, Role r, Roledef rd, int i) + { + if (rd->type == SEND) + { + return func (p, r, rd, i); + } + else + { + return 1; + } + } + + return iterate_role_events (send_wrapper); +} + +//! Create decryption role instance +/** + * Note that this does not add any bindings for the reads. + * + *@param term The term to be decrypted (implies decryption key) + *@param key The key that is needed to decrypt the term + * + *@returns The run id of the decryptor instance + */ +int +create_decryptor (const Term term, const Term key) +{ + if (term != NULL && isTermEncrypt (term)) + { + Roledef rd; + int run; + +#ifdef DEBUG + if (DEBUGL (5)) + { + globalError++; + eprintf ("Creating decryptor for term "); + termPrint (term); + eprintf (" and key "); + termPrint (key); + eprintf ("\n"); + globalError--; + } +#endif + + run = semiRunCreate (INTRUDER, I_RRSD); + rd = sys->runs[run].start; + rd->message = termDuplicateUV (term); + rd->next->message = termDuplicateUV (key); + rd->next->next->message = termDuplicateUV (TermOp (term)); + sys->runs[run].height = 3; + proof_suppose_run (run, 0, 3); + + return run; + } + + globalError++; + eprintf ("Term for which a decryptor instance is requested: "); + termPrint (term); + eprintf ("\n"); + error ("Trying to build a decryptor instance for a non-encrypted term."); + return -1; +} + +//! Get the priority level of a key that is needed for a term (typical pk/sk distinction) +int +getPriorityOfNeededKey (const System sys, const Term keyneeded) +{ + int prioritylevel; + + /* Normally, a key gets higher priority, but unfortunately this is not propagated at the moment. Maybe later. + */ + prioritylevel = 1; + if (realTermEncrypt (keyneeded)) + { + /* the key is a construction itself */ + if (inKnowledge (sys->know, TermKey (keyneeded))) + { + /* the key is constructed by a public thing */ + /* typically, this is a public key, so we postpone it */ + prioritylevel = -1; + } + } + return prioritylevel; +} + +//! Report failed binding +void +report_failed_binding (Binding b, int run, int index) +{ + if (switches.output == PROOF) + { + indentPrint (); + eprintf ("Failed to bind the binding at r%ii%i with term ", b->run_to, + b->ev_to); + termPrint (b->term); + eprintf (" to the source r%ii%i because of orderings.\n", run, index); +#ifdef DEBUG + if (DEBUGL (5)) + { + dependPrint (); + } +#endif + } +} + +//! Make a decryption chain from a binding to some run,index using the key list, and callback if this works. +/** + * The key goals are bound to the goal, and then we iterate on that. + * + *@param b binding to fix (bind), destination filled in + *@param run run of binding start + *@param index index in run of binding start + * Callback return value is int, but is effectively ignored. + */ +void +createDecryptionChain (const Binding b, const int run, const int index, + Termlist keylist, int (*callback) (void)) +{ + if (keylist == NULL) + { + // Immediate binding, no key needed. + if (goal_bind (b, run, index)) + { + callback (); + goal_unbind (b); + return; + } + else + { + report_failed_binding (b, run, index); + } + } + else + { + Term tdecr, tkey; + int smallrun; + + // Some decryptor is needed for the term in the list + + indentDepth++; + + tdecr = keylist->term; + tkey = inverseKey (sys->know->inverses, TermKey (tdecr)); + smallrun = create_decryptor (tdecr, tkey); + { + Roledef rddecrypt; + Binding bnew; + int newgoals; + int prioritylevel; + + /* + * 2. Add goal bindings + */ + + rddecrypt = sys->runs[smallrun].start; + // Add goal for tdecr copy + newgoals = goal_add (rddecrypt->message, smallrun, 0, 0); + if (newgoals != 1) + { + error + ("Added %i goals (instead of one) for decryptor goal 1, weird.", + newgoals); + } + + // This is the unique new goal + bnew = (Binding) sys->bindings->data; + + // Add goal for needed key copy + prioritylevel = getPriorityOfNeededKey (sys, tkey); + newgoals += goal_add (rddecrypt->next->message, smallrun, 1, + prioritylevel); + + if (switches.output == PROOF) + { + indentPrint (); + eprintf + ("This introduces the obligation to decrypt the following subterm: "); + termPrint (tdecr); + eprintf (" to be decrypted using "); + termPrint (tkey); + eprintf ("\n"); + + indentPrint (); + eprintf + ("To this end, we added two new goals and one new send: "); + termPrint (rddecrypt->message); + eprintf (","); + termPrint (rddecrypt->next->message); + eprintf (","); + termPrint (rddecrypt->next->next->message); + eprintf ("\n"); + } + + /* + * 3. Bind open goal to decryptor? + */ + if (goal_bind (b, smallrun, 2)) + { + if (switches.output == PROOF) + { + indentPrint (); + eprintf ("Bound "); + termPrint (b->term); + eprintf (" to r%ii%i: trying new createDecryptionChain.\n", + smallrun, 2); + } + + // Iterate with the new goal + createDecryptionChain (bnew, run, index, keylist->next, callback); + goal_unbind (b); + } + else + { + report_failed_binding (b, smallrun, 2); + } + /* + * clean up + */ + goal_remove_last (newgoals); + } + semiRunDestroy (); + termDelete (tkey); + + indentDepth--; + } +} + + +//! Try to bind a specific existing run to a goal. +/** + * The idea is that we try to bind it this specific run and index. If this + * requires keys, then we should add such goals as well with the required + * decryptor things. + * + * The 'newdecr' boolean signals the addition of decryptors. If it is false, we should not add any. + * + * The key goals are bound to the goal. Iterates on success. + */ +void +bind_existing_to_goal (const Binding b, const int run, const int index, + int newdecr) +{ + Term bigterm; + + int unifiesWithKeys (Termlist substlist, Termlist keylist) + { + int old_length; + int newgoals; + + // TODO this is a hack: in this case we really should not use subterm + // unification but interm instead. However, this effectively does the same + // by avoiding branches that get immediately pruned anyway. + if (!newdecr && keylist != NULL) + { + return true; + } + // We need some adapting because the height would increase; we therefore + // have to add read goals before we know whether it unifies. + old_length = sys->runs[run].height; + newgoals = add_read_goals (run, old_length, index + 1); + + { + // wrap substitution lists + + void wrapSubst (Termlist sl) + { + if (sl == NULL) + { + if (switches.output == PROOF) + { + Roledef rd; + + indentPrint (); + eprintf ("Suppose "); + termPrint (b->term); + eprintf (" originates first at run %i, event %i, as part of ", + run, index); + rd = roledef_shift (sys->runs[run].start, index); + termPrint (rd->message); + eprintf ("\n"); + } + // new create key goals, bind etc. + createDecryptionChain (b, run, index, keylist, iterate); + } + else + { + int neworders; + int allgood; + Term tvar; + + // the idea is, that a substitution in run x with + // something containing should be wrapped; this + // occurs for all subterms of other runs. + int makeDepend (Term tsmall) + { + Term tsubst; + + tsubst = deVar (tsmall); + if (!realTermVariable (tsubst)) + { + // Only for non-variables (i.e. local constants) + int r1, e1; + + r1 = TermRunid (tsubst); + e1 = firstOccurrence (sys, r1, tsubst, SEND); + if (e1 >= 0) + { + int r2, e2; + + r2 = TermRunid (tvar); + e2 = firstOccurrence (sys, r2, tsubst, READ); + if (e2 >= 0) + { + + if (dependPushEvent (r1, e1, r2, e2)) + { + neworders++; + return true; + } + else + { + allgood = false; + if (switches.output == PROOF) + { + indentPrint (); + eprintf ("Substitution for "); + termSubstPrint (sl->term); + eprintf (" (subterm "); + termPrint (tsmall); + eprintf (") could not be safely bound.\n"); + } + return false; + } + } + } + } + return true; + } + + neworders = 0; + allgood = true; + tvar = sl->term; + iterateTermOther (run, tvar, makeDepend); + if (allgood) + { + wrapSubst (sl->next); + } + while (neworders > 0) + { + neworders--; + dependPopEvent (); + } + } + } + + wrapSubst (substlist); + } + + // undo + goal_remove_last (newgoals); + sys->runs[run].height = old_length; + return true; + } + + bigterm = roledef_shift (sys->runs[run].start, index)->message; + subtermUnify (bigterm, b->term, NULL, NULL, unifiesWithKeys); +} + + + + +//! Bind a goal to an existing regular run, if possible, by adding decr events +int +bind_existing_run (const Binding b, const Protocol p, const Role r, + const int index) +{ + int run, flag; + int found; + + flag = 1; + found = 0; + for (run = 0; run < sys->maxruns; run++) + { + if (sys->runs[run].protocol == p && sys->runs[run].role == r) + { + found++; + if (switches.output == PROOF) + { + if (found == 1) + { + indentPrint (); + eprintf ("Can we bind it to an existing regular run of "); + termPrint (p->nameterm); + eprintf (", "); + termPrint (r->nameterm); + eprintf ("?\n"); + } + indentPrint (); + eprintf ("%i. Can we bind it to run %i?\n", found, run); + } + indentDepth++; + bind_existing_to_goal (b, run, index, true); + indentDepth--; + } + } + if (switches.output == PROOF && found == 0) + { + indentPrint (); + eprintf ("There is no existing run for "); + termPrint (p->nameterm); + eprintf (", "); + termPrint (r->nameterm); + eprintf ("\n"); + } + return flag; +} + +//! Bind a goal to a new run, possibly adding decr events +int +bind_new_run (const Binding b, const Protocol p, const Role r, + const int index) +{ + int run; + + run = semiRunCreate (p, r); + proof_suppose_run (run, 0, index + 1); + { + int newgoals; + + newgoals = add_read_goals (run, 0, index + 1); + indentDepth++; + bind_existing_to_goal (b, run, index, true); + indentDepth--; + goal_remove_last (newgoals); + } + semiRunDestroy (); + return true; +} + +//! Print the current semistate +void +printSemiState () +{ + int run; + int open; + + int binding_state_print (void *dt) + { + binding_indent_print ((Binding) dt, 1); + return 1; + } + + indentPrint (); + eprintf ("!! --=[ Semistate ]=--\n"); + indentPrint (); + eprintf ("!!\n"); + indentPrint (); + eprintf ("!! Trace length: %i\n", get_semitrace_length ()); + open = 0; + for (run = 0; run < sys->maxruns; run++) + { + int index; + Role r; + Roledef rd; + Term oldagent; + + indentPrint (); + eprintf ("!!\n"); + indentPrint (); + eprintf ("!! [ Run %i, ", run); + termPrint (sys->runs[run].protocol->nameterm); + eprintf (", "); + r = sys->runs[run].role; + oldagent = r->nameterm->subst; + r->nameterm->subst = NULL; + termPrint (r->nameterm); + r->nameterm->subst = oldagent; + if (oldagent != NULL) + { + eprintf (": "); + termPrint (oldagent); + } + eprintf (" ]\n"); + + index = 0; + rd = sys->runs[run].start; + while (index < sys->runs[run].height) + { + indentPrint (); + eprintf ("!! %i ", index); + roledefPrint (rd); + eprintf ("\n"); + if (isGoal (rd) && !isBound (rd)) + open++; + index++; + rd = rd->next; + } + } + if (sys->bindings != NULL) + { + indentPrint (); + eprintf ("!!\n"); + list_iterate (sys->bindings, binding_state_print); + } + indentPrint (); + eprintf ("!!\n"); + indentPrint (); + eprintf ("!! - open: %i -\n", open); +} + +//! Check if a binding duplicates an old one: if so, simply connect +/** + * If it returns true, it has bound the b_new binding, which we must unbind later. + */ +int +bind_old_goal (const Binding b_new) +{ + if (!b_new->done) + { + List bl; + + bl = sys->bindings; + while (bl != NULL) + { + Binding b_old; + + b_old = (Binding) bl->data; + if (b_old->done && isTermEqual (b_new->term, b_old->term)) + { + // Old is done and has the same term! + // So we try to copy this binding, and fix it. + if (goal_bind (b_new, b_old->run_from, b_old->ev_from)) + { + return true; + } + } + bl = bl->next; + } + } + // No old binding to connect to + return false; +} + +//! Create a new intruder run to generate knowledge from m0 +int +bind_goal_new_m0 (const Binding b) +{ + Termlist m0tl, tl; + int flag; + int found; + + + flag = 1; + found = 0; + m0tl = knowledgeSet (sys->know); + tl = m0tl; + while (flag && tl != NULL) + { + Term m0t; + Termlist subst; + + m0t = tl->term; + subst = termMguTerm (b->term, m0t); //! @todo This needs to be replace by the iterator one, but works for now + if (subst != MGUFAIL) + { + int run; + + I_M->roledef->message = m0t; + run = semiRunCreate (INTRUDER, I_M); + proof_suppose_run (run, 0, 1); + sys->runs[run].height = 1; + { + indentDepth++; + if (goal_bind (b, run, 0)) + { + found++; + proof_suppose_binding (b); + if (switches.output == PROOF) + { + indentPrint (); + eprintf ("* I.e. retrieving "); + termPrint (b->term); + eprintf (" from the initial knowledge.\n"); + } + + { + // Now we also want to add bindings to have this run before all other runs + void wrapRunOrders (const int otherrun) + { + if (otherrun < 0) + { + // No more runs to do + flag = flag && iterate (); + } + else + { + if (otherrun != run) + { + if (dependPushEvent (run, 0, otherrun, 0)) + { + wrapRunOrders (otherrun - 1); + dependPopEvent (); + } + } + else + { + wrapRunOrders (otherrun - 1); + } + } + } + + wrapRunOrders (sys->maxruns - 1); + } + + goal_unbind (b); + } + else + { + proof_cannot_bind (b, run, 0); + } + indentDepth--; + } + semiRunDestroy (); + + + termlistSubstReset (subst); + termlistDelete (subst); + } + + tl = tl->next; + } + + if (found == 0 && switches.output == PROOF) + { + indentPrint (); + eprintf ("Term "); + termPrint (b->term); + eprintf (" cannot be constructed from the initial knowledge.\n"); + } + termlistDelete (m0tl); + + + return flag; +} + +//! Bind an intruder goal by intruder composition construction +/** + * Handles the case where the intruder constructs a composed term himself. + */ +int +bind_goal_new_encrypt (const Binding b) +{ + Term term; + int flag; + int can_be_encrypted; + + + flag = 1; + term = deVar (b->term); + can_be_encrypted = 0; + + if (!realTermLeaf (term)) + { + Term t1, t2; + + if (switches.intruder && (!realTermEncrypt (term))) + { + // tuple construction + error ("Goal that is a tuple should not occur!"); + } + + // must be encryption + t1 = TermOp (term); + t2 = TermKey (term); + + if (t2 != TERM_Hidden) + { + int run; + + can_be_encrypted = 1; + run = semiRunCreate (INTRUDER, I_RRS); + { + int index; + Roledef rd; + + rd = sys->runs[run].start; + rd->message = termDuplicateUV (t1); + rd->next->message = termDuplicateUV (t2); + rd->next->next->message = termDuplicateUV (term); + index = 2; + proof_suppose_run (run, 0, index + 1); + if (switches.output == PROOF) + { + indentPrint (); + eprintf ("* Encrypting "); + termPrint (term); + eprintf (" using term "); + termPrint (t1); + eprintf (" and key "); + termPrint (t2); + eprintf ("\n"); + } + + { + int newgoals; + newgoals = add_read_goals (run, 0, index + 1); + { + + indentDepth++; + if (goal_bind (b, run, index)) + { + proof_suppose_binding (b); + flag = flag && iterate (); + goal_unbind (b); + } + else + { + proof_cannot_bind (b, run, index); + } + indentDepth--; + } + goal_remove_last (newgoals); + } + } + semiRunDestroy (); + } + } + + if (!can_be_encrypted) + { + if (switches.output == PROOF) + { + indentPrint (); + eprintf ("Term "); + termPrint (b->term); + eprintf (" cannot be constructed by encryption.\n"); + } + } + + return flag; +} + +//! Bind an intruder goal by intruder construction +/** + * Handles the case where the intruder constructs a composed term himself, or retrieves it from m0. + * However, it must not already have been created in an intruder run; then it gets bound to that. + */ +int +bind_goal_new_intruder_run (const Binding b) +{ + int flag; + + if (switches.output == PROOF) + { + indentPrint (); + eprintf ("Can we bind "); + termPrint (b->term); + eprintf (" from a new intruder run?\n"); + } + indentDepth++; + //flag = bind_goal_new_m0 (b); + //flag = flag && bind_goal_new_encrypt (b); + flag = bind_goal_new_encrypt (b); + indentDepth--; + return flag; +} + +//! Bind a regular goal +/** + * Problem child. Valgrind does not like it. + */ +int +bind_goal_regular_run (const Binding b) +{ + int flag; + int found; + + /* + * This is a local function so we have access to goal + */ + int bind_this_role_send (Protocol p, Role r, Roledef rd, int index) + { + int test_sub_unification (Termlist substlist, Termlist keylist) + { + // A unification exists; return the signal + return false; + } + + if (p == INTRUDER) + { + // No intruder roles here + return true; + } + + // Test for interm unification +#ifdef DEBUG + if (DEBUGL (5)) + { + indentPrint (); + eprintf ("Checking send candidate with message "); + termPrint (rd->message); + eprintf (" from "); + termPrint (p->nameterm); + eprintf (", "); + termPrint (r->nameterm); + eprintf (", index %i\n", index); + } +#endif + if (!subtermUnify + (rd->message, b->term, NULL, NULL, test_sub_unification)) + { + int sflag; + + // A good candidate + found++; + if (switches.output == PROOF && found == 1) + { + indentPrint (); + eprintf ("The term ", found); + termPrint (b->term); + eprintf + (" matches patterns from the role definitions. Investigate.\n"); + } + if (switches.output == PROOF) + { + indentPrint (); + eprintf ("%i. It matches the pattern ", found); + termPrint (rd->message); + eprintf (" from "); + termPrint (p->nameterm); + eprintf (", "); + termPrint (r->nameterm); + eprintf (", at %i\n", index); + } + indentDepth++; + + // Bind to existing run +#ifdef DEBUG + debug (5, "Trying to bind to existing run."); +#endif + sflag = bind_existing_run (b, p, r, index); + // bind to new run +#ifdef DEBUG + debug (5, "Trying to bind to new run."); +#endif + sflag = sflag && bind_new_run (b, p, r, index); + + indentDepth--; + return sflag; + } + else + { + return true; + } + } + + + // Bind to all possible sends of regular runs + found = 0; + flag = iterate_role_sends (bind_this_role_send); + if (switches.output == PROOF && found == 0) + { + indentPrint (); + eprintf ("The term "); + termPrint (b->term); + eprintf (" does not match any pattern from the role definitions.\n"); + } + return flag; +} + + +//! Bind to all possible sends of intruder runs +int +bind_goal_old_intruder_run (Binding b) +{ + int run; + int flag; + int found; + + found = 0; + flag = 1; + for (run = 0; run < sys->maxruns; run++) + { + if (sys->runs[run].protocol == INTRUDER) + { + int ev; + Roledef rd; + + rd = sys->runs[run].start; + ev = 0; + while (ev < sys->runs[run].height) + { + if (rd->type == SEND) + { + found++; + if (switches.output == PROOF && found == 1) + { + indentPrint (); + eprintf + ("Suppose it is from an existing intruder run.\n"); + } + indentDepth++; + bind_existing_to_goal (b, run, ev, + (sys->runs[run].role != I_RRS)); + indentDepth--; + } + rd = rd->next; + ev++; + } + } + } + if (switches.output == PROOF && found == 0) + { + indentPrint (); + eprintf ("No existing intruder runs to match to.\n"); + } + return flag; +} + +//! Bind a goal in all possible ways +int +bind_goal_all_options (const Binding b) +{ + if (b->blocked) + { + error ("Trying to bind a blocked goal!"); + } + if (!b->done) + { + int flag; + + flag = 1; + proof_select_goal (b); + indentDepth++; + + // Consider a duplicate goal that we already bound before (C-minimality) + // if (1 == 0) + if (bind_old_goal (b)) + { + if (switches.output == PROOF) + { + indentPrint (); + eprintf ("Goal for term "); + termPrint (b->term); + eprintf (" was bound once before, linking up to #%i, %i.\n", + b->run_from, b->ev_from); + } + + flag = flag && iterate (); + + // Unbind again + goal_unbind (b); + indentDepth--; + return flag; + } + else + { + int know_only; + + know_only = false; + + if (1 == 0) // blocked for now + { + // Prune: if it is an SK type construct, ready + // No regular run will apply SK for you. + //!@todo This still needs a lemma, and a more generic (correct) algorithm!! It is currently + // actually false, e.g. for signing protocols, and password-like functions. + // + Term function; + + function = getTermFunction (b->term); + if (function != NULL) + { + if (!inKnowledge (sys->know, function)) + { + // Prune because we didn't know it before, and it is never subterm-sent + if (switches.output == PROOF) + { + indentPrint (); + eprintf ("* Because "); + termPrint (b->term); + eprintf + (" is never sent from a regular run, so we only intruder construct it.\n"); + } + know_only = true; + } + } + } + + if (switches.experimental & 16) + { + // Keylevel lemmas: improves on the previous one + if (!isPossiblySent (b->term)) + { + if (switches.output == PROOF) + { + eprintf + ("Rejecting a term as a regular bind because key levels are off: "); + termPrint (b->term); + if (know_only) + { + eprintf (" [in accordance with function lemma]"); + } + else + { + eprintf (" [stronger than function lemma]"); + } + eprintf ("\n"); + } + know_only = true; + } + } + + if (!(switches.experimental & 32)) + { + /** + * Note: this is slightly weaker than the previous & 16, + * but it actually differs in such minimal cases that it + * might be better to simply have the (much cleaner) + * keylevel lemma. + * + * That's why this is default and the other isn't. + */ + + // Hidelevel variant + int hlf; + + hlf = hidelevelFlag (sys, b->term); + if (hlf == HLFLAG_NONE || hlf == HLFLAG_KNOW) + { + know_only = true; + } + } + + + // Allright, proceed + + proofDepth++; + if (know_only) + { + // Special case: only from intruder + flag = flag && bind_goal_old_intruder_run (b); + //flag = flag && bind_goal_new_intruder_run (b); + } + else + { + // Normal case + { + flag = bind_goal_regular_run (b); + } + flag = flag && bind_goal_old_intruder_run (b); + flag = flag && bind_goal_new_intruder_run (b); + } + proofDepth--; + + indentDepth--; + return flag; + } + } + else + { + return 1; + } +} + +//! Create a generic new term of the same type, with a new run identifier. +/** + * Output: the first element of the returned list. + */ +Termlist +createNewTermGeneric (Termlist tl, Term t) +{ + int freenumber; + Termlist tlscan; + Term newterm; + + /* Determine first free number */ + freenumber = sys->maxruns; + tlscan = tl; + while (tlscan != NULL) + { + Term ts; + + ts = tlscan->term; + if (isLeafNameEqual (t, ts)) + { + if (TermRunid (ts) >= freenumber) + { + freenumber = TermRunid (ts) + 1; + } + } + tlscan = tlscan->next; + } + + /* Make a new term with the free number */ + newterm = (Term) malloc (sizeof (struct term)); + memcpy (newterm, t, sizeof (struct term)); + TermRunid (newterm) = freenumber; + + /* The type of the new term should be that of the parent! */ + newterm->stype = termlistAppend (NULL, t); + + /* return */ + return termlistPrepend (tl, newterm); +} + +//! Construct a list of already used constants +Termlist +findUsedConstants (const System sys) +{ + int run; + Termlist tl; + Termlist tlconst; + + tl = NULL; + tlconst = NULL; + for (run = 0; run < sys->maxruns; run++) + { + tl = termlistAddBasics (tl, sys->runs[run].rho); + tl = termlistAddBasics (tl, sys->runs[run].sigma); + } + while (tl != NULL) + { + Term t; + + t = tl->term; + if (!realTermVariable (t)) + { + tlconst = termlistAddNew (tlconst, t); + } + tl = tl->next; + } + termlistDelete (tl); + return tlconst; +} + +//! Create a new term with incremented run rumber, starting at sys->maxruns. +/** + * This is a rather intricate function that tries to generate new terms of a + * certain type. It first looks up things in the initial knowledge, checking + * whether they are used already. After that, new ones are generated. + * + * Output: the first element of the returned list. + */ +Termlist +createNewTerm (Termlist tl, Term t, int isagent) +{ + /* Does if have an explicit type? + * If so, we try to find a fresh name from the intruder knowledge first. + */ + if (isagent) + { + Termlist knowlist; + Termlist kl; + + knowlist = knowledgeSet (sys->know); + kl = knowlist; + while (kl != NULL) + { + Term k; + + k = kl->term; + if (isAgentType (k->stype)) + { + /* agent */ + /* We don't want to instantiate untrusted agents. */ + if (!inTermlist (sys->untrusted, k)) + { + /* trusted agent */ + if (!inTermlist (tl, k)) + { + /* This agent name is not in the list yet. */ + return termlistPrepend (tl, k); + } + } + } + kl = kl->next; + } + termlistDelete (knowlist); + } + + /* Not an agent or no free one found */ + return createNewTermGeneric (tl, t); +} + +//! Delete a term made in the previous constructions +/** + * \sa createNewTerm + */ +void +deleteNewTerm (Term t) +{ + if (TermRunid (t) >= 0) + { + /* if it has a positive runid, it did not come from the intruder + * knowledge, so it must have been constructed. + */ + free (t); + } +} + +//! Make a trace concrete +/** + * People find reading variables in attack outputs difficult. + * Thus, we instantiate them in a sensible way to make things more readable. + * + * This happens after sys->maxruns is fixed. Intruder constants thus are numbered from sys->maxruns onwards. + * + * \sa makeTraceClass + */ +Termlist +makeTraceConcrete (const System sys) +{ + Termlist changedvars; + Termlist tlnew; + int run; + + changedvars = NULL; + tlnew = findUsedConstants (sys); + run = 0; + + while (run < sys->maxruns) + { + Termlist tl; + + tl = sys->runs[run].locals; + while (tl != NULL) + { + /* variable, and of some run? */ + if (isTermVariable (tl->term) && TermRunid (tl->term) >= 0) + { + Term var; + Term name; + Termlist vartype; + + var = deVar (tl->term); + vartype = var->stype; + // Determine class name + if (vartype != NULL) + { + // Take first type name + name = vartype->term; + } + else + { + // Just a generic name + name = TERM_Data; + } + // We should turn this into an actual term + tlnew = createNewTerm (tlnew, name, isAgentType (var->stype)); + var->subst = tlnew->term; + + // Store for undo later + changedvars = termlistAdd (changedvars, var); + } + tl = tl->next; + } + run++; + } + termlistDelete (tlnew); + return changedvars; +} + +//! Make a trace a class again +/** + * \sa makeTraceConcrete + */ +void +makeTraceClass (const System sys, Termlist varlist) +{ + Termlist tl; + + tl = varlist; + while (tl != NULL) + { + Term var; + + var = tl->term; + if (realTermVariable (var)) + { + deleteNewTerm (var->subst); + var->subst = NULL; + } + tl = tl->next; + } + termlistDelete (varlist); +} + +//! Start attack output +void +attackOutputStart (void) +{ + if (switches.prune != 0) + { + FILE *fd; + + // Close old file (if any) + if (attack_stream != NULL) + { + fclose (attack_stream); // this automatically discards the old temporary file + } + // Create new file + fd = scyther_tempfile (); + attack_stream = fd; + globalStream = (char *) attack_stream; + } +} + +//! Stop attack output +void +attackOutputStop (void) +{ + // Nothing to do, just leave the opened tmpfile +} + +//! Copy one (finite) stream from beginning to end to another +/** + * Ugly first implementation, something to improve later (although it is not + * crucial code in any way) + */ +void +fcopy (FILE * fromstream, FILE * tostream) +{ + int c; + + // 'Just to be sure' + fflush (fromstream); + fseek (fromstream, 0, SEEK_SET); + + // Urgh, using the assignment in the loop condition, brrr. Fugly. + // Discourage. + while ((c = fgetc (fromstream)) != EOF) + { + fputc (c, tostream); + } +} + +//! Output an attack in the desired way +void +arachneOutputAttack () +{ + Termlist varlist; + + // Make concrete + if (switches.concrete) + { + varlist = makeTraceConcrete (sys); + } + else + { + varlist = NULL; + } + + // Wrapper for the real output + attackOutputStart (); + + // Generate the output, already! + if (switches.xml) + { + xmlOutSemitrace (sys); + } + else + { + dotSemiState (sys); + } + + // End wrapper + attackOutputStop (); + + // Undo concretization + makeTraceClass (sys, varlist); +} + +//------------------------------------------------------------------------ +// Main logic core +//------------------------------------------------------------------------ + + +//! Selector to select the first tuple goal. +/** + * Basically to get rid of -m2 tuple goals. + * Nice iteration, I'd suppose + */ +Binding +select_tuple_goal () +{ + List bl; + Binding tuplegoal; + + bl = sys->bindings; + tuplegoal = NULL; + while (bl != NULL && tuplegoal == NULL) + { + Binding b; + + b = (Binding) bl->data; + // Ignore done stuff + if (!b->blocked && !b->done) + { + if (isTermTuple (b->term)) + { + tuplegoal = b; + } + } + bl = bl->next; + } + return tuplegoal; +} + + +//! Iterate a binding +/** + * For DY model, we unfold any tuples first, otherwise we skip that. + */ +int +iterateOneBinding (void) +{ + Binding btup; + int flag; + + // marker + flag = true; + + // Are there any tuple goals? + if (switches.intruder) + { + // Maybe... (well, test) + btup = select_tuple_goal (); + } + else + { + // No, there are non that need to be expanded (no intruder) + btup = NULL; + } + if (btup != NULL) + { + /* Substitution or something resulted in a tuple goal: we immediately split them into compounds. + */ + Term tuple; + + tuple = deVar (btup->term); + if (realTermTuple (tuple)) + { + int count; + Term tupletermbuffer; + + tupletermbuffer = btup->term; + /* + * We solve this by replacing the tuple goal by the left term, and adding a goal for the right term. + */ + btup->term = TermOp1 (tuple); + count = + goal_add (TermOp2 (tuple), btup->run_to, + btup->ev_to, btup->level); + + // Show this in output + if (switches.output == PROOF) + { + indentPrint (); + eprintf ("Expanding tuple goal "); + termPrint (tupletermbuffer); + eprintf (" into %i subgoals.\n", count); + } + + // iterate + flag = iterate (); + + // undo + goal_remove_last (count); + btup->term = tupletermbuffer; + } + } + else + { + // No tuple goals; good + Binding b; + + /** + * Not pruned: count + */ + + sys->states = statesIncrease (sys->states); + sys->current_claim->states = + statesIncrease (sys->current_claim->states); + + /** + * Check whether its a final state (i.e. all goals bound) + */ + + b = (Binding) select_goal (sys); + if (b == NULL) + { + /* + * all goals bound, check for property + */ + if (switches.output == PROOF) + { + indentPrint (); + eprintf ("All goals are now bound.\n"); + } + sys->claims = statesIncrease (sys->claims); + sys->current_claim->count = + statesIncrease (sys->current_claim->count); + flag = property_check (sys); + } + else + { + /* + * bind this goal in all possible ways and iterate + */ + flag = bind_goal_all_options (b); + } + } + return flag; +} + +//! Main recursive procedure for Arachne +int +iterate () +{ + int flag; + + + flag = 1; + if (!prune_theorems (sys)) + { + if (!prune_claim_specifics (sys)) + { + if (!prune_bounds (sys)) + { + // Go and pick a binding for iteration + flag = iterateOneBinding (); + } + else + { + // Pruned because of bound! + sys->current_claim->complete = 0; + } + } + } + +#ifdef DEBUG + if (DEBUGL (5) && !flag) + { + warning ("Flag has turned 0!"); + } +#endif + + return flag; +} + +//! Just before starting output of an attack. +// +//! A wrapper for the case in which we need to buffer attacks. +int +iterate_buffer_attacks (void) +{ + if (switches.prune == 0) + { + return iterate (); + } + else + { + // We are pruning attacks, so they should go into a temporary file. + /* + * Set up the temporary file pointer + */ + char *buffer; + int result; + + // Push the old situation onto the stack + buffer = globalStream; + + // Start stuff + attack_stream = NULL; + attackOutputStart (); + + // Finally, proceed with iteration procedure + result = iterate (); + + /* Now, if it has been set, we need to copy the output to the normal streams. + */ + fcopy (attack_stream, (FILE *) buffer); + + // Close + fclose (attack_stream); + attack_stream = NULL; + + // Restore + globalStream = buffer; + + return result; + } +} + +//! Arachne single claim test +void +arachneClaimTest (Claimlist cl) +{ + // others we simply test... + int run; + int newruns; + Protocol p; + Role r; + + newruns = 0; + sys->current_claim = cl; + attack_length = INT_MAX; + attack_leastcost = INT_MAX; + cl->complete = 1; + p = (Protocol) cl->protocol; + r = (Role) cl->role; + + if (switches.output == PROOF) + { + indentPrint (); + eprintf ("Testing Claim "); + termPrint (cl->type); + eprintf (" from "); + termPrint (p->nameterm); + eprintf (", "); + termPrint (r->nameterm); + eprintf (" at index %i.\n", cl->ev); + } + indentDepth++; + + run = semiRunCreate (p, r); + newruns++; + { + int newgoals; + + int realStart (void) + { +#ifdef DEBUG + if (DEBUGL (5)) + { + printSemiState (); + } +#endif + return iterate_buffer_attacks (); + } + + proof_suppose_run (run, 0, cl->ev + 1); + newgoals = add_read_goals (run, 0, cl->ev + 1); + + /** + * Add initial knowledge node + */ + { + Termlist m0tl; + Term m0t; + int m0run; + + m0tl = knowledgeSet (sys->know); + m0t = termlist_to_tuple (m0tl); + // eprintf("Initial intruder knowledge node for "); + // termPrint(m0t); + // eprintf("\n"); + I_M->roledef->message = m0t; + m0run = semiRunCreate (INTRUDER, I_M); + newruns++; + proof_suppose_run (m0run, 0, 1); + sys->runs[m0run].height = 1; + + { + /** + * Add specific goal info and iterate algorithm + */ + add_claim_specifics (sys, cl, + roledef_shift (sys->runs[run]. + start, cl->ev), realStart); + } + + + // remove initial knowledge node + termDelete (m0t); + termlistDelete (m0tl); + semiRunDestroy (); + newruns--; + } + // remove claiming run goals + goal_remove_last (newgoals); + semiRunDestroy (); + newruns--; + } + //! Destroy + while (sys->maxruns > 0 && newruns > 0) + { + semiRunDestroy (); + newruns--; + } +#ifdef DEBUG + if (sys->bindings != NULL) + { + error ("sys->bindings NOT empty after claim test."); + } + if (sys->maxruns != 0) + { + error ("%i undestroyed runs left after claim test.", sys->maxruns); + } + if (newruns != 0) + { + error ("Lost %i runs after claim test.", newruns); + } +#endif + + //! Indent back + indentDepth--; + + if (switches.output == PROOF) + { + indentPrint (); + eprintf ("Proof complete for this claim.\n"); + } +} + +//! Arachne single claim inspection +int +arachneClaim (Claimlist cl) +{ + // Skip the dummy claims + if (!isTermEqual (cl->type, CLAIM_Empty)) + { + // Some claims are always true! + if (!cl->alwaystrue) + { + // others we simply test... + arachneClaimTest (cl); + } + claimStatusReport (sys, cl); + if (switches.xml) + { + xmlOutClaim (sys, cl); + } + return true; + } + return false; +} + + +//! Main code for Arachne +/** + * For this test, we manually set up some stuff. + * + * But later, this will just iterate over all claims. + * + * @TODO what does it return? And is that -1 valid, if nothing is tested? + */ +int +arachne () +{ + Claimlist cl; + int count; + + int print_send (Protocol p, Role r, Roledef rd, int index) + { + eprintf ("IRS: "); + termPrint (p->nameterm); + eprintf (", "); + termPrint (r->nameterm); + eprintf (", %i, ", index); + roledefPrint (rd); + eprintf ("\n"); + return 1; + } + + int determine_encrypt_max (Protocol p, Role r, Roledef rd, int index) + { + int tlevel; + + tlevel = term_encryption_level (rd->message); +#ifdef DEBUG + if (DEBUGL (3)) + { + eprintf ("Encryption level %i found for term ", tlevel); + termPrint (rd->message); + eprintf ("\n"); + } +#endif + if (tlevel > max_encryption_level) + max_encryption_level = tlevel; + return 1; + } + + /* + * set up claim role(s) + */ + + if (switches.runs == 0) + { + // No real checking. + return -1; + } + + if (sys->maxruns > 0) + { + error ("Something is wrong, number of runs >0."); + } + + sys->num_regular_runs = 0; + sys->num_intruder_runs = 0; + + max_encryption_level = 0; + iterate_role_events (determine_encrypt_max); +#ifdef DEBUG + if (DEBUGL (1)) + { + eprintf ("Maximum encryption level: %i\n", max_encryption_level); + } +#endif + + fixAgentKeylevels (); + + indentDepth = 0; + proofDepth = 0; + cl = sys->claimlist; + count = 0; + while (cl != NULL) + { + /** + * Check each claim + */ + if (arachneClaim (cl)) + { + count++; + } + + // next + cl = cl->next; + } + return count; +} + +//! Construct knowledge set at some event, based on a semitrace. +/** + * This is a very 'stupid' algorithm; it is just there because GijsH + * requested it. It does in no way guarantee that this is the actual + * knowledge set at the given point. It simply gives an underapproximation, + * that will be correct in most cases. The main reason for this is that it + * completely ignores any information on unbound variables, and regards them + * as bound constants. + * + * Because everything is supposed to be bound, we conclude that even 'read' + * events imply a certain knowledge. + * + * If aftercomplete is 0 or false, we actually check the ordering; otherwise we + * just assume the trace has finished. + * + * Use knowledgeDelete later to clean up. + */ +Knowledge +knowledgeAtArachne (const System sys, const int myrun, const int myindex, + const int aftercomplete) +{ + Knowledge know; + int run; + + know = knowledgeDuplicate (sys->know); // duplicate initial knowledge + run = 0; + while (run < sys->maxruns) + { + int index; + int maxheight; + Roledef rd; + + index = 0; + rd = sys->runs[run].start; + maxheight = sys->runs[run].height; + if (run == myrun && myindex > maxheight) + { + // local run index can override real step + maxheight = myindex; + } + + while (rd != NULL && index < maxheight) + { + // Check whether this event precedes myevent + if (aftercomplete || isDependEvent (run, index, myrun, myindex)) + { + // If it is a send (trivial) or a read (remarkable, but true + // because of bindings) we can add the message and the agents to + // the knowledge. + if (rd->type == SEND || rd->type == READ) + { + knowledgeAddTerm (know, rd->message); + if (rd->from != NULL) + knowledgeAddTerm (know, rd->from); + if (rd->to != NULL) + knowledgeAddTerm (know, rd->to); + } + index++; + rd = rd->next; + } + else + { + // Not ordered before anymore, so we skip to the next run. + rd = NULL; + } + } + run++; + } + return know; +} + +//! Determine whether a term is trivially known at some event in a partially ordered structure. +/** + * Important: read disclaimer at knowledgeAtArachne() + * + * Returns true iff the term is certainly known at that point in the + * semitrace. + */ +int +isTriviallyKnownAtArachne (const System sys, const Term t, const int run, + const int index) +{ + int result; + Knowledge knowset; + + knowset = knowledgeAtArachne (sys, run, index, false); + result = inKnowledge (knowset, t); + knowledgeDelete (knowset); + return result; +} + +//! Determine whether a term is trivially known after execution of some partially ordered structure. +/** + * Important: read disclaimer at knowledgeAtArachne() + * + * Returns true iff the term is certainly known after all events in the + * semitrace. + */ +int +isTriviallyKnownAfterArachne (const System sys, const Term t, const int run, + const int index) +{ + int result; + Knowledge knowset; + + knowset = knowledgeAtArachne (sys, run, index, true); + result = inKnowledge (knowset, t); + knowledgeDelete (knowset); + return result; +} diff --git a/gui/src/arachne.h b/gui/src/arachne.h new file mode 100644 index 0000000..02c9105 --- /dev/null +++ b/gui/src/arachne.h @@ -0,0 +1,20 @@ +#ifndef ARACHNE +#define ARACHNE + +#include "system.h" + +void arachneInit (const System sys); +void arachneDone (); +int arachne (); +int get_semitrace_length (); +void indentPrint (); +int isTriviallyKnownAtArachne (const System sys, const Term t, const int run, + const int index); +int isTriviallyKnownAfterArachne (const System sys, const Term t, + const int run, const int index); +void arachneOutputAttack (); +void printSemiState (); +int countIntruderActions (); +void role_name_print (const int run); + +#endif diff --git a/gui/src/attacktemplate.tex b/gui/src/attacktemplate.tex new file mode 100644 index 0000000..623c282 --- /dev/null +++ b/gui/src/attacktemplate.tex @@ -0,0 +1,61 @@ +\documentclass{article} +\usepackage{a4wide} +\usepackage{msc} +\usepackage{ifthen} + +%\setlength{\instwidth}{3.0cm} +%\setlength{\instdist}{4cm} +%\setlength{\actionwidth}{3.6cm} +%\setlength{\conditionoverlap}{1.9cm} + +% Action macro from MSC documentation + +\newsavebox{\labelbox} +\newlength{\oldwd} +\newlength{\oldht} +\newcommand{\Action}[2]{% + \setlength{\oldwd}{\actionwidth}% + \setlength{\oldht}{\actionheight}% + \savebox{\labelbox}{#1}% + \setlength{\actionwidth}{\wd\labelbox + 2\labeldist}% + \setlength{\actionheight}{\ht\labelbox + \dp\labelbox + 2\labeldist}% + \action{\usebox{\labelbox}}{#2}% + \setlength{\actionwidth}{\oldwd}% + \setlength{\actionheight}{\oldht}% +} + +\newlength{\mscspacer} +\setlength{\mscspacer}{1ex} + +\newcommand{\ActionBox}[2]{% + \Action{\parbox{\maxmscaction - 2\mscspacer}{\centering #1}}{#2} +} + +\newlength{\maxtemp} + +\newcommand{\maxlength}[2]{ + \settowidth{\maxtemp}{#2} + \ifthenelse{\lengthtest{#1 < \maxtemp}}{\setlength{#1}{\maxtemp}}{} + \ifthenelse{\lengthtest{\maxmscall < \maxtemp}}{\setlength{\maxmscall}{\maxtemp}}{} +} + + + +\newlength{\maxmscall} +\newlength{\maxmscinst} +\newlength{\maxmscaction} +\newlength{\maxmsccondition} + +\setlength{\maxmscall}{\mscspacer} +\setlength{\maxmscinst}{\mscspacer} +\setlength{\maxmscaction}{\mscspacer} +\setlength{\maxmsccondition}{\mscspacer} + +% pagestyle without numbering +\pagestyle{empty} + +\begin{document} + +\input{attack} + +\end{document} diff --git a/gui/src/binding.c b/gui/src/binding.c new file mode 100644 index 0000000..f5f9bb5 --- /dev/null +++ b/gui/src/binding.c @@ -0,0 +1,617 @@ +/** + * Handle bindings for Arache engine. + */ + +#include "list.h" +#include "role.h" +#include "label.h" +#include "system.h" +#include "binding.h" +#include "warshall.h" +#include "debug.h" +#include "term.h" +#include "termmap.h" +#include "arachne.h" +#include "switches.h" +#include "depend.h" +#include "error.h" +#if !defined(__APPLE__) +#include +#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; +} diff --git a/gui/src/binding.h b/gui/src/binding.h new file mode 100644 index 0000000..34bb8b8 --- /dev/null +++ b/gui/src/binding.h @@ -0,0 +1,53 @@ +#ifndef BINDINGS +#define BINDINGS + +#include "term.h" +#include "termmap.h" +#include "system.h" + +//! Binding structure +/* + * Idea is the ev_from *has to* precede the ev_to + */ +struct binding +{ + int done; //!< Iff true, it is bound + int blocked; //!< Iff true, ignore it + + int run_from; //!< origination run + int ev_from; //!< step in origination run + + int run_to; //!< destination run + int ev_to; //!< step in destination run + + Term term; //!< Binding term + int level; //!< ??? +}; + +typedef struct binding *Binding; //!< pointer to binding structure + + +void bindingInit (const System mysys); +void bindingDone (); + +int binding_print (Binding b); +int valid_binding (Binding b); + +int goal_add (Term term, const int run, const int ev, const int level); +int goal_add_fixed (Term term, const int run, const int ev, const int fromrun, + const int fromev); +void goal_remove_last (int n); +int goal_bind (const Binding b, const int run, const int ev); +void goal_unbind (const Binding b); +int binding_block (Binding b); +int binding_unblock (Binding b); +int labels_ordered (Termmap runs, Termlist labels); + +int iterate_bindings (int (*func) (Binding b)); +int iterate_preceding_bindings (const int run, const int ev, + int (*func) (Binding b)); + +int bindings_c_minimal (); +int countBindingsDone (); + +#endif diff --git a/gui/src/bugs.txt b/gui/src/bugs.txt new file mode 100644 index 0000000..98e77b0 --- /dev/null +++ b/gui/src/bugs.txt @@ -0,0 +1,119 @@ +--+++ Crititcal Bugs + + * soph segfaults at no switch or -r4 (-r3 is okay??) using non-debug version. + * './scyther -a ../spdl/nsl3.spdl --increment-runs' segfaults. The main reason is that the Archne engine uses runs in a different way. + Maybe it is best to disable --increment rules for non-ModelChecker verification. + +---+++ Bugs + + * Problem with goal bindings: instantiation of variable with a tuple might + introduce a tuple goal, which is forbidden. We must find a way to deal with this. This typically occurs in type flaw searches. + * Arachne seems to trip over claims with empty prec sets. Maybe we + simply should not test these. + * Splice/AS does not work well because priority key search stumbles over the + public key search stuff. That is a flaw in the heuristic: we should not look + for anything that is in the intruder knowledge already. In fact, it is a + problem with branching. We should not look for PK(X), even if X is a + variable. Priority should go to keys of which the constructor is not in M_0, + maybe that heuristic works. + However, there seems to be an infinite loop for this in the algorithm, which + I did not anticipate. Investigate! +
+ 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 [,] ]; + 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. + diff --git a/gui/src/build.sh b/gui/src/build.sh new file mode 100755 index 0000000..c68c94e --- /dev/null +++ b/gui/src/build.sh @@ -0,0 +1,16 @@ +#!/bin/sh + +PLATFORM=`uname` +echo $PLATFORM +if [ "$PLATFORM" = "Darwin" ] +then + ./subbuild-mac-universal.sh +else + if [ "$PLATFORM" = "Linux" ] + then + ./subbuild-unix-both.sh + else + echo "I don't know platform $PLATFORM, so I won't do anything" + fi +fi + diff --git a/gui/src/claim.c b/gui/src/claim.c new file mode 100644 index 0000000..982029a --- /dev/null +++ b/gui/src/claim.c @@ -0,0 +1,1136 @@ +/** + * + *@file claim.c + * + * Claim handling for the Arachne engine. + * + */ + +#include + +#include "termmap.h" +#include "system.h" +#include "label.h" +#include "error.h" +#include "debug.h" +#include "binding.h" +#include "arachne.h" +#include "specialterm.h" +#include "switches.h" +#include "color.h" +#include "cost.h" +#include "timer.h" + +//! When none of the runs match +#define MATCH_NONE 0 +//! When the order matches +#define MATCH_ORDER 1 +//! When the order is reversed +#define MATCH_REVERSE 2 +//! When the content matches +#define MATCH_CONTENT 3 + +//! This label is fixed +#define LABEL_GOOD -3 +//! This label still needs to be done +#define LABEL_TODO -2 + +extern int globalError; +extern int attack_leastcost; + +// Debugging the NI-SYNCH checks +//#define OKIDEBUG + +// Forward declaration +int oki_nisynch (const System sys, const int trace_index, + const Termmap role_to_run, const Termmap label_to_index); + +/* + * Validity checks for claims + * + * Note that the first few operate on claims, and that the tests for e.g. the Arachne engine are seperate. + */ + + +#ifdef OKIDEBUG +int indac = 0; + +void +indact () +{ + int i; + + i = indac; + while (i > 0) + { + eprintf ("| "); + i--; + } +} +#endif + +//! Check complete message match +/** + * Roledef based. + *@returns MATCH_NONE or MATCH_CONTENT + */ +__inline__ int +events_match_rd (const Roledef rdi, const Roledef rdj) +{ + if (isTermEqual (rdi->message, rdj->message) && + isTermEqual (rdi->from, rdj->from) && + isTermEqual (rdi->to, rdj->to) && + isTermEqual (rdi->label, rdj->label) && + !(rdi->internal || rdj->internal)) + { + return MATCH_CONTENT; + } + else + { + return MATCH_NONE; + } +} + + +//! Check complete message match +/** + *@returns any of the MATCH_ signals + */ +__inline__ int +events_match (const System sys, const int i, const int j) +{ + Roledef rdi, rdj; + + rdi = sys->traceEvent[i]; + rdj = sys->traceEvent[j]; + if (isTermEqual (rdi->message, rdj->message) && + isTermEqual (rdi->from, rdj->from) && + isTermEqual (rdi->to, rdj->to) && + isTermEqual (rdi->label, rdj->label) && + !(rdi->internal || rdj->internal)) + { + if (rdi->type == SEND && rdj->type == READ) + { + if (i < j) + return MATCH_ORDER; + else + return MATCH_REVERSE; + } + if (rdi->type == READ && rdj->type == SEND) + { + if (i > j) + return MATCH_ORDER; + else + return MATCH_REVERSE; + } + } + return MATCH_NONE; +} + + +//! Check nisynch from label_to_index. +__inline__ int +oki_nisynch_full (const System sys, const Termmap label_to_index) +{ + // Are all labels well linked? + Termmap label_to_index_scan; + + label_to_index_scan = label_to_index; + while (label_to_index_scan != NULL) + { + if (label_to_index_scan->result != LABEL_GOOD) + { +#ifdef OKIDEBUG + indact (); + eprintf ("Incorrectly linked label at the end,"); + eprintf ("label: "); + termPrint (label_to_index_scan->term); + eprintf ("\n"); +#endif + return 0; + } + label_to_index_scan = label_to_index_scan->next; + } + // Apparently they are all well linked + return 1; +} + +//! Evaluate claims or internal reads (chooses) +__inline__ int +oki_nisynch_other (const System sys, const int trace_index, + const Termmap role_to_run, const Termmap label_to_index) +{ + int result; + +#ifdef OKIDEBUG + indact (); + eprintf ("Exploring further assuming this (claim) run is not involved.\n"); + indac++; +#endif + result = oki_nisynch (sys, trace_index - 1, role_to_run, label_to_index); +#ifdef OKIDEBUG + indact (); + eprintf (">%i<\n", result); + indac--; +#endif + return result; +} + +//! Evaluate reads +__inline__ int +oki_nisynch_read (const System sys, const int trace_index, + const Termmap role_to_run, const Termmap label_to_index) +{ + /* + * Read is only relevant for already involved runs, and labels in prec + */ + Termmap role_to_run_scan; + int result = 7; + Roledef rd; + int rid; + + rd = sys->traceEvent[trace_index]; + rid = sys->traceRun[trace_index]; + + role_to_run_scan = role_to_run; + while (role_to_run_scan != NULL) + { + if (role_to_run_scan->result == rid) + { + // Involved, but is it a prec label? + if (termmapGet (label_to_index, rd->label) == LABEL_TODO) + { + Termmap label_to_index_buf; + int result; + + label_to_index_buf = termmapDuplicate (label_to_index); + label_to_index_buf = + termmapSet (label_to_index_buf, rd->label, trace_index); +#ifdef OKIDEBUG + indact (); + eprintf ("Exploring because this (read) run is involved.\n"); + indac++; +#endif + result = + oki_nisynch (sys, trace_index - 1, role_to_run, + label_to_index_buf); +#ifdef OKIDEBUG + indact (); + eprintf (">%i<\n", result); + indac--; +#endif + termmapDelete (label_to_index_buf); + return result; + } + } + role_to_run_scan = role_to_run_scan->next; + } + // Apparently not involved +#ifdef OKIDEBUG + indact (); + eprintf ("Exploring further assuming this (read) run is not involved.\n"); + indac++; +#endif + result = oki_nisynch (sys, trace_index - 1, role_to_run, label_to_index); +#ifdef OKIDEBUG + indac--; +#endif + return result; +} + + +//! Evaluate sends +__inline__ int +oki_nisynch_send (const System sys, const int trace_index, + const Termmap role_to_run, const Termmap label_to_index) +{ + Roledef rd; + int rid; + int result = 8; + int old_run; + Term rolename; + + rd = sys->traceEvent[trace_index]; + rid = sys->traceRun[trace_index]; + /* + * Two options: it is either involved or not + */ + // 1. Assume that this run is not yet involved +#ifdef OKIDEBUG + indact (); + eprintf ("Exploring further assuming (send) run %i is not involved.\n", + rid); + indac++; +#endif + result = oki_nisynch (sys, trace_index - 1, role_to_run, label_to_index); +#ifdef OKIDEBUG + indact (); + eprintf (">%i<\n", result); + indac--; +#endif + if (result) + return 1; + +#ifdef OKIDEBUG + indact (); + eprintf ("Exploring when %i is involved.\n", rid); +#endif + // 2. It is involved. Then either already used for this role, or will be now. + rolename = sys->runs[rid].role->nameterm; + old_run = termmapGet (role_to_run, rolename); // what was already stored for this role as the runid + if (old_run == -1 || old_run == rid) + { + int partner_index; + + // Was not involved yet in a registerd way, or was the correct rid + partner_index = termmapGet (label_to_index, rd->label); + // Ordered match needed for this label + // So it already needs to be filled by a read + if (partner_index >= 0) + { + // There is already a read for it + if (events_match (sys, partner_index, trace_index) == MATCH_ORDER) + { + // They match in the right order + Termmap role_to_run_buf, label_to_index_buf; + +#ifdef OKIDEBUG + indact (); + eprintf ("Matching messages found for label "); + termPrint (rd->label); + eprintf ("\n"); +#endif + /** + *@todo Optimization can be done when old_run == rid, no copy of role_to_run needs to be made. + */ + role_to_run_buf = termmapDuplicate (role_to_run); + role_to_run_buf = termmapSet (role_to_run_buf, rolename, rid); + label_to_index_buf = termmapDuplicate (label_to_index); + label_to_index_buf = + termmapSet (label_to_index_buf, rd->label, LABEL_GOOD); +#ifdef OKIDEBUG + indact (); + eprintf ("In NI-Synch scan, assuming %i run is involved.\n", + rid); + indact (); + eprintf + ("Exploring further assuming this matching, which worked.\n"); + indac++; +#endif + result = + oki_nisynch (sys, trace_index - 1, role_to_run_buf, + label_to_index_buf); +#ifdef OKIDEBUG + indact (); + eprintf (">%i<\n", result); + indac--; +#endif + termmapDelete (label_to_index_buf); + termmapDelete (role_to_run_buf); + return result; + } + } + } + return 0; +} + + +//! nisynch generalization +/** + * role_to_run maps the involved roles to run identifiers. + * label_to_index maps all labels in prec to the event indices for things already found, + * or to LABEL_TODO for things not found yet but in prec, and LABEL_GOOD for well linked messages (and that have thus defined a runid for the corresponding role). + * All values not in prec map to -1. + *@returns 1 iff the claim is allright, 0 iff it is violated. + */ +int +oki_nisynch (const System sys, const int trace_index, + const Termmap role_to_run, const Termmap label_to_index) +{ + int type; + + // Check for completed trace + if (trace_index < 0) + return oki_nisynch_full (sys, label_to_index); + +#ifdef OKIDEBUG + indact (); + eprintf ("Checking event %i", trace_index); + eprintf (" = #%i : ", sys->traceRun[trace_index]); + roledefPrint (sys->traceEvent[trace_index]); + eprintf ("\n"); +#endif + + type = sys->traceEvent[trace_index]->type; + + if (type == CLAIM || sys->traceEvent[trace_index]->internal) + return oki_nisynch_other (sys, trace_index, role_to_run, label_to_index); + if (type == READ) + return oki_nisynch_read (sys, trace_index, role_to_run, label_to_index); + if (type == SEND) + return oki_nisynch_send (sys, trace_index, role_to_run, label_to_index); + /* + * Exception: no claim, no send, no read, what is it? + */ + error ("Unrecognized event type in claim scanner at %i.", trace_index); + return 0; +} + +/* + * Real checks + */ + +//! Check validity of ni-synch claim at event i. +/** + *@returns 1 iff claim is true. + */ +int +check_claim_nisynch (const System sys, const int i) +{ + Roledef rd; + int result; + int rid; + Termmap f, g; + Term label; + Claimlist cl; + Termlist tl; + + rid = sys->traceRun[i]; + rd = sys->traceEvent[i]; + cl = rd->claiminfo; + cl->count = statesIncrease (cl->count); + f = termmapSet (NULL, sys->runs[rid].role->nameterm, rid); + + // map all labels in prec to LABEL_TODO + g = NULL; + label = rd->label; + + tl = cl->prec; + while (tl != NULL) + { + g = termmapSet (g, tl->term, LABEL_TODO); + tl = tl->next; + } + /* + * Check claim + */ + result = oki_nisynch (sys, i, f, g); + if (!result) + { +#ifdef DEBUG + globalError++; + warning ("Claim has failed!"); + eprintf ("To be exact, claim label "); + termPrint (cl->label); + eprintf (" with prec set "); + termlistPrint (cl->prec); + eprintf ("\n"); + eprintf ("i: %i\nf: ", i); + termmapPrint (f); + eprintf ("\ng: "); + termmapPrint (g); + eprintf ("\n"); + globalError--; +#endif + + } + termmapDelete (f); + termmapDelete (g); + return result; +} + +//! Check validity of ni-agree claim at event i. +/** + *@returns 1 iff claim is true. + *@todo This is now just a copy of ni-synch, should be fixed asap. + */ +int +check_claim_niagree (const System sys, const int i) +{ + Roledef rd; + int result; + int rid; + Termmap f, g; + Term label; + Claimlist cl; + Termlist tl; + + rid = sys->traceRun[i]; + rd = sys->traceEvent[i]; + cl = rd->claiminfo; + cl->count = statesIncrease (cl->count); + f = termmapSet (NULL, sys->runs[rid].role->nameterm, rid); + + // map all labels in prec to LABEL_TODO + g = NULL; + label = rd->label; + + tl = cl->prec; + while (tl != NULL) + { + g = termmapSet (g, tl->term, LABEL_TODO); + tl = tl->next; + } + /* + * Check claim + */ + result = oki_nisynch (sys, i, f, g); + if (!result) + { +#ifdef DEBUG + warning ("Claim has failed!"); + eprintf ("To be exact, claim label "); + termPrint (cl->label); + eprintf (" with prec set "); + termlistPrint (cl->prec); + eprintf ("\n"); + eprintf ("i: %i\nf: ", i); + termmapPrint (f); + eprintf ("\ng: "); + termmapPrint (g); + eprintf ("\n"); +#endif + + } + termmapDelete (f); + termmapDelete (g); + return result; +} + + + +//! Check generic agree claim for a given set of runs, arachne style +int +arachne_runs_agree (const System sys, const Claimlist cl, const Termmap runs) +{ + Termlist labels; + int flag; + +#ifdef DEBUG + if (DEBUGL (5)) + { + eprintf ("Checking runs agreement for Arachne.\n"); + termmapPrint (runs); + eprintf ("\n"); + } +#endif + + flag = 1; + labels = cl->prec; + while (flag && labels != NULL) + { + // For each label, check whether it matches. Maybe a bit too strict (what about variables?) + // Locate roledefs for read & send, and check whether they are before step + Roledef rd_send, rd_read; + Labelinfo linfo; + + Roledef get_label_event (const Term role, const Term label) + { + Roledef rd, rd_res; + int i; + int run; + + run = termmapGet (runs, role); + if (run != -1) + { +#ifdef DEBUG + if (run < 0 || run >= sys->maxruns) + { + globalError++; + eprintf ("Run mapping %i out of bounds for role ", run); + termPrint (role); + eprintf (" and label "); + termPrint (label); + eprintf ("\n"); + eprintf ("This label has sendrole "); + termPrint (linfo->sendrole); + eprintf (" and readrole "); + termPrint (linfo->readrole); + eprintf ("\n"); + globalError--; + error ("Run mapping is out of bounds."); + } +#endif + rd = sys->runs[run].start; + rd_res = NULL; + i = 0; + while (i < sys->runs[run].step && rd != NULL) + { + if (isTermEqual (rd->label, label)) + { + rd_res = rd; + rd = NULL; + } + else + { + rd = rd->next; + } + i++; + } + return rd_res; + } + else + { + return NULL; + } + } + + // Main + linfo = label_find (sys->labellist, labels->term); + if (!linfo->ignore) + { + rd_send = get_label_event (linfo->sendrole, labels->term); + rd_read = get_label_event (linfo->readrole, labels->term); + + if (rd_send == NULL || rd_read == NULL) + { + // False! + flag = 0; + } + else + { + // Compare + if (events_match_rd (rd_send, rd_read) != MATCH_CONTENT) + { + // False! + flag = 0; + } + } + } + + labels = labels->next; + } + return flag; +} + +//! Check arachne authentications claim +/** + * Per default, occurs in run 0, but for generality we have left the run parameter in. + *@returns 1 if the claim is true, 0 if it is not. + */ +int +arachne_claim_authentications (const System sys, const int claim_run, + const int claim_index, const int require_order) +{ + Claimlist cl; + Roledef rd; + Termmap runs_involved; + int flag; + + int fill_roles (Termlist roles_tofill) + { + if (roles_tofill == NULL) + { + // All roles have been chosen + if (arachne_runs_agree (sys, cl, runs_involved)) + { + // niagree holds + if (!require_order) + { + return 1; + } + else + { + // Stronger claim: nisynch. Test for ordering as well. + return labels_ordered (runs_involved, cl->prec); + } + } + else + { + // niagree does not hold + return 0; + } + } + else + { + // Choose a run for this role, if possible + // Note that any will do + int run, flag; + + run = 0; + flag = 0; + while (run < sys->maxruns) + { + // Has to be from the right protocol + if (sys->runs[run].protocol == cl->protocol) + { + // Has to be the right name + if (isTermEqual + (sys->runs[run].role->nameterm, roles_tofill->term)) + { + // Choose, iterate + runs_involved = + termmapSet (runs_involved, roles_tofill->term, run); + flag = flag || fill_roles (roles_tofill->next); + } + } + run++; + } + return flag; + } + } + +#ifdef DEBUG + if (DEBUGL (5)) + { + eprintf ("Testing for Niagree claim with any sort of runs.\n"); + } +#endif + + rd = roledef_shift (sys->runs[claim_run].start, claim_index); +#ifdef DEBUG + if (rd == NULL) + error ("Retrieving claim info for NULL node??"); +#endif + cl = rd->claiminfo; + + runs_involved = termmapSet (NULL, cl->roles->term, claim_run); + flag = fill_roles (cl->roles->next); + + termmapDelete (runs_involved); + return flag; +} + +//! Test niagree +int +arachne_claim_niagree (const System sys, const int claim_run, + const int claim_index) +{ + return arachne_claim_authentications (sys, claim_run, claim_index, 0); +} + +//! Test nisynch +int +arachne_claim_nisynch (const System sys, const int claim_run, + const int claim_index) +{ + return arachne_claim_authentications (sys, claim_run, claim_index, 1); +} + +//! Are all agents trusted of the claim run (as required by the property?) +int +pruneClaimRunTrusted (const System sys) +{ + if (sys->trustedRoles == NULL) + { + // all agents need to be trusted + if (!isRunTrusted (sys, 0)) + { + return true; + } + } + else + { + // a subset is trusted + if (!isAgentlistTrusted (sys, sys->trustedRoles)) + { + return true; + } + } + return false; +} + +//! Prune determination for specific properties +/** + * Sometimes, a property holds in part of the tree. Thus, we don't need to explore that part further if we want to find an attack. + * + *@returns true iff this state is invalid for some reason + */ +int +prune_claim_specifics (const System sys) +{ + // generic status of (all) roles trusted or not + if (pruneClaimRunTrusted (sys)) + { + if (switches.output == PROOF) + { + indentPrint (); + eprintf + ("Pruned because all agents of the claim run must be trusted.\n"); + } + return true; + } + + // specific claims + if (sys->current_claim->type == CLAIM_Niagree) + { + if (arachne_claim_niagree (sys, 0, sys->current_claim->ev)) + { + sys->current_claim->count = + statesIncrease (sys->current_claim->count); + if (switches.output == PROOF) + { + indentPrint (); + eprintf + ("Pruned: niagree holds in this part of the proof tree.\n"); + } + return 1; + } + } + if (sys->current_claim->type == CLAIM_Nisynch) + { + if (arachne_claim_nisynch (sys, 0, sys->current_claim->ev)) + { + sys->current_claim->count = + statesIncrease (sys->current_claim->count); + if (switches.output == PROOF) + { + indentPrint (); + eprintf + ("Pruned: nisynch holds in this part of the proof tree.\n"); + } + return 1; + } + } + return 0; +} + +//! Setup system for specific claim test and iterate +int +add_claim_specifics (const System sys, const Claimlist cl, const Roledef rd, + int (*callback) (void)) +{ + /* + * different cases + */ + + // per default, all agents are trusted + sys->trustedRoles = NULL; + + if (cl->type == CLAIM_Secret) + { + int newgoals; + int flag; + + /** + * Secrecy claim + */ + if (switches.output == PROOF) + { + indentPrint (); + eprintf ("* To verify the secrecy claim, we add the term "); + termPrint (rd->message); + eprintf (" as a goal.\n"); + indentPrint (); + eprintf + ("* If all goals can be bound, this constitutes an attack.\n"); + } + + /** + * We say that a state exists for secrecy, but we don't really test wheter the claim can + * be reached (without reaching the attack). + */ + cl->count = statesIncrease (cl->count); + newgoals = goal_add (rd->message, 0, cl->ev, 0); // Assumption that all claims are in run 0 + + flag = callback (); + + goal_remove_last (newgoals); + return flag; + } + + if (cl->type == CLAIM_Reachable) + { + int flag; + + if (switches.check) + { + // For reachability claims in check mode, we restrict the number of runs to the number of roles of this protocol + Protocol protocol; + int rolecount; + + protocol = (Protocol) cl->protocol; + rolecount = termlistLength (protocol->rolenames); + switches.runs = rolecount; + } + if (rd->message != NULL) + { + sys->trustedRoles = tuple_to_termlist (rd->message); + +#ifdef DEBUG + if (DEBUGL (2)) + { + eprintf ("Trusted roles : "); + termlistPrint (sys->trustedRoles); + eprintf ("\n"); + } +#endif + } + + flag = callback (); + + if (rd->message != NULL) + { + termlistDelete (sys->trustedRoles); + sys->trustedRoles = NULL; + } + return flag; + } + + return callback (); +} + +//! Count a false claim +/** + * Counts global attacks as well as claim instances. + */ +void +count_false_claim (const System sys) +{ + sys->attackid++; + sys->current_claim->failed = statesIncrease (sys->current_claim->failed); +} + + +//! Check properties +int +property_check (const System sys) +{ + int flag; + int cost; + + flag = 1; + + /** + * By the way the claim is handled, this automatically means a flaw. + */ + count_false_claim (sys); + if (switches.output == ATTACK) + { + arachneOutputAttack (); + } + // Store attack cost if cheaper + cost = attackCost (sys); + if (cost < attack_leastcost) + { + // Cheapest attack + attack_leastcost = cost; + if (switches.output == PROOF) + { + indentPrint (); + eprintf ("New cheaper attack found with cost %i.\n", cost); + } + } + + return flag; +} + +/* claim status reporting */ + +//! Print something bad +void +printBad (char *s) +{ + eprintf ("%s%s%s", COLOR_Red, s, COLOR_Reset); +} + +//! Print something good +void +printGood (char *s) +{ + eprintf ("%s%s%s", COLOR_Green, s, COLOR_Reset); +} + +//! Print state (existState, isAttack) +/** + * Fail == ( existState xor isAttack ) + */ +void +printOkFail (int existState, int isAttack) +{ + if (existState != isAttack) + { + printGood ("Ok"); + } + else + { + printBad ("Fail"); + } +} + + +//! Report claim status +int +claimStatusReport (const System sys, Claimlist cl) +{ + if (isTermEqual (cl->type, CLAIM_Empty)) + { + return false; + } + else + { + Protocol protocol; + Term pname; + Term rname; + Termlist labellist; + int isAttack; // stores whether this claim failure constitutes an attack or not + + if (switches.output != SUMMARY) + { + globalError++; + } + if (isTermEqual (cl->type, CLAIM_Reachable)) + { + // An attack on reachable is not really an attack, we're just generating the state space + isAttack = false; + } + else + { + isAttack = true; + } + + eprintf ("claim\t"); + + protocol = (Protocol) cl->protocol; + pname = protocol->nameterm; + rname = cl->rolename; + + labellist = tuple_to_termlist (cl->label); + + /* maybe the label contains duplicate info: if so, we remove it here */ + { + Termlist tl; + tl = labellist; + while (tl != NULL) + { + if (isTermEqual (tl->term, pname) + || isTermEqual (tl->term, rname)) + { + tl = termlistDelTerm (tl); + labellist = tl; + } + else + { + tl = tl->next; + } + } + } + + termPrint (pname); + eprintf (","); + termPrint (rname); + eprintf ("\t"); + /* second print event_label */ + termPrint (cl->type); + + eprintf ("_"); + if (labellist != NULL) + { + Termlist tl; + + tl = labellist; + while (tl != NULL) + { + termPrint (tl->term); + tl = tl->next; + if (tl != NULL) + { + eprintf (","); + } + } + /* clean up */ + termlistDelete (labellist); + labellist = NULL; + } + else + { + eprintf ("?"); + } + /* add parameter */ + eprintf ("\t"); + if (cl->parameter != NULL) + { + termPrint (cl->parameter); + } + else + { + eprintf ("-"); + } + + /* now report the status */ + eprintf ("\t"); + if (cl->count > 0 && cl->failed > 0) + { + /* there is a state */ + printOkFail (true, isAttack); + + eprintf ("\t"); + /* are these all attacks? */ + eprintf ("["); + if (cl->complete) + { + eprintf ("exactly"); + } + else + { + eprintf ("at least"); + } + eprintf (" %i ", cl->failed); + if (isAttack) + { + eprintf ("attack"); + } + else + { + eprintf ("variant"); + } + if (cl->failed != 1) + { + eprintf ("s"); + } + eprintf ("]"); + } + else + { + /* no state */ + printOkFail (false, isAttack); + eprintf ("\t"); + + /* subcases */ + if (cl->count == 0) + { + /* not encountered */ + eprintf ("[does not occur]"); + } + else + { + /* does occur */ + if (cl->complete) + { + /* complete proof */ + eprintf ("[proof of correctness]"); + } + else + { + /* only due to bounds */ + eprintf ("[no attack within bounds]"); + } + } + if (cl->timebound) + eprintf ("\ttime=%i", get_time_limit ()); + } + + /* states (if asked) */ + if (switches.countStates) + { + eprintf ("\tstates="); + statesFormat (cl->states); + } + + /* any warnings */ + if (cl->warnings) + { + eprintf ("\t[read the warnings for more information]"); + } + + /* new line */ + eprintf ("\n"); + + if (switches.output != SUMMARY) + { + globalError--; + } + + return true; + } +} diff --git a/gui/src/claim.h b/gui/src/claim.h new file mode 100644 index 0000000..bf916c8 --- /dev/null +++ b/gui/src/claim.h @@ -0,0 +1,18 @@ +#ifndef CLAIMS +#define CLAIMS + +int check_claim_nisynch (const System sys, const int i); +int check_claim_niagree (const System sys, const int i); +int arachne_claim_niagree (const System sys, const int claim_run, + const int claim_index); +int arachne_claim_nisynch (const System sys, const int claim_run, + const int claim_index); + +int prune_claim_specifics (const System sys); +int add_claim_specifics (const System sys, const Claimlist cl, const + Roledef rd, int (*callback) (void)); +void count_false_claim (const System sys); +int property_check (const System sys); +int claimStatusReport (const System sys, Claimlist cl); + +#endif diff --git a/gui/src/color.c b/gui/src/color.c new file mode 100644 index 0000000..6eb56a8 --- /dev/null +++ b/gui/src/color.c @@ -0,0 +1,39 @@ +/** @file color.c \brief Color output for terminals. + * + * Depends on the switches (to disable them with a --plain switch) + */ + +#include +#include +#include +#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) +{ +} diff --git a/gui/src/color.h b/gui/src/color.h new file mode 100644 index 0000000..d174ed8 --- /dev/null +++ b/gui/src/color.h @@ -0,0 +1,12 @@ +#ifndef COLOROUTPUT +#define COLOROUTPUT + +extern char *COLOR_Reset; +extern char *COLOR_Red; +extern char *COLOR_Green; +extern char *COLOR_Bold; + +void colorInit (void); +void colorDone (void); + +#endif diff --git a/gui/src/compile.txt b/gui/src/compile.txt new file mode 100644 index 0000000..71e32d5 --- /dev/null +++ b/gui/src/compile.txt @@ -0,0 +1,18 @@ +How to compile Scyther + +Requirements expressed as Ubuntu packages where [name][location] + +Needed: + + gcc + If you don't know what this is, please stop reading. + scons + A Python script set to replace the make etc. toolchain. + +For cross-compilation (Windows): + + [mingw32][universe] + GCC variant to compile for windows + w32 binutils. + + Use 'scons arch=windows' to generate the binary. + diff --git a/gui/src/compiler.c b/gui/src/compiler.c new file mode 100644 index 0000000..8cdfe2c --- /dev/null +++ b/gui/src/compiler.c @@ -0,0 +1,2164 @@ +#include +#include +#include +#include +#include "tac.h" +#include "term.h" +#include "termlist.h" +#include "label.h" +#include "system.h" +#include "knowledge.h" +#include "symbol.h" +#include "compiler.h" +#include "switches.h" +#include "specialterm.h" +#include "warshall.h" +#include "hidelevel.h" +#include "debug.h" +#include "intruderknowledge.h" +#include "error.h" +#include "mgu.h" + +/* + Simple sys pointer as a global. Yields cleaner code although it's against programming standards. + It is declared as static to hide it from the outside world, and to indicate its status. + Other modules will just see a nicely implemented sys parameter of compile, so we can always change + it later if somebody complains. Which they won't. +*/ + +static System sys; +static Tac tac_root; + +/* + * Declaration from system.c + */ +extern int protocolCount; + +/* + Forward declarations. +*/ + +void tacProcess (Tac tc); +void levelInit (void); +void levelDone (void); +Term levelFind (Symbol s, int i); +Term symbolFind (Symbol s); +Term tacTerm (Tac tc); +Termlist tacTermlist (Tac tc); +Term levelDeclare (Symbol s, int isVar, int level); +void compute_role_variables (const System sys, Protocol p, Role r); +void roleKnows (Tac tc); + +/* + * Global stuff + */ + +//! Levels of scope: global, protocol, role +#define MAXLEVELS 3 +static Termlist leveltl[MAXLEVELS]; +static int level; +static int maxruns; +static Protocol thisProtocol; +static Role thisRole; + +//! Init terms and such +void +compilerInit (const System mysys) +{ + int i; + + /* transfer to global static variable */ + sys = mysys; + /* init levels */ + for (i = 0; i < MAXLEVELS; i++) + leveltl[i] = NULL; + level = -1; + levelInit (); + + /* create special terms */ + specialTermInit (sys); +} + +//! Make a global constant +Term +makeGlobalConstant (const char *s) +{ + return levelDeclare (symbolSysConst (s), 0, 0); +} + +//! Make a global variable +Term +makeGlobalVariable (const char *s) +{ + return levelDeclare (symbolSysConst (s), 1, 0); +} + +//! Clean up afterwards +void +compilerDone (void) +{ + return; +} + +//! Compute read variables for a role +Termlist +compute_read_variables (const Role r) +{ + Termlist tl; + + int process_event (Roledef rd) + { + if (rd->type == READ) + { + tl = termlistAddVariables (tl, rd->from); + tl = termlistAddVariables (tl, rd->to); + tl = termlistAddVariables (tl, rd->message); + } + return 1; + } + + tl = NULL; + roledef_iterate_events (r->roledef, process_event); + return tl; +} + +/* ------------------------------------------------------------------- */ + +//! Compile the tac into the system +/** + *@todo Currently, the semantics assume all labels are globally unique, but this is not enforced yet. There should be some automatic renaming when compositing protocols. + *\sa oki_nisynch + */ +void +compile (Tac tc, int maxrunsset) +{ + /* Init globals */ + maxruns = maxrunsset; + tac_root = tc; + + /* process the tac */ + tacProcess (tac_root); + + /* Clean up keylevels */ + symbol_fix_keylevels (); + + /* cleanup */ + levelDone (); +} + +//! Print error line number. +/** + *@todo This is obsolete, and should all go to stderr + */ +void +errorTac (int lineno) +{ + globalError++; + eprintf (" on line %i.\n", lineno); + exit (1); +} + +//! Enter nested scope. +void +levelInit (void) +{ + level++; + if (level >= MAXLEVELS) + { + error ("level is increased too much."); + } + leveltl[level] = NULL; +} + +//! Leave nested scope. +void +levelDone (void) +{ + if (level < 0) + { + error ("level is decreased too much."); + } + leveltl[level] = NULL; + level--; +} + +Term +levelDeclare (Symbol s, int isVar, int level) +{ + Term t; + + t = levelFind (s, level); + if (t == NULL) + { + /* new! */ + if (isVar) + { + t = makeTermType (VARIABLE, s, -(level + 1)); + sys->variables = termlistAdd (sys->variables, t); + } + else + { + t = makeTermType (GLOBAL, s, -(level + 1)); + } + leveltl[level] = termlistAdd (leveltl[level], t); + + /* add to relevant list */ + switch (level) + { + case 0: + sys->locals = termlistAdd (sys->locals, t); + break; + case 1: + thisProtocol->locals = termlistAdd (thisProtocol->locals, t); + break; + case 2: + thisRole->locals = termlistAdd (thisRole->locals, t); + break; + } + } + return t; +} + +//! Generate a term from a symbol +Term +symbolDeclare (Symbol s, int isVar) +{ + return levelDeclare (s, isVar, level); +} + +Term +levelFind (Symbol s, int level) +{ + Termlist tl; + + tl = leveltl[level]; + while (tl != NULL) + { + if (isTermLeaf (tl->term)) + { + if (TermSymb (tl->term) == s) + { + return tl->term; + } + } + tl = tl->next; + } + return NULL; +} + +Term +symbolFind (Symbol s) +{ + int i; + Term t; + + i = level; + while (i >= 0) + { + t = levelFind (s, i); + if (t != NULL) + return t; + i--; + } + return NULL; +} + +//! Yield a basic global constant term (we suppose it exists) or NULL, given a string +Term +findGlobalConstant (const char *s) +{ + return levelFind (lookup (s), 0); +} + +void +defineUsertype (Tac tcdu) +{ + Tac tc; + Term t; + Term tfind; + + tc = tcdu->t1.tac; + + if (tc == NULL) + { + error ("Empty usertype declaration on line %i.", tcdu->lineno); + } + while (tc != NULL && tc->op == TAC_STRING) + { + /* check whether this term is already declared in the same way + * (i.e. as a type) */ + + tfind = levelFind (tc->t1.sym, 0); + if (tfind == NULL) + { + /* this is what we expected: this type is not declared yet */ + t = levelDeclare (tc->t1.sym, 0, 0); + t->stype = termlistAdd (NULL, TERM_Type); + } + else + { + /* oi!, there's already one. Let's hope is is a type too. */ + if (inTermlist (tfind->stype, TERM_Type)) + { + if (switches.check) + { + /* phew. warn anyway */ + globalError++; + eprintf ("warning: double declaration of usertype "); + termPrint (tfind); + eprintf ("\n"); + globalError--; + } + } + else + { + /* that's not right! */ + error + ("Conflicting definitions in usertype definition on line %i.", + tc->lineno); + } + } + tc = tc->next; + } +} + +//! Declare a variable at the current level +void +levelTacDeclaration (Tac tc, int isVar) +{ + Tac tscan; + Termlist typetl = NULL; + Term t; + int isAgent; + + // tscan contains the type list (as is const x,z: Term or var y: Term,Ding) + tscan = tc->t2.tac; + if (!isVar && tscan->next != NULL) + { + error ("Multiple type definition for constant on line %i.", + tscan->lineno); + } + // scan the whole type info list + while (tscan != NULL && tscan->op == TAC_STRING) + { + /* apparently there is type info, termlist? */ + t = levelFind (tscan->t1.sym, 0); + + if (t == NULL) + { + /* not declared, that is unacceptable. */ + error ("Undeclared type on line %i.", tscan->lineno); + } + else + { + if (!inTermlist (t->stype, TERM_Type)) + { + error ("Non-type constant in type declaration on line %i.", + tscan->lineno); + } + } + typetl = termlistAdd (typetl, t); + tscan = tscan->next; + } + /* check whether the type list contains the agent type */ + isAgent = inTermlist (typetl, TERM_Agent); + + /* parse all constants and vars, because a single declaration can contain multiple ones */ + tscan = tc->t1.tac; + while (tscan != NULL) + { + /* declare this variable/constant with the previously derived type list */ + t = symbolDeclare (tscan->t1.sym, isVar); + t->stype = typetl; + /* local to the role? */ + if (level == 2) + { + if (isVar) + { + /* it is a role variable, so add it to the nicely declared variables */ + thisRole->declaredvars = + termlistAdd (thisRole->declaredvars, t); + } + else + { + /* it is a role constant, so add it to the nicely declared constants */ + thisRole->declaredconsts = + termlistAdd (thisRole->declaredconsts, t); + } + } + else if (level == 0) + { + sys->globalconstants = termlistAdd (sys->globalconstants, t); + if (isAgent) + { + sys->agentnames = termlistAdd (sys->agentnames, t); + } + } + tscan = tscan->next; + } +} + +//! Get last role def +Roledef +getLastRoledef (Roledef rd) +{ + if (rd != NULL) + { + while (rd->next != NULL) + { + rd = rd->next; + } + } + return rd; +} + +//! Mark last roledef lineno +void +markLastRoledef (Roledef rd, const int lineno) +{ + rd = getLastRoledef (rd); + rd->lineno = lineno; +} + + +//! Check whether a claim label already occurs +int +isClaimlabelUsed (const System sys, const Term label) +{ + Claimlist cl; + + if (label == NULL) + { + /* we assign this 'occurs' because it is an invalid label */ + return true; + } + cl = sys->claimlist; + while (cl != NULL) + { + if (isTermEqual (cl->label, label)) + { + return true; + } + cl = cl->next; + } + return false; +} + +//! Generate a fresh claim label +Term +generateFreshClaimlabel (const System sys, const Protocol protocol, + const Role role, const Term claim) +{ + Term label; + + /* Simply use the role as a prefix */ + label = freshTermPrefix (role->nameterm); + label = makeTermTuple (protocol->nameterm, label); + return label; +} + +//! Create a claim and add it to the claims list, and add the role event. +Claimlist +claimCreate (const System sys, const Protocol protocol, const Role role, + const Term claim, Term label, const Term msg, const int lineno) +{ + Claimlist cl; + + /* generate full unique label */ + /* is the label empty or used? */ + if (label == NULL || isClaimlabelUsed (sys, label)) + { + /* simply generate a fresh one */ + label = generateFreshClaimlabel (sys, protocol, role, claim); + } + + if (switches.filterProtocol != NULL) + { + // only this protocol + if (strcmp + (switches.filterProtocol, TermSymb (protocol->nameterm)->text) != 0) + { + // not this protocol; return + return NULL; + } + // and maybe also a specific label? + if (switches.filterLabel != NULL) + { + if (label == NULL) + { + return NULL; + } + else + { + Term t; + + t = label; + while (isTermTuple (t)) + { + t = TermOp2 (t); + } + if (strcmp (switches.filterLabel, TermSymb (t)->text) != 0) + { + // not this label; return + return NULL; + } + } + } + } + + // Assert: label is unique, add claimlist info + cl = malloc (sizeof (struct claimlist)); + cl->type = claim; + cl->label = label; + cl->parameter = msg; + cl->protocol = thisProtocol; + cl->rolename = role->nameterm; + cl->role = role; + cl->roledef = NULL; + cl->count = 0; + cl->complete = 0; + cl->timebound = 0; + cl->failed = 0; + cl->states = 0; + cl->prec = NULL; + cl->roles = NULL; + cl->alwaystrue = false; + cl->warnings = false; + cl->lineno = lineno; + + /* add the claim to the end of the current list */ + cl->next = NULL; + if (sys->claimlist == NULL) + { + sys->claimlist = cl; + } + else + { + Claimlist cl2; + + cl2 = sys->claimlist; + while (cl2->next != NULL) + { + cl2 = cl2->next; + } + cl2->next = cl; + } + + /* add the role event */ + role->roledef = roledefAdd (role->roledef, CLAIM, label, + role->nameterm, claim, msg, cl); + markLastRoledef (role->roledef, lineno); + + /* possible special handlers for each claim */ + + if (claim == CLAIM_Secret) + { + Termlist claimvars; + Termlist readvars; + + /* now check whether the claim contains variables that can actually be influenced by the intruder */ + + claimvars = termlistAddVariables (NULL, msg); + readvars = compute_read_variables (thisRole); + while (claimvars != NULL) + { + if (!inTermlist (readvars, claimvars->term)) + { + /* this claimvar does not occur in the reads? */ + /* then we should ignore it later */ + cl->alwaystrue = true; + cl->warnings = true; + + /* show a warning for this */ + globalError++; + eprintf ("warning: secrecy claim of role "); + termPrint (cl->rolename); + eprintf (" contains a variable "); + termPrint (claimvars->term); + eprintf + (" which is never read; therefore the claim will be true.\n"); + globalError--; + } + claimvars = claimvars->next; + } + } + return cl; +} + +//! Parse a communication event tc of type event, and add a role definition event for it. +void +commEvent (int event, Tac tc) +{ + /* Add an event to the roledef, send or read */ + Claimlist cl; + Term fromrole = NULL; + Term torole = NULL; + Term msg = NULL; + Term label = NULL; + Term claim = NULL; + Term claimbig = NULL; + int n = 0; + Tac trip; + Labelinfo linfo; + + /* Construct label, if any */ + if (tc->t1.sym == NULL) + { + /* right, now this should not be NULL anyway, if so we construct a fresh one. + * This can be a weird choice if it is a read or send, because in that case + * we cannot chain them anymore and the send-read correspondence is lost. + */ + label = freshTermPrefix (thisRole->nameterm); + } + else + { + label = levelFind (tc->t1.sym, level - 1); + if (label == NULL) + { + /* effectively, labels are bound to the protocol */ + level--; + /* leaves a garbage tuple. dunnoh what to do with it */ + label = levelConst (tc->t1.sym); + level++; + } + else + { + /* leaves a garbage tuple. dunnoh what to do with it */ + } + } + label = makeTermTuple (thisProtocol->nameterm, label); + + /** + * Parse the specific event type + */ + trip = tc->t2.tac; + switch (event) + { + case READ: + case SEND: + /** + * We know the label. Find the corresponding labelinfo bit or make a new one + */ + linfo = label_find (sys->labellist, label); + if (linfo == NULL) + { + /* Not found, make a new one */ + linfo = label_create (label, thisProtocol); + sys->labellist = list_append (sys->labellist, linfo); + } + + /* now parse triplet info */ + if (trip == NULL || trip->next == NULL || trip->next->next == NULL) + { + error ("Problem with %i event on line %i.", event, tc->lineno); + } + fromrole = tacTerm (trip); + torole = tacTerm (trip->next); + msg = tacTerm (tacTuple ((trip->next->next))); + cl = NULL; + + if (event == SEND) + { + /* set sendrole */ + if (!isTermEqual (fromrole, thisRole->nameterm)) + error + ("Send role does not correspond to execution role at line %i.", + tc->lineno); + if (linfo->sendrole != NULL) + error ("Label defined twice for sendrole!"); + linfo->sendrole = fromrole; + + /* set keylevels based on send events */ + term_set_keylevels (fromrole); + term_set_keylevels (torole); + term_set_keylevels (msg); + } + else + { + // READ + /* set readrole */ + if (!isTermEqual (torole, thisRole->nameterm)) + error + ("Read role does not correspond to execution role at line %i.", + tc->lineno); + if (linfo->readrole != NULL) + error ("Label defined twice for readrole!"); + linfo->readrole = torole; + } + + /* and make that read/send event */ + thisRole->roledef = roledefAdd (thisRole->roledef, event, label, + fromrole, torole, msg, cl); + /* mark last one with line number */ + markLastRoledef (thisRole->roledef, tc->lineno); + break; + + case CLAIM: + /* switch can be used to remove all *parsed* claims */ + if (!switches.removeclaims) + { + /* now parse tuple info */ + if (trip == NULL || trip->next == NULL) + { + error ("Problem with claim %i event on line %i.", event, + tc->lineno); + } + fromrole = tacTerm (trip); + claimbig = tacTerm (tacTuple ((trip->next))); + /* check for several types */ + claim = tupleProject (claimbig, 0); + torole = claim; + + /* check for obvious flaws */ + if (claim == NULL) + { + error ("Invalid claim specification on line %i.", tc->lineno); + } + if (!inTermlist (claim->stype, TERM_Claim)) + { + globalError++; + eprintf ("error: [%i] claim term is not of claim type ", + trip->next->lineno); + termPrint (claim); + errorTac (trip->next->lineno); + globalError--; + } + /* unfold parameters to msg */ + msg = NULL; + n = tupleCount (claimbig) - 1; + if (n < 1) + { + /* no parameters */ + n = 0; + } + else + { + /* n parameters */ + msg = TermOp2 (deVar (claimbig)); + if (tupleCount (msg) != n) + { + error ("Problem with claim tuple unfolding at line %i.", + trip->next->lineno); + } + } + + // check whether label is unique + + if (isClaimlabelUsed (sys, label)) + { + if (switches.check) + { + warning + ("Claim label is not unique at line %i, generating fresh label.", + tc->lineno); + } + // the reported new label will be generated later in claimCreate() + } + + if (!isTermEqual (fromrole, thisRole->nameterm)) + error + ("Claim role does not correspond to execution role at line %i.", + tc->lineno); + + /* handles claim types with different syntactic claims */ + + if (claim == CLAIM_Secret) + { + if (n == 0) + { + error + ("Secrecy claim requires a list of terms to be secret on line %i.", + trip->next->lineno); + } + if (n > 1) + { + error + ("Secrecy claim on line %i should not contain tuples (for Arachne) until it is officially supported.", + trip->next->lineno); + } + } + if (claim == CLAIM_Nisynch) + { + if (n != 0) + { + error ("NISYNCH claim requires no parameters at line %i.", + trip->next->lineno); + } + } + if (claim == CLAIM_Niagree) + { + if (n != 0) + { + error ("NIAGREE claim requires no parameters at line %i.", + trip->next->lineno); + } + } + + /* create the event */ + + cl = + claimCreate (sys, thisProtocol, thisRole, claim, label, msg, + tc->lineno); + } + break; + } +} + +int +normalDeclaration (Tac tc) +{ + switch (tc->op) + { + case TAC_VAR: + levelDeclareVar (tc); + if (level < 2 && tc->t3.tac == NULL) + knowledgeAddTermlist (sys->know, tacTermlist (tc->t1.tac)); + break; + case TAC_CONST: + levelDeclareConst (tc); + if (level < 2 && tc->t3.tac == NULL) + knowledgeAddTermlist (sys->know, tacTermlist (tc->t1.tac)); + break; + case TAC_SECRET: + levelDeclareConst (tc); + break; + case TAC_COMPROMISED: + knowledgeAddTermlist (sys->know, tacTermlist (tc->t1.tac)); + break; + case TAC_INVERSEKEYS: + knowledgeAddInverse (sys->know, tacTerm (tc->t1.tac), + tacTerm (tc->t2.tac)); + break; + default: + /* abort with false */ + return 0; + } + return 1; +} + +//! Add all sorts of claims to this role +void +claimAddAll (const System sys, const Protocol protocol, const Role role) +{ + /* first: secrecy claims for all locally declared things */ + void addSecrecyList (Termlist tl) + { + while (tl != NULL) + { + Term t; + + t = deVar (tl->term); + if (realTermLeaf (t)) + { + // Add a secrecy claim + claimCreate (sys, protocol, role, CLAIM_Secret, NULL, t, -1); + } + tl = tl->next; + } + } + + addSecrecyList (role->declaredconsts); + addSecrecyList (role->declaredvars); + + /* full non-injective agreement and ni-synch */ + claimCreate (sys, protocol, role, CLAIM_Niagree, NULL, NULL, -1); + claimCreate (sys, protocol, role, CLAIM_Nisynch, NULL, NULL, -1); +} + +//! Compile a role +/** + * Input: a name and a roledef tac + * + * Upon return, thisRole should contain the role definition + */ +void +roleCompile (Term nameterm, Tac tc) +{ + /* locate the role, protocol into thisRole */ + /* scan through role list */ + thisRole = thisProtocol->roles; + while (thisRole != NULL && !isTermEqual (thisRole->nameterm, nameterm)) + { + thisRole = thisRole->next; + } + if (thisRole == NULL) + { + globalError++; + eprintf ("error: [%i] undeclared role name ", tc->lineno); + termPrint (nameterm); + eprintf (" in line "); + errorTac (tc->lineno); + } + + /* parse the content of the role */ + levelInit (); + + { + int firstEvent; + + /* initiator/responder flag not set */ + firstEvent = 1; + + while (tc != NULL) + { + switch (tc->op) + { + case TAC_READ: + if (firstEvent) + { + // First a read, thus responder + /* + * Semantics: defaults (in role.c) to initiator _unless_ the first event is a read, + * in which case we assume that the agent names are possibly received as variables + */ + thisRole->initiator = 0; + firstEvent = 0; + } + commEvent (READ, tc); + break; + case TAC_SEND: + firstEvent = 0; + commEvent (SEND, tc); + break; + case TAC_CLAIM: + commEvent (CLAIM, tc); + break; + case TAC_KNOWS: + roleKnows (tc); + break; + default: + if (!normalDeclaration (tc)) + { + globalError++; + eprintf ("error: [%i] illegal command %i in role ", + tc->lineno, tc->op); + termPrint (thisRole->nameterm); + eprintf (" "); + errorTac (tc->lineno); + } + break; + } + tc = tc->next; + } + } + + /* add any claims according to the switches */ + + if (switches.addreachableclaim) + { + claimCreate (sys, thisProtocol, thisRole, CLAIM_Reachable, NULL, NULL, + -1); + } + if (switches.addallclaims) + { + claimAddAll (sys, thisProtocol, thisRole); + } + + /* last bits */ + compute_role_variables (sys, thisProtocol, thisRole); + levelDone (); +} + +//! Initial role knowledge declaration +void +roleKnows (Tac tc) +{ + sys->knowledgedefined = true; // apparently someone uses this, so we enable the check + thisRole->knows = + termlistConcat (thisRole->knows, tacTermlist (tc->t1.tac)); +} + +void +runInstanceCreate (Tac tc) +{ + /* create an instance of an existing role + * tac1 is the dot-separated reference to the role. + * tac2 is the list of parameters to be filled in. + */ + + Protocol p; + Role r; + Symbol psym, rsym; + Termlist instParams; + + /* check whether we can still do it */ + if (sys->maxruns >= maxruns) + return; + + /* first, locate the protocol */ + psym = tc->t1.tac->t1.sym; + p = sys->protocols; + while (p != NULL && TermSymb (p->nameterm) != psym) + p = p->next; + if (p == NULL) + { + globalError++; + eprintf + ("error: [%i] Trying to create a run of a non-declared protocol ", + tc->lineno); + symbolPrint (psym); + eprintf (" "); + errorTac (tc->lineno); + } + + /* locate the role */ + rsym = tc->t1.tac->t2.sym; + r = p->roles; + while (r != NULL && TermSymb (r->nameterm) != rsym) + r = r->next; + if (r == NULL) + { + globalError++; + eprintf ("error: [%i] Protocol ", tc->lineno); + symbolPrint (psym); + eprintf (" has no role called "); + symbolPrint (rsym); + eprintf (" "); + errorTac (tc->lineno); + } + + /* we now know what we are instancing, equal numbers? */ + instParams = tacTermlist (tc->t2.tac); + if (termlistLength (instParams) != termlistLength (p->rolenames)) + { + globalError++; + eprintf + ("error: [%i] Run instance has different number of parameters than protocol ", + tc->lineno); + termPrint (p->nameterm); + eprintf (" "); + errorTac (tc->lineno); + } + + /* equal numbers, so it seems to be safe */ + roleInstance (sys, p, r, instParams, NULL); // technically, we don't need to do this for Arachne [fix later] + + /* after creation analysis */ + /* originator assumption for CLP ? */ + /* TODO */ +} + +//! Check whether the roles in a protocol are non-empty +void +checkProtocolRoles (void) +{ + Role role; + Termlist badroles; + + badroles = NULL; + role = thisProtocol->roles; + while (role != NULL) + { + if (role->roledef == NULL) + { + // Hey, this role is empty. + badroles = termlistAdd (badroles, role->nameterm); + } + role = role->next; + } + + if (badroles != NULL) + { + globalError++; + eprintf ("warning: protocol "); + termPrint (thisProtocol->nameterm); + eprintf (" has empty role definitions for the roles: "); + termlistPrint (badroles); + eprintf ("\n"); + globalError--; + termlistDelete (badroles); + } +} + +//! Compile a protocol description +void +protocolCompile (Symbol prots, Tac tc, Tac tcroles) +{ + Protocol pr; + Term t; + + /* make new (empty) current protocol with name */ + pr = protocolCreate (levelConst (prots)); + thisProtocol = pr; + { + // check for double name declarations + Protocol prold; + + prold = sys->protocols; + while (prold != NULL) + { + if (isTermEqual (pr->nameterm, prold->nameterm)) + { + globalError++; + eprintf ("error: [%i] Double declaration of protocol ", + tc->lineno); + symbolPrint (prots); + eprintf (" "); + errorTac (tc->lineno); + } + prold = prold->next; + } + } + + /* add protocol to list */ + pr->next = sys->protocols; + sys->protocols = pr; + protocolCount++; + + levelInit (); + /* add the role names */ + pr->rolenames = NULL; + while (tcroles != NULL) + { + Term rolename; + Role r; + + rolename = levelVar (tcroles->t1.sym); + rolename->stype = termlistAdd (NULL, TERM_Agent); + + /* add name to list of role names */ + pr->rolenames = termlistAppend (pr->rolenames, rolename); + /* make new (empty) current protocol with name */ + r = roleCreate (rolename); + /* add role to role list of the protocol */ + r->next = thisProtocol->roles; + thisProtocol->roles = r; + + /* next role name */ + tcroles = tcroles->next; + } + + /* parse the content of the protocol */ + while (tc != NULL) + { + switch (tc->op) + { + case TAC_UNTRUSTED: + sys->untrusted = + termlistConcat (sys->untrusted, tacTermlist (tc->t1.tac)); + break; + case TAC_ROLE: + t = levelFind (tc->t1.sym, level); + if (t != NULL) + { + // Compile a role + roleCompile (t, tc->t2.tac); + // singular? + if (tc->t3.value != 0) + { + thisRole->singular = true; + } + } + else + { + globalError++; + eprintf ("warning: undeclared role name"); + symbolPrint (tc->t1.sym); + eprintf (" in protocol "); + termPrint (pr->nameterm); + globalError--; + } + break; + default: + if (!normalDeclaration (tc)) + { + globalError++; + eprintf ("error: [%i] illegal command %i in protocol ", + tc->lineno, tc->op); + termPrint (thisProtocol->nameterm); + errorTac (tc->lineno); + } + break; + } + tc = tc->next; + } + + /* new we should have parsed each protocol role. check this. */ + checkProtocolRoles (); + + levelDone (); +} + +void +tacProcess (Tac tc) +{ + while (tc != NULL) + { + switch (tc->op) + { + case TAC_PROTOCOL: + protocolCompile (tc->t1.sym, tc->t2.tac, tc->t3.tac); + break; + case TAC_UNTRUSTED: + sys->untrusted = + termlistConcat (sys->untrusted, tacTermlist (tc->t1.tac)); + break; + case TAC_RUN: + runInstanceCreate (tc); + break; + case TAC_USERTYPE: + defineUsertype (tc); + break; + default: + if (!normalDeclaration (tc)) + { + globalError++; + eprintf ("error: [%i] illegal command %i at the global level ", + tc->lineno, tc->op); + errorTac (tc->lineno); + } + break; + } + tc = tc->next; + } +} + +Term +tacTerm (Tac tc) +{ + switch (tc->op) + { + case TAC_ENCRYPT: + return makeTermEncrypt (tacTerm (tc->t1.tac), tacTerm (tc->t2.tac)); + case TAC_TUPLE: + return makeTermTuple (tacTerm (tc->t1.tac), tacTerm (tc->t2.tac)); + case TAC_STRING: + { + Term t = symbolFind (tc->t1.sym); + if (t == NULL) + { + globalError++; + eprintf ("error: [%i] undeclared symbol ", tc->lineno); + symbolPrint (tc->t1.sym); + errorTac (tc->lineno); + } + return t; + } + default: + return NULL; + } +} + +Termlist +tacTermlist (Tac tc) +{ + Termlist tl = NULL; + + while (tc != NULL) + { + tl = termlistAppend (tl, tacTerm (tc)); + tc = tc->next; + } + return tl; +} + +//! Compute variables for a roles (for Arachne) +void +compute_role_variables (const System sys, Protocol p, Role r) +{ + if (r->variables == NULL) + { + // Not computed before, for some reason + Termlist tl; + + int process_event (Roledef rd) + { + tl = termlistAddVariables (tl, rd->from); + tl = termlistAddVariables (tl, rd->to); + tl = termlistAddVariables (tl, rd->message); + return 1; + } + + tl = NULL; + roledef_iterate_events (r->roledef, process_event); + r->variables = tl; + +#ifdef DEBUG + if (DEBUGL (5)) + { + eprintf ("All variables for role "); + termPrint (r->nameterm); + eprintf (" are "); + termlistPrint (tl); + eprintf ("\n"); + } +#endif + } +} + +//! Compute term list of rolenames involved in a given term list of labels +Termlist +compute_label_roles (Termlist labels) +{ + Termlist roles; + + roles = NULL; + while (labels != NULL) + { + Labelinfo linfo; + + linfo = label_find (sys->labellist, labels->term); +#ifdef DEBUG + if (linfo == NULL) + error ("Label in prec list not found in label info list"); +#endif + roles = termlistAddNew (roles, linfo->sendrole); + roles = termlistAddNew (roles, linfo->readrole); + + labels = labels->next; + } + return roles; +} + +//! Order the label roles for a given claim +void +order_label_roles (const Claimlist cl) +{ + Termlist roles_remaining; + Termlist roles_ordered; + int distance; + +#ifdef DEBUG + if (DEBUGL (4)) + { + eprintf ("Ordering label roles for claim "); + termPrint (cl->label); + eprintf ("; 0: "); + termPrint (cl->rolename); + } +#endif + roles_remaining = termlistShallow (cl->roles); + roles_ordered = termlistAdd (NULL, cl->rolename); + roles_remaining = + termlistDelTerm (termlistFind (roles_remaining, cl->rolename)); + + distance = 0; + while (roles_remaining != NULL) + { + int scan_label (void *data) + { + Labelinfo linfo; + Termlist tl; + + linfo = (Labelinfo) data; + if (linfo == NULL) + return 1; + tl = cl->prec; + if (inTermlist (tl, linfo->label)) + { + if (linfo->protocol == cl->protocol) + { + // If it's not the same protocol, the labels can't match + + // This function checks whether the newrole can connect to the connectedrole, and whether they fulfil their requirements. + void roles_test (const Term connectedrole, const Term newrole) + { + if (inTermlist (roles_ordered, connectedrole) && + inTermlist (roles_remaining, newrole)) + { +#ifdef DEBUG + if (DEBUGL (4)) + { + eprintf (" "); + termPrint (newrole); + } +#endif + roles_ordered = termlistAppend (roles_ordered, newrole); + roles_remaining = + termlistDelTerm (termlistFind + (roles_remaining, newrole)); + } + } + + roles_test (linfo->sendrole, linfo->readrole); + roles_test (linfo->readrole, linfo->sendrole); + } + } + return 1; + } + + distance++; +#ifdef DEBUG + if (DEBUGL (4)) + { + eprintf (" %i:", distance); + } +#endif + list_iterate (sys->labellist, scan_label); + } + cl->roles = roles_ordered; +#ifdef DEBUG + if (DEBUGL (4)) + { + eprintf ("\n"); + } +#endif +} + +//! Compute prec() sets for each claim. +/** + * Generates two auxiliary structures. First, a table that contains + * a mapping from all events to event/claim labels. + * A second table is used to compute the precedence order, and + * Warshall's algorithm is used to compute the transitive closure. + * Then, for each claim, the in the preceding labels occurring roles are stored, + * which is useful later. + *@returns For each claim in the claim list, a preceding label set is defined. + */ +void +compute_prec_sets (const System sys) +{ + Term *eventlabels; // array: maps events to labels + unsigned int *prec; // array: maps event*event to precedence + int size; // temp constant: rolecount * roleeventmax + int rowsize; + int r1, r2, ev1, ev2; // some counters + Claimlist cl; + + // Assist: compute index from role, lev + int index (int r, int lev) + { + return r * sys->roleeventmax + lev; + } + + // Assist: yield roledef from r, lev + Roledef roledef_re (int r, int lev) + { + Protocol pr; + Role ro; + Roledef rd; + + pr = sys->protocols; + ro = pr->roles; + while (r > 0 && ro != NULL) + { + ro = ro->next; + if (ro == NULL) + { + pr = pr->next; + if (pr != NULL) + { + ro = pr->roles; + } + else + { + ro = NULL; + } + } + r--; + } + if (ro != NULL) + { + rd = ro->roledef; + while (lev > 0 && rd != NULL) + { + rd = rd->next; + lev--; + } + return rd; + } + else + { + return NULL; + } + } + + // Assist: print matrix + void show_matrix (void) + { + int r1, r2, ev1, ev2; + + r1 = 0; + while (r1 < sys->rolecount) + { + ev1 = 0; + while (ev1 < sys->roleeventmax) + { + eprintf ("prec %i,%i: ", r1, ev1); + r2 = 0; + while (r2 < sys->rolecount) + { + ev2 = 0; + while (ev2 < sys->roleeventmax) + { + eprintf ("%i ", + BIT (prec + rowsize * index (r2, ev2), + index (r1, ev1))); + ev2++; + } + eprintf (" "); + r2++; + } + eprintf ("\n"); + ev1++; + } + eprintf ("\n"); + r1++; + } + eprintf ("\n"); + } + + /* + * Phase 1: Allocate structures and map to labels + */ + //eprintf ("Rolecount: %i\n", sys->rolecount); + //eprintf ("Maxevent : %i\n", sys->roleeventmax); + size = sys->rolecount * sys->roleeventmax; + rowsize = WORDSIZE (size); + eventlabels = malloc (size * sizeof (Term)); + prec = (unsigned int *) CALLOC (1, rowsize * size * sizeof (unsigned int)); + // Assign labels + r1 = 0; + while (r1 < sys->rolecount) + { + Roledef rd; + + ev1 = 0; + rd = roledef_re (r1, ev1); + while (rd != NULL) + { + eventlabels[index (r1, ev1)] = rd->label; + //termPrint (rd->label); + //eprintf ("\t"); + ev1++; + rd = rd->next; + } + while (ev1 < sys->roleeventmax) + { + eventlabels[index (r1, ev1)] = NULL; + ev1++; + } + //eprintf ("\n"); + r1++; + } + // Set simple precedence (progress within a role) + r1 = 0; + while (r1 < sys->rolecount) + { + ev1 = 1; + while (ev1 < (sys->roleeventmax)) + { + SETBIT (prec + rowsize * index (r1, ev1 - 1), index (r1, ev1)); + ev1++; + } + r1++; + } + // Scan for label correspondence + r1 = 0; + while (r1 < sys->rolecount) + { + ev1 = 0; + while (ev1 < sys->roleeventmax) + { + Roledef rd1; + + rd1 = roledef_re (r1, ev1); + if (rd1 != NULL && rd1->type == SEND) + { + r2 = 0; + while (r2 < sys->rolecount) + { + ev2 = 0; + while (ev2 < sys->roleeventmax) + { + Roledef rd2; + + rd2 = roledef_re (r2, ev2); + if (rd2 != NULL && rd2->type == READ + && isTermEqual (rd1->label, rd2->label)) + { + SETBIT (prec + rowsize * index (r1, ev1), + index (r2, ev2)); + } + ev2++; + } + r2++; + } + } + ev1++; + } + r1++; + } + +#ifdef DEBUG + if (DEBUGL (5)) + { + show_matrix (); + } +#endif + + /* + * Compute transitive closure (Warshall). + */ + transitive_closure (prec, size); + +#ifdef DEBUG + if (DEBUGL (5)) + { + show_matrix (); + } +#endif + + /* + * Last phase: Process all individual claims + */ + cl = sys->claimlist; + while (cl != NULL) + { + Roledef rd; + Term label; + int claim_index; + + label = cl->label; + // Locate r,lev from label, requires (TODO) unique labeling of claims! + r1 = 0; + ev1 = -1; + do + { + ev1++; + if (ev1 == sys->roleeventmax) + { + ev1 = 0; + r1++; + } + } + while (r1 < sys->rolecount + && !isTermEqual (label, eventlabels[index (r1, ev1)])); + + if (r1 == sys->rolecount) + { + error + ("Prec() setup: Could not find the event corresponding to a claim label."); + } + rd = roledef_re (r1, ev1); + if (rd->type != CLAIM) + { + error + ("Prec() setup: First event with claim label doesn't seem to be a claim."); + } + // Store in claimlist structure + cl->r = r1; + cl->ev = ev1; + cl->roledef = rd; + + /* + * We have found the claim roledef, and r1,ev1 + * Now we compute the preceding label set + */ + cl->prec = NULL; // clear first + claim_index = index (r1, ev1); + r2 = 0; + while (r2 < sys->rolecount) + { + Roledef rd2; + + ev2 = 0; + rd = roledef_re (r2, ev2); + while (rd != NULL) + { + if (BIT (prec + rowsize * index (r2, ev2), claim_index)) + { + // This event precedes the claim + + if (rd->type == READ) + { + // Only store read labels (but send would work as well) + cl->prec = termlistAdd (cl->prec, rd->label); + } + } + rd = rd->next; + ev2++; + } + r2++; + } + + /** + * ---------------------------------------- + * cl->prec is done, now we infer cl->roles + * Next, we nicely order them + * ---------------------------------------- + */ + + cl->roles = compute_label_roles (cl->prec); + order_label_roles (cl); + + /** + * --------------------------- + * Distinguish types of claims + * --------------------------- + */ + + // For ni-synch, the preceding label sets are added to the synchronising_labels sets. + if (cl->type == CLAIM_Nisynch) + { + Termlist tl_scan; + + tl_scan = cl->prec; + while (tl_scan != NULL) + { + sys->synchronising_labels = + termlistAddNew (sys->synchronising_labels, tl_scan->term); + tl_scan = tl_scan->next; + } + } + + // For ni-agree, the preceding set is also important, but we furthermore need a restricted + // synchronising_labels set + + //@todo Fix ni-agree synchronising label sets + if (cl->type == CLAIM_Niagree) + { + int r_scan; + + // Scan each role (except the current one) and pick out the last prec events. + r_scan = 0; + while (r_scan < sys->rolecount) + { + // Only other roles + if (r_scan != r1) + { + // Scan fully + int ev_scan; + Term t_buf; + + t_buf = NULL; + ev_scan = 0; + while (ev_scan < sys->roleeventmax) + { + // if this event preceds the claim, replace the label term + if (BIT + (prec + rowsize * index (r_scan, ev_scan), + claim_index)) + { + Roledef rd; + + rd = roledef_re (r_scan, ev_scan); + if (rd->label != NULL) + { + t_buf = rd->label; + } + } + ev_scan++; + } + // Store only the last label + if (t_buf != NULL) + { + sys->synchronising_labels = + termlistAddNew (sys->synchronising_labels, t_buf); + } + } + r_scan++; + } + } + +#ifdef DEBUG + // Porparam = 100 (weirdness) [x][cc][debug] can turn of the synchronising label sets (override). + if (switches.switchP == 100) + { + termlistDelete (sys->synchronising_labels); + sys->synchronising_labels = NULL; + warning + ("Emptied synchronising labels set manually because --pp=100."); + } +#endif + // Check for empty stuff + //@todo This is for debugging, mainly. + if (cl->prec == NULL) + { + if (inTermlist (CLAIMS_dep_prec, cl->type)) + { + /* this claim depends on prec, but it is empty! */ + + cl->warnings = true; + globalError++; + eprintf ("warning: claim with label "); + termPrint (cl->label); + eprintf (" of role "); + termPrint (cl->rolename); + eprintf (" has an empty prec() set.\n"); + globalError--; + } + } + else + { +#ifdef DEBUG + if (DEBUGL (3)) + { + Protocol p; + + eprintf ("Preceding label set for r:%i, ev:%i = ", r1, ev1); + termlistPrint (cl->prec); + eprintf (", involving roles "); + termlistPrint (cl->roles); + eprintf (", from protocol "); + p = (Protocol) cl->protocol; + termPrint (p->nameterm); + eprintf ("\n"); + } +#endif + } + + // Proceed to next claim + cl = cl->next; + } + + /* + * Cleanup + */ + free (eventlabels); + FREE (prec); + +#ifdef DEBUG + if (DEBUGL (2)) + { + eprintf ("Synchronising labels set: "); + termlistPrint (sys->synchronising_labels); + eprintf ("\n"); + } +#endif + +} + +//! Check unused variables +void +checkRoleVariables (const System sys, const Protocol p, const Role r) +{ + Termlist vars; + Termlist declared; + + int process_event (Roledef rd) + { + if (rd->type == READ) + { + vars = termlistAddVariables (vars, rd->from); + vars = termlistAddVariables (vars, rd->to); + vars = termlistAddVariables (vars, rd->message); + } + return 1; + } + + /* Gather all variables occurring in the reads */ + vars = NULL; + roledef_iterate_events (r->roledef, process_event); + + /* Now, all variables for this role should be in the reads */ + declared = r->declaredvars; + while (declared != NULL) + { + if (!inTermlist (vars, declared->term)) + { + if (switches.check) + { + // Warning + globalError++; + eprintf ("warning: variable "); + termPrint (declared->term); + eprintf (" was declared in role "); + termPrint (p->nameterm); + eprintf (","); + termPrint (r->nameterm); + eprintf (" but never used in a read event.\n"); + globalError--; + } + } + declared = declared->next; + } + + termlistDelete (vars); +} + +//! Check unused variables +/** + * This is checked per role + */ +void +checkUnusedVariables (const System sys) +{ + Protocol p; + + p = sys->protocols; + while (p != NULL) + { + Role r; + r = p->roles; + while (r != NULL) + { + checkRoleVariables (sys, p, r); + r = r->next; + } + p = p->next; + } +} + +//! Is a complete role well-formed +int +WellFormedRole (const System sys, Protocol p, Role r) +{ + Knowledge know; + int okay; + Roledef rd; + + okay = true; + know = emptyKnowledge (); + // Transfer inverses + know->inverses = sys->know->inverses; + // Add role knowledge + knowledgeAddTermlist (know, r->knows); + // Add role names + //@TODO this is not in the semantics as such, often implicit + knowledgeAddTermlist (know, p->rolenames); + // Add local constants + //@TODO this is not in the semantics as such, often implicit + knowledgeAddTermlist (know, r->declaredconsts); + + // Test + rd = r->roledef; + while (rd != NULL) + { + Knowledge knowres; + + knowres = WellFormedEvent (r->nameterm, know, rd); + if (knowres == NULL) + { + okay = false; + break; + } + else + { + know = knowres; + rd = rd->next; + } + } + + // clean up + knowledgeDelete (know); + return okay; +} + +//! Well-formedness check +void +checkWellFormed (const System sys) +{ + int thisRole (Protocol p, Role r) + { + WellFormedRole (sys, p, r); + return true; + } + + iterateRoles (sys, thisRole); +} + +//! Check matching role defs +int +checkEventMatch (const Roledef rd1, const Roledef rd2, + const Termlist rolenames) +{ + if (!isTermEqual (rd1->from, rd2->from)) + { + return false; + } + if (!isTermEqual (rd1->to, rd2->to)) + { + return false; + } + if (!checkRoletermMatch (rd1->message, rd2->message, rolenames)) + { + return false; + } + return true; +} + +//! Check label matchup for protocol p,r, roledef rd (which is a read) +/** + * Any send with the same label should match + */ +void +checkLabelMatchThis (const System sys, const Protocol p, const Role readrole, + const Roledef readevent) +{ + Role sendrole; + int found; + + found = 0; + sendrole = p->roles; + while (sendrole != NULL) + { + Roledef event; + + event = sendrole->roledef; + while (event != NULL) + { + if (event->type == SEND) + { + if (isTermEqual (event->label, readevent->label)) + { + // Same labels, so they should match up! + if (!checkEventMatch (event, readevent, p->rolenames)) + { + globalError++; + eprintf ("error: [%i]", readevent->lineno); + if (sys->protocols != NULL) + { + if (sys->protocols->next != NULL) + { + eprintf (" Protocol "); + termPrint (sys->protocols->nameterm); + } + } + eprintf (" events for label "); + termPrint (event->label); + eprintf (" do not match, in particular: \n"); + eprintf ("error: [%i] ", event->lineno); + roledefPrint (event); + eprintf (" does not match\n"); + eprintf ("error: [%i] ", readevent->lineno); + roledefPrint (readevent); + eprintf ("\n"); + error_die (); + globalError--; + } + else + { + found++; +#ifdef DEBUG + if (DEBUGL (2)) + { + eprintf ("Matching up label "); + termPrint (event->label); + eprintf (" to match: "); + roledefPrint (event); + eprintf (" <> "); + roledefPrint (readevent); + eprintf ("\n"); + } +#endif + } + } + } + event = event->next; + } + sendrole = sendrole->next; + } + + /* How many did we find? + * 1 is normal, more is interesting (branching?) + * 0 is not good, nobody will send it + */ + if (found == 0) + { + globalError++; + eprintf ("error: [%i] for the read event ", readevent->lineno); + roledefPrint (readevent); + eprintf (" of protocol "); + termPrint (p->nameterm); + eprintf + (" there is no corresponding send event (with the same label and matching content). Start the label name with '!' if this is intentional.\n"); + error_die (); + globalError--; + } +} + +//! Check label matchup for protocol p +void +checkLabelMatchProtocol (const System sys, const Protocol p) +{ + // For each read label the sends should match + Role r; + + r = p->roles; + while (r != NULL) + { + Roledef rd; + + rd = r->roledef; + while (rd != NULL) + { + if (rd->type == READ) + { + // We don't check all, if they start with a bang we ignore them. + Labelinfo li; + + li = label_find (sys->labellist, rd->label); + if (li != NULL) + { + if (!li->ignore) + { + checkLabelMatchThis (sys, p, r, rd); + } + } + else + { + globalError++; + eprintf + ("error: [%i] cannot determine label information for ", + rd->lineno); + roledefPrint (rd); + eprintf ("\n"); + error_die (); + globalError--; + } + } + rd = rd->next; + } + r = r->next; + } +} + +//! Check label matchup +void +checkLabelMatching (const System sys) +{ + Protocol p; + + // For each protocol + p = sys->protocols; + while (p != NULL) + { + checkLabelMatchProtocol (sys, p); + p = p->next; + } +} + +//! Preprocess after system compilation +void +preprocess (const System sys) +{ + /* + * init some counters + */ + sys->rolecount = compute_rolecount (sys); + sys->roleeventmax = compute_roleeventmax (sys); + /* + * compute preceding label sets + */ + compute_prec_sets (sys); + /* + * check whether labels match up + */ + checkLabelMatching (sys); + /* + * check for ununsed variables + */ + if (switches.check) + { + checkUnusedVariables (sys); + } + /* + * compute hidelevels + */ + hidelevelCompute (sys); + /* + * Initial knowledge + */ + if (sys->knowledgedefined) + { + initialIntruderKnowledge (sys); + } + /* + * Check well-formedness + */ + if (sys->knowledgedefined) + { + checkWellFormed (sys); + } +} diff --git a/gui/src/compiler.h b/gui/src/compiler.h new file mode 100644 index 0000000..c6dc011 --- /dev/null +++ b/gui/src/compiler.h @@ -0,0 +1,26 @@ +#ifndef COMPILER +#define COMPILER + +#include "tac.h" +#include "role.h" +#include "system.h" + +void compilerInit (const System sys); +void compilerDone (void); + +void compile (Tac tc, int maxruns); +void preprocess (const System sys); +Term findGlobalConstant (const char *s); +Term makeGlobalConstant (const char *s); +Term makeGlobalVariable (const char *s); +void compute_role_variables (const System sys, Protocol p, Role r); + +Term symbolDeclare (Symbol s, int isVar); +void levelTacDeclaration (Tac tc, int isVar); + +#define levelDeclareVar(s) levelTacDeclaration(s,1) +#define levelDeclareConst(s) levelTacDeclaration(s,0) +#define levelVar(s) symbolDeclare(s,1) +#define levelConst(s) symbolDeclare(s,0) + +#endif diff --git a/gui/src/copy2gui.sh b/gui/src/copy2gui.sh new file mode 100755 index 0000000..c4ffda6 --- /dev/null +++ b/gui/src/copy2gui.sh @@ -0,0 +1,11 @@ +#!/bin/sh + +cp scyther-linux ../gui/Scyther/Bin +cp scyther-w32.exe ../gui/Scyther/Bin +cp scyther-mac ../gui/Scyther/Bin + +# bonus... +cp scyther-linux ~/bin + +echo Copied the files to their respective locations and ~/bin + diff --git a/gui/src/cost.c b/gui/src/cost.c new file mode 100644 index 0000000..cf0d5e2 --- /dev/null +++ b/gui/src/cost.c @@ -0,0 +1,74 @@ +/** + * + *@file cost.c + * + * Determine cost of a given semitrace in sys + * Constructed for Arachne results, unreliable otherwise. + * + */ +#include "switches.h" +#include "system.h" +#include "binding.h" +#include "error.h" +#include + +//************************************************************************ +// 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; +} diff --git a/gui/src/cost.h b/gui/src/cost.h new file mode 100644 index 0000000..75a09ae --- /dev/null +++ b/gui/src/cost.h @@ -0,0 +1,6 @@ +#ifndef COST +#define COST + +int attackCost (const System sys); + +#endif diff --git a/gui/src/debug.c b/gui/src/debug.c new file mode 100644 index 0000000..9a6aacf --- /dev/null +++ b/gui/src/debug.c @@ -0,0 +1,52 @@ +/** + *@file debug.c + *\brief Debugging code. + * + * It is hoped that this code will become redundant over time. + */ +#include +#include +#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 +} diff --git a/gui/src/debug.h b/gui/src/debug.h new file mode 100644 index 0000000..2e3253d --- /dev/null +++ b/gui/src/debug.h @@ -0,0 +1,10 @@ +#ifndef DEBUG_H +#define DEBUG_H + +void debugSet (int level); +int debugCond (int level); +void debug (int level, char *string); + +#define DEBUGL(a) debugCond(a) + +#endif diff --git a/gui/src/depend.c b/gui/src/depend.c new file mode 100644 index 0000000..6b9978f --- /dev/null +++ b/gui/src/depend.c @@ -0,0 +1,569 @@ +/** + * @file depend.c + * \brief interface for graph code from the viewpoint of events. + * + */ + +#include +#include +#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; +} diff --git a/gui/src/depend.h b/gui/src/depend.h new file mode 100644 index 0000000..d7ebfab --- /dev/null +++ b/gui/src/depend.h @@ -0,0 +1,44 @@ +#ifndef DEPEND +#define DEPEND + +#include "system.h" + +/* + * The code here mainly involves an interface for creating graphs etc., but + * most of it is implicit: we just add dependencies/runs and undo them again + * later. + */ + +void dependInit (const System sys); +void dependPrint (); +void dependDone (const System sys); + +/* + * The push code returns true or false: if false, the operation fails because + * it there is now a cycle in the graph, and there is no need to pop the + * result. + */ +void dependPushRun (const System sys); +void dependPopRun (); +int dependPushEvent (const int r1, const int e1, const int r2, const int e2); +void dependPopEvent (); + +/* + * Test/set + */ + +int getNode (const int n1, const int n2); +void setNode (const int n1, const int n2); +int isDependEvent (const int r1, const int e1, const int r2, const int e2); +void setDependEvent (const int r1, const int e1, const int r2, const int e2); + +/* + * Outside helpers + */ +int hasCycle (); +int eventNode (const int r, const int e); +int nodeCount (void); +int iteratePrecedingEvents (const System sys, int (*func) (int run, int ev), + const int run, const int ev); + +#endif diff --git a/gui/src/design.txt b/gui/src/design.txt new file mode 100644 index 0000000..97c40bb --- /dev/null +++ b/gui/src/design.txt @@ -0,0 +1,47 @@ +Design Issues for the Model Checker +----------------------------------- + +- For secrecy, we can trigger all sends at once. For synchronisation, + this is not the case. + +- Modules have to be split up sensibly. + + - Although 'knowledge' and 'term matching' seem to different items, + their intertwined workings suggest that they should be implemented + in parallel. + + - State generation (as in creating instances) might already allow for + a lot of static analysis. + +- We should make a list of required operations. Ingmar's work can serve + as a starting point. + +- For now, there will be no parser, and test cases will be input by + hand. + +- Synchronisation is more difficult to test, so we focus on secrecy + first. I've got some good ideas on Synchronisation testing though + (with narrowing sets of possible partners). Synchronisation is very + hard to prune, I presume. I have to prove that though ;) + +Sketch for secrecy: + +SimulateStep(F,M,constraints): + if Empty(F): + return + else: + for (s in PossibleSends): + add s.message to M + if (secrecy violated): + halt + remove s from F + ReadSets = supersetTransitions(F) + for (ReadSet in ReadSets): + for (s in ReadSet): + // dit is vaag + if NonMatch goto next ReadSet + constraint = F,M,match() + SimulateStep(F \ s,M,constraints) + + + diff --git a/gui/src/dotout.c b/gui/src/dotout.c new file mode 100644 index 0000000..2e7ba6e --- /dev/null +++ b/gui/src/dotout.c @@ -0,0 +1,1814 @@ +#include +#include +#include "system.h" +#include "switches.h" +#include "arachne.h" +#include "binding.h" +#include "depend.h" +#include "type.h" +#include "debug.h" +#include "error.h" + +extern Protocol INTRUDER; // Pointers, to be set by the Init of arachne.c +extern Role I_M; // Same here. +extern Role I_RRS; +extern Role I_RRSD; + +#define INVALID -1 +#define isGoal(rd) (rd->type == READ && !rd->internal) +#define isBound(rd) (rd->bound) +#define length step + +#define CLAIMTEXTCOLOR "#ffffff" +#define CLAIMCOLOR "#000000" +#define GOODCOMMCOLOR "forestgreen" + +#define INTRUDERCOLORH 18.0 +#define INTRUDERCOLORL 0.65 +#define INTRUDERCOLORS 0.9 +#define RUNCOLORL1 0.90 +#define RUNCOLORL2 0.65 +#define RUNCOLORH1 (INTRUDERCOLORH + 360 - 10.0) +#define RUNCOLORH2 (INTRUDERCOLORH + 10.0) +#define RUNCOLORS1 0.8 +#define RUNCOLORS2 0.6 +#define RUNCOLORDELTA 0.2 // maximum hue delta between roles (0.2): smaller means role colors of a protocol become more similar. +#define RUNCOLORCONTRACT 0.8 // contract from protocol edges: smaller means more distinction between protocols. +#define UNTRUSTEDCOLORS 0.4 + +#define CHOOSEWEIGHT "2.0" +#define RUNWEIGHT "10.0" +//#define CHOOSEWEIGHT "1.0" +//#define RUNWEIGHT "1.0" + +/* + * Dot output + * + * + * The algorithm itself is not very complicated; because the semi-bundles have + * bindings etcetera, a graph can be draw quickly and efficiently. + * + * Interesting issues: + * + * Binding annotations are only drawn if they don't connect with regular + * events, and when the item does not occur in any previous binding, it might + * be connected to the initial intruder knowledge. + * + * Color management is quite involved. We draw identical protocols in similar + * color schemes. A color scheme is a gradient between two colors, evenly + * spread over all the runs. + */ + +static System sys = NULL; + +/* + * code + */ + +//! Is this term chosen by the intruder? +int +isIntruderChoice (const Term t) +{ + if (realTermLeaf (t)) + { + if (TermRunid (t) >= sys->maxruns) + { + // Chosen by intruder + // However, if it is a rolename, this is not really what we mean + if (!(t->roleVar || isAgentType (t->stype))) + { + // Not a role variable, and chosen by the intruder: that's it + return true; + } + } + } + return false; +} + +//! Print the run identifier in some meaningful way +void +printVisualRunID (int rid) +{ + int run; + int displayi; + int displayr; + int display; + + if (rid < sys->maxruns) + { + // < sys->maxruns means normal thing (not from makeTraceConcrete) + displayi = 0; + displayr = 0; + for (run = 0; run < rid; run++) + { + if (sys->runs[run].protocol != INTRUDER) + { + displayr++; + } + else + { + displayi++; + } + } + if (sys->runs[rid].protocol == INTRUDER) + { + display = sys->maxruns + displayi + 1; + } + else + { + display = displayr + 1; + } + eprintf ("#%i", display); + } + else + { + eprintf ("%i", (rid - sys->maxruns + 1)); + } +} + +void +printVisualRun (const Term t) +{ + if (isIntruderChoice (t)) + { + eprintf ("Intruder"); + } + printVisualRunID (TermRunid (t)); +} + +//! Remap term stuff +void +termPrintRemap (const Term t) +{ + termPrintCustom (t, "", "", "(", ")", "\\{ ", " \\}", printVisualRun); +} + +//! Remap term list +void +termlistPrintRemap (Termlist tl, char *sep) +{ + while (tl != NULL) + { + termPrintRemap (tl->term); + tl = tl->next; + if (tl != NULL) + { + eprintf ("%s", sep); + } + } +} + +//! Print a term; if it is a variable, show that +void +explainVariable (Term t) +{ + t = deVar (t); + if (realTermVariable (t)) + { + eprintf ("any "); + if (t->roleVar) + { + eprintf ("agent "); + } + termPrintRemap (t); + if (!t->roleVar) + { + if (switches.match == 0 && t->stype != NULL) + { + Termlist tl; + + eprintf (" of type "); + for (tl = t->stype; tl != NULL; tl = tl->next) + { + termPrintRemap (tl->term); + if (tl->next != NULL) + { + eprintf (","); + } + } + } + } + } + else + { + termPrintRemap (t); + } +} + + +//! Name of intruder node +void +intruderNodeM0 (void) +{ + eprintf ("intruder"); +} + +//! Draw node +void +node (const System sys, const int run, const int index) +{ + if (sys->runs[run].protocol == INTRUDER) + { + if (sys->runs[run].role == I_M) + { + intruderNodeM0 (); + } + else + { + eprintf ("ri%i", run); + } + } + else + { + eprintf ("r%ii%i", run, index); + } +} + +//! Draw arrow +void +arrow (const System sys, Binding b) +{ + node (sys, b->run_from, b->ev_from); + eprintf (" -> "); + node (sys, b->run_to, b->ev_to); +} + +//! Redirect node +void +redirNode (const System sys, Binding b) +{ + eprintf ("redir_"); + node (sys, b->run_from, b->ev_from); + node (sys, b->run_to, b->ev_to); +} + +//! Roledef draw +void +roledefDraw (Roledef rd) +{ + void optlabel (void) + { + Term label; + + label = rd->label; + if (label != NULL) + { + if (realTermTuple (label)) + { + label = TermOp2 (label); + } + eprintf ("_"); + termPrintRemap (label); + } + } + + if (rd->type == READ) + { + eprintf ("read"); + optlabel (); + eprintf (" from "); + termPrintRemap (rd->from); + eprintf ("\\n"); + termPrintRemap (rd->message); + } + if (rd->type == SEND) + { + eprintf ("send"); + optlabel (); + eprintf (" to "); + termPrintRemap (rd->to); + eprintf ("\\n"); + termPrintRemap (rd->message); + } + if (rd->type == CLAIM) + { + eprintf ("claim"); + optlabel (); + eprintf ("\\n"); + termPrintRemap (rd->to); + if (rd->message != NULL) + { + eprintf (" : "); + termPrintRemap (rd->message); + } + } +} + +//! Choose term node +void +chooseTermNode (const Term t) +{ + eprintf ("CHOOSE"); + { + char *rsbuf; + + rsbuf = RUNSEP; + RUNSEP = "x"; + termPrint (t); + RUNSEP = rsbuf; + } +} + +//! Value for hlsrgb conversion +static double +hlsValue (double n1, double n2, double hue) +{ + if (hue > 360.0) + hue -= 360.0; + else if (hue < 0.0) + hue += 360.0; + if (hue < 60.0) + return n1 + (n2 - n1) * hue / 60.0; + else if (hue < 180.0) + return n2; + else if (hue < 240.0) + return n1 + (n2 - n1) * (240.0 - hue) / 60.0; + else + return n1; +} + +//! hls to rgb conversion +void +hlsrgbreal (int *r, int *g, int *b, double h, double l, double s) +{ + double m1, m2; + + int bytedouble (double d) + { + double x; + + x = 255.0 * d; + if (x <= 0) + return 0; + else if (x >= 255.0) + return 255; + else + return (int) x; + } + + while (h >= 360.0) + h -= 360.0; + while (h < 0) + h += 360.0; + m2 = (l <= 0.5) ? (l * (l + s)) : (l + s - l * s); + m1 = 2.0 * l - m2; + if (s == 0.0) + { + *r = *g = *b = bytedouble (l); + } + else + { + *r = bytedouble (hlsValue (m1, m2, h + 120.0)); + *g = bytedouble (hlsValue (m1, m2, h)); + *b = bytedouble (hlsValue (m1, m2, h - 120.0)); + } +} + +//! hls to rgb conversion +/** + * Secretly takes the monochrome switch into account + */ +void +hlsrgb (int *r, int *g, int *b, double h, double l, double s) +{ + double closer (double l, double factor) + { + return l + ((1.0 - l) * factor); + } + + if (switches.monochrome) + { + // No colors + s = 0; + h = 0; + } + + if (switches.lightness > 0) + { + // correction switch for lightness + if (switches.lightness == 100) + { + l = 1.0; + } + else + { + l = closer (l, ((double) switches.lightness / 100.0)); + } + } + +// convert + hlsrgbreal (r, g, b, h, l, s); +} + + +//! print color from h,l,s triplet +void +printColor (double h, double l, double s) +{ + int r, g, b; + + hlsrgb (&r, &g, &b, h, l, s); + eprintf ("#%02x%02x%02x", r, g, b); +} + + +//! Set local buffer with the correct color for this run. +/** + * Determines number of protocols, shifts to the right color pair, and colors + * the run within the current protocol in the fade between the color pair. + * + * This can be done much more efficiently by computing these colors once, + * instead of each time again for each run. However, this is not a + * speed-critical section so this will do just nicely. + */ +void +setRunColorBuf (const System sys, int run, char *colorbuf) +{ + int range; + int index; + double protoffset, protrange; + double roleoffset, roledelta; + double color; + double h, l, s; + int r, g, b; + + // help function: contract roleoffset, roledelta with a factor (<= 1.0) + void contract (double factor) + { + roledelta = roledelta * factor; + roleoffset = (roleoffset * factor) + ((1.0 - factor) / 2.0); + } + + // determine #protocol, resulting in two colors + { + Termlist protocols; + Term refprot; + int r; + int firstfound; + + protocols = NULL; + refprot = sys->runs[run].protocol->nameterm; + index = 0; + range = 1; + firstfound = false; + for (r = 0; r < sys->maxruns; r++) + { + if (sys->runs[r].protocol != INTRUDER) + { + Term prot; + + prot = sys->runs[r].protocol->nameterm; + if (!isTermEqual (prot, refprot)) + { + // Some 'other' protocol + if (!inTermlist (protocols, prot)) + { + // New other protocol + protocols = termlistAdd (protocols, prot); + range++; + if (!firstfound) + { + index++; + } + } + } + else + { + // Our protocol + firstfound = true; + } + } + } + termlistDelete (protocols); + } + + // Compute protocol offset [0.0 ... 1.0> + protrange = 1.0 / range; + protoffset = index * protrange; + + // We now now our range, and we can determine which role this one is. + { + Role rr; + int done; + + range = 0; + index = 0; + done = false; + + for (rr = sys->runs[run].protocol->roles; rr != NULL; rr = rr->next) + { + if (sys->runs[run].role == rr) + { + done = true; + } + else + { + if (!done) + { + index++; + } + } + range++; + } + } + + // Compute role offset [0.0 ... 1.0] + if (range <= 1) + { + roledelta = 0.0; + roleoffset = 0.5; + } + else + { + // range over 0..1 + roledelta = 1.0 / (range - 1); + roleoffset = index * roledelta; + // Now this can result in a delta that is too high (depending on protocolrange) + if (protrange * roledelta > RUNCOLORDELTA) + { + contract (RUNCOLORDELTA / (protrange * roledelta)); + } + } + + // We slightly contract the colors (taking them away from protocol edges) + contract (RUNCOLORCONTRACT); + + // Now we can convert this to a color + color = protoffset + (protrange * roleoffset); + h = RUNCOLORH1 + color * (RUNCOLORH2 - RUNCOLORH1); + l = RUNCOLORL1 + color * (RUNCOLORL2 - RUNCOLORL1); + s = RUNCOLORS1 + color * (RUNCOLORS2 - RUNCOLORS1); + + // If the run is not trusted, we lower the saturation significantly + if (!isRunTrusted (sys, run)) + { + s = UNTRUSTEDCOLORS; + } + + // set to buffer + hlsrgb (&r, &g, &b, h, l, s); + sprintf (colorbuf, "#%02x%02x%02x", r, g, b); + + // compute second color (light version) + /* + l += 0.07; + if (l > 1.0) + l = 1.0; + */ + hlsrgb (&r, &g, &b, h, l, s); + sprintf (colorbuf + 8, "#%02x%02x%02x", r, g, b); +} + +//! Communication status +int +isCommunicationExact (const System sys, Binding b) +{ + Roledef rd1, rd2; + + rd1 = eventRoledef (sys, b->run_from, b->ev_from); + rd2 = eventRoledef (sys, b->run_to, b->ev_to); + + if (!isTermEqual (rd1->message, rd2->message)) + { + return false; + } + if (!isTermEqual (rd1->from, rd2->from)) + { + return false; + } + if (!isTermEqual (rd1->to, rd2->to)) + { + return false; + } + if (!isTermEqual (rd1->label, rd2->label)) + { + return false; + } + return true; +} + +//! Ignore some events +int +isEventIgnored (const System sys, int run, int ev) +{ + Roledef rd; + + rd = eventRoledef (sys, run, ev); + if (rd->type == CLAIM) + { + if (run != 0) + { + return true; + } + else + { + if (ev != sys->current_claim->ev) + { + return true; + } + } + } + return false; +} + +//! Check whether an event is a function application +int +isApplication (const System sys, const int run) +{ + if (sys->runs[run].protocol == INTRUDER) + { + if (sys->runs[run].role == I_RRS) + { + Roledef rd; + + rd = sys->runs[run].start->next; + if (rd != NULL) + { + if (isTermFunctionName (rd->message)) + { + return true; + } + } + } + } + return false; +} + +//! Is an event enabled by M0 only? +int +isEnabledM0 (const System sys, const int run, const int ev) +{ + List bl; + + for (bl = sys->bindings; bl != NULL; bl = bl->next) + { + Binding b; + + b = (Binding) bl->data; + if (!b->blocked) + { + // if the binding is not done (class choice) we might + // still show it somewhere. + if (b->done) + { + if (b->run_to == run && b->ev_to == ev) + { + if (sys->runs[b->run_from].role != I_M) + { + return false; + } + } + } + } + } + return true; +} + +//! Check whether the event is an M_0 function application (special case of the previous) +int +isApplicationM0 (const System sys, const int run) +{ + if (sys->runs[run].length > 1) + { + if (isApplication (sys, run)) + { + if (isEnabledM0 (sys, run, 1)) + { + return true; + } + } + } + return false; +} + +//! Determine ranks for all nodes +/** + * Some crude algorithm I sketched on the blackboard. + */ +int +graph_ranks (int *ranks, int nodes) +{ + int done; + int rank; + int changes; + + int getrank (int run, int ev) + { + return ranks[eventNode (run, ev)]; + } + + void setrank (int run, int ev, int rank) + { + ranks[eventNode (run, ev)] = rank; + } + +#ifdef DEBUG + if (hasCycle ()) + { + error ("Graph ranks tried, but a cycle exists!"); + } +#endif + + { + int i; + + for (i = 0; i < nodes; i++) + { + ranks[i] = INT_MAX; + } + } + + rank = 0; + done = false; + changes = true; + while (!done) + { + int checkCanEventHappenNow (int run, Roledef rd, int ev) + { + //if (sys->runs[run].protocol != INTRUDER) + { + if (getrank (run, ev) == INT_MAX) + { + // Allright, this regular event is not assigned yet + int precevent (int run2, int ev2) + { + //if (sys->runs[run2].protocol != INTRUDER) + { + // regular preceding event + int rank2; + + rank2 = getrank (run2, ev2); + if (rank2 > rank) + { + // higher rank, this cannot be done + return false; + } + if (rank2 == rank) + { + // equal rank: only if different run + if ((sys->runs[run].protocol != INTRUDER) + && (run2 == run)) + { + return false; + } + } + } + return true; + } + + if (iteratePrecedingEvents (sys, precevent, run, ev)) + { + // we can do it! + changes = true; + setrank (run, ev, rank); + } + else + { + done = false; + } + } + } + return true; + } + + + if (!changes) + { + rank++; + if (rank >= nodes) + { + warning ("Rank %i increased to the number of nodes %i.", rank, + nodes); + return rank; + } + } + done = true; + changes = false; + iterateAllEvents (sys, checkCanEventHappenNow); + } + return rank; +} + +//! Display the ranks +/** + * Reinstated after it had been gone for a while + */ +void +showRanks (const System sys, const int maxrank, const int *ranks, + const int nodes) +{ + int rank; + + //return; + + for (rank = 0; rank <= maxrank; rank++) + { + int found; + int run; + + found = 0; + for (run = 0; run < sys->maxruns; run++) + { + if (sys->runs[run].protocol != INTRUDER) + { + int ev; + + for (ev = 0; ev < sys->runs[run].step; ev++) + { + if (!isEventIgnored (sys, run, ev)) + { + + int n; + + n = eventNode (run, ev); + if (ranks[n] == rank) + { + if (found == 0) + { + eprintf ("\t{ rank = same; "); + } + node (sys, run, ev); + eprintf ("; "); + found++; + } + } + } + } + } + if (found > 0) + { + eprintf ("}\n"); + } + } +} + +//! Does a term occur in a run? +int +termOccursInRun (Term t, int run) +{ + Roledef rd; + int e; + + rd = sys->runs[run].start; + e = 0; + while (e < sys->runs[run].step) + { + if (roledefSubTerm (rd, t)) + { + return true; + } + e++; + rd = rd->next; + } + return false; +} + +//! Draw a class choice +/** + * \rho classes are already dealt with in the headers, so we should ignore them. + */ +void +drawClass (const System sys, Binding b) +{ + Term varterm; + + // now check in previous things whether we saw that term already + int notSameTerm (Binding b2) + { + return (!isTermEqual (varterm, b2->term)); + } + + varterm = deVar (b->term); + + // Variable? + if (!isTermVariable (varterm)) + { + return; + } + + // Agent variable? + { + int run; + + run = TermRunid (varterm); + if ((run >= 0) && (run < sys->maxruns)) + { + if (inTermlist (sys->runs[run].rho, varterm)) + { + return; + } + } + } + + // Seen before? + if (!iterate_preceding_bindings (b->run_to, b->ev_to, notSameTerm)) + { + // We saw the same term before. Exit. + return; + } + + + + + // not seen before: choose class + eprintf ("\t"); + chooseTermNode (varterm); + eprintf (" [label=\""); + explainVariable (varterm); + eprintf ("\"];\n"); + eprintf ("\t"); + chooseTermNode (varterm); + eprintf (" -> "); + node (sys, b->run_to, b->ev_to); + eprintf (" [weight=\"%s\",arrowhead=\"none\",style=\"dotted\"];\n", + CHOOSEWEIGHT); +} + +//! Print label of a regular->regular transition node (when comm. is not exact) +/** + * Note that we ignore any label differences, these are left implicit + */ +void +regularModifiedLabel (Binding b) +{ + Roledef rdfrom; + Roledef rdto; + int unknown; + + rdfrom = eventRoledef (sys, b->run_from, b->ev_from); + rdto = eventRoledef (sys, b->run_to, b->ev_to); + unknown = true; + + // First up: compare messages contents': what was sent, what is needed + if (!isTermEqual (rdfrom->message, b->term)) + { + // What is sent is not equal to what is bound + if (termInTerm (rdfrom->message, b->term)) + { + // Interm: simple select + unknown = false; + eprintf ("select "); + termPrintRemap (b->term); + eprintf ("\\n"); + } + } + + // Second: agent things + if (!isTermEqual (rdfrom->from, rdto->from)) + { + unknown = false; + eprintf ("fake sender "); + termPrintRemap (rdto->from); + eprintf ("\\n"); + } + if (!isTermEqual (rdfrom->to, rdto->to)) + { + unknown = false; + eprintf ("redirect to "); + termPrintRemap (rdto->to); + eprintf ("\\n"); + } + + // Any leftovers for which I don't have a good name yet. + if (unknown) + { + // I'm not quite sure, we call it 'combine' for now. TODO + eprintf ("combine\\n"); + } +} + +//! + +//! Draw a single binding +void +drawBinding (const System sys, Binding b) +{ + int intr_to, intr_from, m0_from; + + void myarrow (const Binding b) + { + if (m0_from) + { + eprintf ("\t"); + intruderNodeM0 (); + eprintf (" -> "); + node (sys, b->run_to, b->ev_to); + } + else + { + arrow (sys, b); + } + + } + + intr_from = (sys->runs[b->run_from].protocol == INTRUDER); + intr_to = (sys->runs[b->run_to].protocol == INTRUDER); + m0_from = false; + + // Pruning: things going to M0 applications are pruned; + if (isApplicationM0 (sys, b->run_to)) + { + return; + } + if (isApplicationM0 (sys, b->run_from) || + sys->runs[b->run_from].role == I_M) + { + m0_from = true; + } + + // Normal drawing cases; + if (intr_from) + { + // from intruder + /* + * Because this can be generated many times, it seems + * reasonable to not duplicate such arrows, especially when + * they're from M_0. Maybe the others are still relevant. + */ + if (1 == 1 || sys->runs[b->run_from].role == I_M) + { + // now check in previous things whether we saw that term already + int notSameTerm (Binding b2) + { + return (!isTermEqual (b->term, b2->term)); + } + + if (!iterate_preceding_bindings (b->run_to, b->ev_to, notSameTerm)) + { + // We saw the same term before. Exit. + return; + } + } + + // normal from intruder, not seen before (might be M_0) + if (intr_to) + { + // intr->intr + eprintf ("\t"); + myarrow (b); + eprintf (" [label=\""); + termPrintRemap (b->term); + eprintf ("\""); + if (m0_from) + { + eprintf (",weight=\"10.0\""); + } + eprintf ("]"); + eprintf (";\n"); + } + else + { + // intr->regular + eprintf ("\t"); + myarrow (b); + if (m0_from) + { + eprintf ("[weight=\"0.5\"]"); + } + eprintf (";\n"); + } + } + else + { + // not from intruder + if (intr_to) + { + // regular->intr + eprintf ("\t"); + myarrow (b); + eprintf (";\n"); + } + else + { + // regular->regular + /* + * Has this been done *exactly* as we hoped? + */ + if (isCommunicationExact (sys, b)) + { + eprintf ("\t"); + myarrow (b); + eprintf (" [style=bold,color=\"%s\"]", GOODCOMMCOLOR); + eprintf (";\n"); + } + else + { + // Something was changed, so we call this a redirect + eprintf ("\t"); + node (sys, b->run_from, b->ev_from); + eprintf (" -> "); + redirNode (sys, b); + eprintf (" -> "); + node (sys, b->run_to, b->ev_to); + eprintf (";\n"); + + eprintf ("\t"); + redirNode (sys, b); + eprintf (" [style=filled,fillcolor=\""); + printColor (INTRUDERCOLORH, INTRUDERCOLORL, INTRUDERCOLORS); + eprintf ("\",label=\""); + regularModifiedLabel (b); + eprintf ("\"]"); + eprintf (";\n"); + + } + } + } +} + +//! Draw dependecies (including intruder!) +/** + * Returns from_intruder_count (from M_0) + */ +int +drawAllBindings (const System sys) +{ + List bl; + int fromintr; + + fromintr = 0; + for (bl = sys->bindings; bl != NULL; bl = bl->next) + { + Binding b; + + b = (Binding) bl->data; + if (!b->blocked) + { + // if the binding is not done (class choice) we might + // still show it somewhere. + if (b->done) + { + // done, draw + drawBinding (sys, b); + // from intruder? + if (sys->runs[b->run_from].protocol == INTRUDER) + { + if (sys->runs[b->run_from].role == I_M) + { + fromintr++; + } + } + } + else + { + drawClass (sys, b); + } + } + } + return fromintr; +} + +//! Print "Alice in role R" of a run +void +printAgentInRole (const System sys, const int run) +{ + Term rolename; + Term agentname; + + rolename = sys->runs[run].role->nameterm; + agentname = agentOfRunRole (sys, run, rolename); + explainVariable (agentname); + eprintf (" in role "); + termPrintRemap (rolename); +} + +//! rho, sigma, const +/* + * true if it has printed + */ +int +showLocal (const int run, Term told, Term tnew, char *prefix, char *cursep) +{ + if (realTermVariable (tnew)) + { + if (termOccursInRun (tnew, run)) + { + // Variables are mapped, maybe. But then we wonder whether they occur in reads. + eprintf (cursep); + eprintf (prefix); + termPrintRemap (told); + eprintf (" -\\> "); + explainVariable (tnew); + } + else + { + return false; + } + } + else + { + eprintf (cursep); + eprintf (prefix); + termPrintRemap (tnew); + } + return true; +} + + +//! show a list of locals +/** + * never ends with the seperator + */ +int +showLocals (const int run, Termlist tlold, Termlist tlnew, + Term tavoid, char *prefix, char *sep) +{ + int anything; + char *cursep; + + cursep = ""; + anything = false; + while (tlold != NULL && tlnew != NULL) + { + if (!isTermEqual (tlold->term, tavoid)) + { + if (showLocal (run, tlold->term, tlnew->term, prefix, cursep)) + { + cursep = sep; + anything = true; + } + } + tlold = tlold->next; + tlnew = tlnew->next; + } + return anything; +} + +//! Explain the local constants +/** + * Return true iff something was printed + */ +int +printRunConstants (const System sys, const int run) +{ + if (sys->runs[run].constants != NULL) + { + eprintf ("Const "); + showLocals (run, sys->runs[run].role-> + declaredconsts, sys->runs[run].constants, NULL, "", ", "); + eprintf ("\\l"); + return true; + } + else + { + return false; + } +} + + +//! Explain a run in two lines +void +printRunExplanation (const System sys, const int run, + char *runrolesep, char *newline) +{ + int hadcontent; + + eprintf ("Run "); + printVisualRunID (run); + + eprintf (runrolesep); + // Print first line + printAgentInRole (sys, run); + eprintf ("\\l"); + + // Second line + // Possible protocol (if more than one) + { + int showprotocol; + Protocol p; + int morethanone; + + // Simple case: don't show + showprotocol = false; + + // Check whether the protocol spec has more than one + morethanone = false; + for (p = sys->protocols; p != NULL; p = p->next) + { + if (p != INTRUDER) + { + if (p != sys->runs[run].protocol) + { + morethanone = true; + break; + } + } + } + + // More than one? + if (morethanone) + { + // This used to work for run 0 always... + //if (run == 0) + if (false) + { + // If this is run 0 we report the protocol anyway, even is there is only a single one in the attack + showprotocol = true; + } + else + { + int r; + // For other runs we only report when there are multiple protocols + showprotocol = false; + for (r = 0; r < sys->maxruns; r++) + { + if (sys->runs[r].protocol != INTRUDER) + { + if (sys->runs[r].protocol != sys->runs[run].protocol) + { + showprotocol = true; + break; + } + } + } + } + } + + // Use the result + if (showprotocol) + { + eprintf ("Protocol "); + termPrintRemap (sys->runs[run].protocol->nameterm); + eprintf ("\\l"); + } + } + + eprintf (newline); + hadcontent = false; + + { + /* + * Originally, we ignored the actor in the rho list, but for more than two-party protocols, this was unclear. + */ + int numroles; + int ignoreactor; + + ignoreactor = false; // set to true to ignore the actor + numroles = termlistLength (sys->runs[run].rho); + + if (numroles > 1) + { + { + Term ignoreterm; + + if (ignoreactor) + { + ignoreterm = sys->runs[run].role->nameterm; + } + else + { + ignoreterm = NULL; + } + hadcontent = showLocals (run, sys->runs[run].protocol-> + rolenames, sys->runs[run].rho, + ignoreterm, "", "\\l"); + } + } + } + + if (hadcontent) + { + eprintf ("\\l"); + eprintf (newline); + hadcontent = false; + } + hadcontent = printRunConstants (sys, run); + + if (sys->runs[run].sigma != NULL) + { + if (hadcontent) + { + eprintf (newline); + hadcontent = false; + } + if (showLocals (run, sys->runs[run].role-> + declaredvars, sys->runs[run].sigma, NULL, "Var ", + "\\l")) + { + eprintf ("\\l"); + } + } +} + +//! Draw regular runs +void +drawRegularRuns (const System sys) +{ + int run; + int rcnum; + char *colorbuf; + + // two buffers, eight chars each + colorbuf = malloc (16 * sizeof (char)); + + rcnum = 0; + for (run = 0; run < sys->maxruns; run++) + { + if (sys->runs[run].length > 0) + { + if (sys->runs[run].protocol != INTRUDER) + { + Roledef rd; + int index; + int prevnode; + + prevnode = 0; + index = 0; + rd = sys->runs[run].start; + // Regular run + + if (switches.clusters) + { + eprintf ("\tsubgraph cluster_run%i {\n", run); + + eprintf ("\t\tstyle=filled;\n"); + eprintf ("\t\tcolor=lightgrey;\n"); + + eprintf ("\t\tlabel=\""); + printRunExplanation (sys, run, " : ", ""); + eprintf ("\";\n\n"); + } + + // set color + setRunColorBuf (sys, run, colorbuf); + + // Display the respective events + while (index < sys->runs[run].length) + { + if (!isEventIgnored (sys, run, index)) + { + // Print node itself + eprintf ("\t\t"); + node (sys, run, index); + eprintf (" ["); + if (run == 0 && index == sys->current_claim->ev) + { + // The claim under scrutiny + eprintf + ("style=filled,fontcolor=\"%s\",fillcolor=\"%s\",shape=box,", + CLAIMTEXTCOLOR, CLAIMCOLOR); + } + else + { + eprintf ("shape=box,style=filled,"); + // print color of this run + eprintf ("fillcolor=\"%s\",", colorbuf); + } + eprintf ("label=\""); + //roledefPrintShort (rd); + roledefDraw (rd); + eprintf ("\"]"); + eprintf (";\n"); + + // Print binding to previous node + if (index > sys->runs[run].firstReal) + { + // index > 0 + eprintf ("\t\t"); + node (sys, run, prevnode); + eprintf (" -> "); + node (sys, run, index); + eprintf (" [style=\"bold\", weight=\"%s\"]", + RUNWEIGHT); + eprintf (";\n"); + prevnode = index; + } + else + { + // index <= firstReal + if (index == sys->runs[run].firstReal) + { + // index == firstReal + Roledef rd; + int send_before_read; + int done; + + // Determine if it is an active role or note + /** + *@todo note that this will probably become a standard function call for role.h + */ + rd = + roledef_shift (sys->runs[run].start, + sys->runs[run].firstReal); + done = 0; + send_before_read = 0; + while (!done && rd != NULL) + { + if (rd->type == READ) + { + done = 1; + } + if (rd->type == SEND) + { + done = 1; + send_before_read = 1; + } + rd = rd->next; + } + + if (!switches.clusters) + { + // Draw the first box (HEADER) + // This used to be drawn only if done && send_before_read, now we always draw it. + eprintf ("\t\ts%i [label=\"{ ", run); + + printRunExplanation (sys, run, "\\l", "|"); + // close up + eprintf ("}\", shape=record"); + eprintf + (",style=filled,fillcolor=\"%s\"", + colorbuf + 8); + eprintf ("];\n"); + eprintf ("\t\ts%i -> ", run); + node (sys, run, index); + eprintf + (" [style=bold, weight=\"%s\"];\n", + RUNWEIGHT); + prevnode = index; + } + + + } + } + } + index++; + rd = rd->next; + } + + if (switches.clusters) + { + eprintf ("\t}\n"); + } + + } + } + } + free (colorbuf); +} + +//! Draw intruder runs +void +drawIntruderRuns (const System sys) +{ + int run; + + if (switches.clusters) + { + //eprintf ("\tsubgraph cluster_intruder {\n"); + eprintf ("\tsubgraph intr {\n"); + eprintf ("\t\tlabel = \"Intruder\";\n"); + eprintf ("\t\tcolor = red;\n"); + } + + for (run = 0; run < sys->maxruns; run++) + { + if (sys->runs[run].length > 0) + { + if (sys->runs[run].protocol == INTRUDER) + { + // Intruder run + if (sys->runs[run].role != I_M && !isApplicationM0 (sys, run)) + { + // Not an M_0 run, and not an M0 function application, so we can draw it. + eprintf ("\t\t"); + node (sys, run, 0); + eprintf (" [style=filled,fillcolor=\""); + printColor (INTRUDERCOLORH, INTRUDERCOLORL, INTRUDERCOLORS); + eprintf ("\","); + if (sys->runs[run].role == I_RRSD) + { + eprintf ("label=\"decrypt\""); + } + if (sys->runs[run].role == I_RRS) + { + // Distinguish function application + if (isTermFunctionName + (sys->runs[run].start->next->message)) + { + eprintf ("label=\"apply\""); + } + else + { + eprintf ("label=\"encrypt\""); + } + } + eprintf ("];\n"); + } + } + } + } + if (switches.clusters) + { + eprintf ("\t}\n\n"); + } +} + +//! Display the current semistate using dot output format. +/** + * This is not as nice as we would like it. Furthermore, the function is too big. + */ +void +dotSemiState (const System mysys) +{ + static int attack_number = 0; + Protocol p; + int *ranks; + int maxrank; + int from_intruder_count; + int nodes; + + sys = mysys; + + // Open graph + attack_number++; + eprintf ("digraph semiState%i {\n", attack_number); + eprintf ("\tlabel = \"[Id %i] Protocol ", sys->attackid); + p = (Protocol) sys->current_claim->protocol; + termPrintRemap (p->nameterm); + eprintf (", role "); + termPrintRemap (sys->current_claim->rolename); + eprintf (", claim type "); + termPrintRemap (sys->current_claim->type); + eprintf ("\";\n"); + + // Needed for the bindings later on: create graph + + nodes = nodeCount (); + ranks = malloc (nodes * sizeof (int)); + maxrank = graph_ranks (ranks, nodes); // determine ranks + +#ifdef DEBUG + if (DEBUGL (1)) + { + // For debugging purposes, we also display an ASCII version of some stuff in the comments + printSemiState (); + // Even draw all dependencies for non-intruder runs + // Real nice debugging :( + int run; + + run = 0; + while (run < sys->maxruns) + { + int ev; + + ev = 0; + while (ev < sys->runs[run].length) + { + int run2; + int notfirstrun; + + eprintf ("// precedence: r%ii%i <- ", run, ev); + run2 = 0; + notfirstrun = 0; + while (run2 < sys->maxruns) + { + int notfirstev; + int ev2; + + notfirstev = 0; + ev2 = 0; + while (ev2 < sys->runs[run2].length) + { + if (isDependEvent (run2, ev2, run, ev)) + { + if (notfirstev) + eprintf (","); + else + { + if (notfirstrun) + eprintf (" "); + eprintf ("r%i:", run2); + } + eprintf ("%i", ev2); + notfirstrun = 1; + notfirstev = 1; + } + ev2++; + } + run2++; + } + eprintf ("\n"); + ev++; + } + run++; + } + } +#endif + + // First, runs + drawRegularRuns (sys); + drawIntruderRuns (sys); + from_intruder_count = drawAllBindings (sys); + + // Third, the intruder node (if needed) + { + /* + * Stupid brute analysis, can probably be done much more efficient, but + * this is not a timing critical bit, so we just do it like this. + */ + Termlist found; + List bl; + + // collect the intruder-generated constants + found = NULL; + for (bl = sys->bindings; bl != NULL; bl = bl->next) + { + Binding b; + + b = (Binding) bl->data; + if (!b->blocked) + { + int addsubterms (Term t) + { + if (isIntruderChoice (t)) + { + found = termlistAddNew (found, t); + } + return true; + } + + term_iterate_open_leaves (b->term, addsubterms); + } + } + + // now maybe we draw the node + if ((from_intruder_count > 0) || (found != NULL)) + { + eprintf ("\tintruder [\n"); + eprintf ("\t\tlabel=\""); + eprintf ("Initial intruder knowledge"); + if (found != NULL) + { + eprintf ("\\n"); + eprintf ("The intruder generates: "); + termlistPrintRemap (found, ", "); + } + eprintf ("\",\n"); + eprintf ("\t\tstyle=filled,fillcolor=\""); + printColor (INTRUDERCOLORH, INTRUDERCOLORL, INTRUDERCOLORS); + eprintf ("\"\n\t];\n"); + } + termlistDelete (found); + } + + // eprintf ("\t};\n"); + + // For debugging we might add more stuff: full dependencies +#ifdef DEBUG + if (DEBUGL (3)) + { + int r1; + + for (r1 = 0; r1 < sys->maxruns; r1++) + { + if (sys->runs[r1].protocol != INTRUDER) + { + int e1; + + for (e1 = 0; e1 < sys->runs[r1].step; e1++) + { + int r2; + + for (r2 = 0; r2 < sys->maxruns; r2++) + { + if (sys->runs[r2].protocol != INTRUDER) + { + int e2; + + for (e2 = 0; e2 < sys->runs[r2].step; e2++) + { + if (isDependEvent (r1, e1, r2, e2)) + { + eprintf + ("\tr%ii%i -> r%ii%i [color=grey];\n", + r1, e1, r2, e2); + } + } + } + } + } + } + } + } +#endif + + // Ranks + if (switches.clusters) + { + showRanks (sys, maxrank, ranks, nodes); + } + +#ifdef DEBUG + // Debug: print dependencies + if (DEBUGL (3)) + { + dependPrint (); + } +#endif + + // clean memory + free (ranks); // ranks + + // close graph + eprintf ("};\n\n"); +} diff --git a/gui/src/dotout.h b/gui/src/dotout.h new file mode 100644 index 0000000..63cad32 --- /dev/null +++ b/gui/src/dotout.h @@ -0,0 +1,6 @@ +#ifndef DOTOUTPUT +#define DOTOUTPUT + +void dotSemiState (const System sys); + +#endif diff --git a/gui/src/error.c b/gui/src/error.c new file mode 100644 index 0000000..d192b17 --- /dev/null +++ b/gui/src/error.c @@ -0,0 +1,94 @@ +#include +#include +#include +#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); +} diff --git a/gui/src/error.h b/gui/src/error.h new file mode 100644 index 0000000..869642b --- /dev/null +++ b/gui/src/error.h @@ -0,0 +1,19 @@ +#ifndef ERROR +#define ERROR + +//! usestderr is defined iff we use it +#define USESTDERR + +//! Types of exit codes +enum exittypes +{ EXIT_NOATTACK = 0, EXIT_ERROR = 1, EXIT_ATTACK = 3 }; + +void vprintfstderr (char *fmt, va_list args); +void printfstderr (char *fmt, ...); +void error_die (void); +void error_pre (void); +void error_post (char *fmt, ...); +void error (char *fmt, ...); +void warning (char *fmt, ...); + +#endif diff --git a/gui/src/git-test.txt b/gui/src/git-test.txt new file mode 100644 index 0000000..d35b7c9 --- /dev/null +++ b/gui/src/git-test.txt @@ -0,0 +1,4 @@ +Test file to see whether it works. +Wow. +New line. +And a better conflict should start here. diff --git a/gui/src/heuristic.c b/gui/src/heuristic.c new file mode 100644 index 0000000..fb63a7d --- /dev/null +++ b/gui/src/heuristic.c @@ -0,0 +1,399 @@ +/** + * + *@file heuristic.c + * + * Heuristics code for Arachne method + * + */ + +#include +#include + +#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; +} diff --git a/gui/src/heuristic.h b/gui/src/heuristic.h new file mode 100644 index 0000000..89108c6 --- /dev/null +++ b/gui/src/heuristic.h @@ -0,0 +1,9 @@ +#ifndef HEURISTIC +#define HEURISTIC + +#include "system.h" +#include "binding.h" + +Binding select_goal (const System sys); + +#endif diff --git a/gui/src/hidelevel.c b/gui/src/hidelevel.c new file mode 100644 index 0000000..640e3b3 --- /dev/null +++ b/gui/src/hidelevel.c @@ -0,0 +1,261 @@ +/** @file hidelevel.c \brief Hidelevel lemma base functions. + * + * The Hidelevel lemma is fairly complex and so it requires some buffering, + * instead of fully recomputing the required data each time again. + */ + +#include +#include +#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; +} diff --git a/gui/src/hidelevel.h b/gui/src/hidelevel.h new file mode 100644 index 0000000..a16472c --- /dev/null +++ b/gui/src/hidelevel.h @@ -0,0 +1,27 @@ +#ifndef HIDELEVELS +#define HIDELEVELS + +#include "term.h" +#include "system.h" + +/* + * Flags for hidelevel lemma + * + * Use binary or (|) to compose results: by default, a term can be satisfied by + * both the protocol and the initial knowledge. + */ +#define HLFLAG_BOTH 0 +#define HLFLAG_KNOW 1 +#define HLFLAG_PROT 2 +#define HLFLAG_NONE 3 + +/* + * The structure hiddenterm/Hiddenterm is defined in system.h + */ + +void hidelevelCompute (const System sys); +int hidelevelInteresting (const System sys, const Term goalterm); +int hidelevelImpossible (const System sys, const Term goalterm); +unsigned int hidelevelFlag (const System sys, const Term goalterm); + +#endif diff --git a/gui/src/hidelevel.txt b/gui/src/hidelevel.txt new file mode 100644 index 0000000..e547450 --- /dev/null +++ b/gui/src/hidelevel.txt @@ -0,0 +1,31 @@ +Implemented: + +- scans +- test functions (in hidelevel.c) + +TODO: + +- use test functions (impossible for pruning, interesting for goal selection heuristic) +- state count display switch for comparisons +- consider adding info for goal stuff (only from M_0, not by create) + +******************************************************************* + +roivas:~scyther% ./scyther ccitt509-1c.spdl +Global constants: [te, ne, Eve, Bob, Alice, unhash, sk, hash, pk] + +Possibly interesting term: unhash; know 2147483647, prot 2147483647 +Possibly interesting term: sk; know 1, prot 2 + + +roivas:~scyther% ./scyther yahalom.spdl +warning: variable T was declared in role yahalom,R but never used in a read event. +Global constants: [Simon, Bob, Alice, Compromised, Fresh, k] + +Possibly interesting term: k; know 2147483647, prot 2 + + +roivas:~scyther% ./scyther ns3.spdl +Global constants: [Eve, sk, pk] + +Possibly interesting term: sk; know 1, prot 2147483647 diff --git a/gui/src/intruderknowledge.c b/gui/src/intruderknowledge.c new file mode 100644 index 0000000..b429649 --- /dev/null +++ b/gui/src/intruderknowledge.c @@ -0,0 +1,197 @@ +/** + * Initial intruder knowledge computation. + */ + +#include "intruderknowledge.h" + +//! Add a (copy of) a term to the intruder knowledge +void +addSTerm (const System sys, Term t, Termlist fromlist, Termlist tolist) +{ + Term t2; + + t2 = termLocal (t, fromlist, tolist); + + if (switches.check) + { + globalError++; + eprintf ("[ Adding "); + termPrint (t2); + eprintf (" to the initial intruder knowledge]\n"); + globalError--; + } +} + +//! Unfold the term for all possible options +void +addEnumTerm (const System sys, Term t, Term actor, Termlist todo, + Termlist fromlist, Termlist tolist) +{ + if (todo == NULL) + { + addSTerm (sys, t, fromlist, tolist); + } + else + { + if (termSubTerm (t, todo->term)) + { + // Occurs, we have to iterate + void iterateThis (Term to) + { + tolist = termlistPrepend (tolist, to); + + addEnumTerm (sys, t, actor, todo->next, fromlist, tolist); + + tolist = termlistDelTerm (tolist); + } + + fromlist = termlistPrepend (fromlist, todo->term); + if (isTermEqual (todo->term, actor)) + { + // Untrusted agents only + Termlist tl; + + for (tl = sys->untrusted; tl != NULL; tl = tl->next) + { + iterateThis (tl->term); + } + } + else + { + // any agents + Termlist tl; + + for (tl = sys->agentnames; tl != NULL; tl = tl->next) + { + iterateThis (tl->term); + } + } + fromlist = termlistDelTerm (fromlist); + } + else + { + // Simply proceed to next + addEnumTerm (sys, t, actor, todo->next, fromlist, tolist); + } + } +} + +//! Does t contain any of sublist? +int +anySubTerm (Term t, Termlist sublist) +{ + while (sublist != NULL) + { + if (termSubTerm (t, sublist->term)) + { + return true; + } + sublist = sublist->next; + } + return false; +} + +void +initialIntruderKnowledge (const System sys) +{ + /* + * display initial role knowledge + */ + int deriveFromRole (Protocol p, Role r) + { + void addListKnowledge (Termlist tl, Term actor) + { + void addTermKnowledge (Term t) + { + if (anySubTerm (t, p->rolenames)) + { + Term f; + // Has rolename subterms. We have to enumerate those. + /** + * Hack. Enumerating is not always good (or even desirable). + * If some I knows sk(I), sk should not be in the intruder knowledge. + * But for hash(I), we typically would have h; but if it is never used differently, it would suffice. + * To summarize, the operational semantics definition is perfectly fine, but maybe a bit strict sometimes. + * + * The hack is that if function application: + */ + f = getTermFunction (t); + if (f != NULL) + { + // it's a function, right. So we see whether it is public. It is if it does not contain the actor... + if (!termSubTerm (t, actor)) + { + // no actor, then nothing secret I guess. + addSTerm (sys, f, NULL, NULL); + return; + } + else + { + // has actor. but does it contain even more? + + int allagents (Term t) + { + if (!inTermlist (sys->agentnames, t)) + { + if (!inTermlist (p->rolenames, t)) + { + return false; + } + } + return true; + } + + if (!term_iterate_leaves (TermOp (t), allagents)) + { + // something else as well, so that probably means a hash or something like that. + addSTerm (sys, f, NULL, NULL); + return; + } + } + } + // otherwise, we enumerate + addEnumTerm (sys, t, actor, p->rolenames, NULL, NULL); + } + else + { + // No actor subterm. Simply add. + addSTerm (sys, t, NULL, NULL); + } + } + + while (tl != NULL) + { + addTermKnowledge (tl->term); + tl = tl->next; + } + } + + if (switches.check) + { + globalError++; + eprintf ("Role "); + termPrint (r->nameterm); + eprintf (" knows "); + termlistPrint (r->knows); + eprintf ("\n"); + globalError--; + } + addListKnowledge (r->knows, r->nameterm); + return true; + } + + if (switches.check) + { + globalError++; + eprintf ("Computing initial intruder knowledge.\n\n"); + eprintf ("Agent names : "); + termlistPrint (sys->agentnames); + eprintf ("\n"); + eprintf ("Untrusted agents : "); + termlistPrint (sys->untrusted); + eprintf ("\n"); + globalError--; + } + + iterateRoles (sys, deriveFromRole); +} diff --git a/gui/src/intruderknowledge.h b/gui/src/intruderknowledge.h new file mode 100644 index 0000000..a871286 --- /dev/null +++ b/gui/src/intruderknowledge.h @@ -0,0 +1,9 @@ +#ifndef INTRUDERKNOWLEDGE +#define INTRUDERKNOWLEDGE + +#include "system.h" +#include "switches.h" + +void initialIntruderKnowledge (const System sys); + +#endif diff --git a/gui/src/knowledge.c b/gui/src/knowledge.c new file mode 100644 index 0000000..674f9d7 --- /dev/null +++ b/gui/src/knowledge.c @@ -0,0 +1,550 @@ +/** + *@file knowledge.c + *\brief Procedures concerning knowledge structures. + * + * The main issue of this code is to maintain the minimal property of the knowledge set. + */ +#include +#include +#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; +} diff --git a/gui/src/knowledge.h b/gui/src/knowledge.h new file mode 100644 index 0000000..c40c7cd --- /dev/null +++ b/gui/src/knowledge.h @@ -0,0 +1,75 @@ +#ifndef KNOWLEDGE +#define KNOWLEDGE + +#include "term.h" +#include "termlist.h" + +//! Knowledge structure. +/** + * Contains a miminal representation of a knowledge set. + */ +struct knowledge +{ + //! A list of non-encrypted terms. + Termlist basic; + //! A list of terms encrypted, such that the inverse is not in the knowledge set. + Termlist encrypt; + //! List of inverse pairs (thus length of list is even) + Termlist inverses; + //! List of open variables in the knowledge set. + /** + * This list is used to determine whether the knowledge needs to be rewritten. + * If a new substitution is done, one of the elements of this list will become closed, + * and we need to reconstruct the knowledge set. + */ + Termlist vars; // special: denotes unsubstituted variables +}; + +//! Shorthand for knowledge pointer. +typedef struct knowledge *Knowledge; + +void knowledgeInit (void); +void knowledgeDone (void); +Knowledge makeKnowledge (); +Knowledge emptyKnowledge (); +Knowledge knowledgeDuplicate (Knowledge know); +void knowledgeDelete (Knowledge know); +void knowledgeDestroy (Knowledge know); +int knowledgeAddTerm (Knowledge know, Term term); +int knowledgeAddTermlist (Knowledge know, Termlist tl); +void knowledgeAddInverse (Knowledge know, Term t1, Term t2); +void knowledgeSetInverses (Knowledge know, Termlist tl); +void knowledgeSimplify (Knowledge know, Term decryptkey); +int inKnowledge (const Knowledge know, Term term); +void knowledgePrint (Knowledge know); +void knowledgePrintShort (const Knowledge know); +void knowledgeInversesPrint (Knowledge know); +int isKnowledgeEqual (Knowledge know1, Knowledge know2); +Termlist knowledgeSet (const Knowledge know); +Termlist knowledgeGetInverses (const Knowledge know); +Termlist knowledgeGetBasics (const Knowledge know); +int knowledgeSubstNeeded (const Knowledge know); +Knowledge knowledgeSubstDo (const Knowledge know); +void knowledgeSubstUndo (const Knowledge know); +Termlist knowledgeNew (const Knowledge oldk, const Knowledge newk); + +//! Harnass macro for recursive procedures. +#define mindwipe(k,recurse) \ + Termlist tl; \ + int flag; \ + if (k != NULL && k->vars != NULL) { \ + tl = k->vars; \ + while (tl != NULL) { \ + if (tl->term->subst != NULL) { \ + Term oldsubst = tl->term->subst; \ + tl->term->subst = NULL; \ + flag = recurse; \ + tl->term->subst = oldsubst; \ + return flag; \ + } \ + tl = tl->next; \ + } \ + } \ + + +#endif diff --git a/gui/src/label.c b/gui/src/label.c new file mode 100644 index 0000000..20a2fad --- /dev/null +++ b/gui/src/label.c @@ -0,0 +1,86 @@ +/** + * Label info + */ + +#include +#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; +} diff --git a/gui/src/label.h b/gui/src/label.h new file mode 100644 index 0000000..ee80809 --- /dev/null +++ b/gui/src/label.h @@ -0,0 +1,26 @@ +#ifndef LABEL +#define LABEL + +#include "term.h" +#include "list.h" +#include "system.h" + +/* + * Structure to store label information + */ +struct labelinfo +{ + Term label; + int ignore; + Protocol protocol; + Term sendrole; + Term readrole; +}; + +typedef struct labelinfo *Labelinfo; + +Labelinfo label_create (const Term label, const Protocol protocol); +void label_destroy (Labelinfo linfo); +Labelinfo label_find (List labellist, const Term label); + +#endif diff --git a/gui/src/language.txt b/gui/src/language.txt new file mode 100644 index 0000000..a3e84ba --- /dev/null +++ b/gui/src/language.txt @@ -0,0 +1,46 @@ +Language +-------- + +language := ()* +def := ( | | | ) + +//directive := +//dir_require := require ; + +protocol := protocol ( ) { * } optsc +protocolname := + +intruderknow := public ; +roledef := role { } optsc +rolename := +actions := (;)+ +action := ( | | ) +decl := ( | )+ +const := const [ : ]; +var := var [ : ]; + +read := read [_