diff --git a/src/Makefile-fallback b/src/Makefile-fallback
deleted file mode 100644
index 22694f2..0000000
--- a/src/Makefile-fallback
+++ /dev/null
@@ -1,86 +0,0 @@
-#
-#	Scyther Makefile
-#
-
-#
-#	DEBUG or optimization settings: uncomment a single line:
-#
-CFLAGS = -g3 -D DEBUG		# default usage, for e.g. with valgrind
-#CFLAGS = -g3 -D DEBUG -pg	# for code profiling with gprof
-#CFLAGS = -O3 -static -finline-functions -fomit-frame-pointer
-
-#
-#	Compiler and linkage
-#
-CC = gcc
-# Note that these paths must include the path to the argtable library.
-CPPFLAGS = -I/scratch/ccremers/include -I/usr/local/include -Wall
-LDFLAGS = -L/scratch/ccremers/lib -L/usr/local/lib
-LOADLIBS = -lfl
-LDLIBS = -largtable2
-OPTIONS = ${CPPFLAGS} ${CFLAGS} ${LDFLAGS}
-
-#
-#	Module set for the modelchecker
-#
-MODULES=memory.o terms.o termlists.o symbols.o knowledge.o runs.o modelchecker.o \
-report.o debug.o  mgu.o substitutions.o \
-match_basic.o \
-match_clp.o constraints.o \
-output.o latex.o \
-varbuf.o tracebuf.o attackminimize.o \
-tac.o parser.o compiler.o 
-
-#
-#	Dependencies
-#
-MODELCHECKER = ${MODULES} main.o
-
-all:		scyther tags
-
-${Target}.o:	${Target}.c
-		$(CC) $(OPTIONS) ${Target}.c -c
-
-scanner.c:	scanner.lex
-		flex scanner.lex
-		cp lex.yy.c scanner.c
-
-tok.h:		parser.c
-
-parser.c:	parser.y
-		bison -d -v parser.y
-		cp parser.tab.c parser.c
-		cmp -s parser.tab.h tok.h || cp parser.tab.h tok.h
-
-tags:		*.c *.h
-		ctags *.c *.h
-
-modules:	$(MODULES)
-
-scyther:	scanner.o $(MODELCHECKER)
-		$(CC) $(OPTIONS) $(MODELCHECKER) -o scyther $(LOADLIBS) $(LDLIBS)
-
-ptestmain.o scanner.o	: tok.h
-
-#
-#	Cleanup
-#
-clean:
-		rm -f *.o
-		rm -f scyther
-		rm -f scanner.c
-		rm -f parser.c
-		rm -f tok.h
-#
-#	Clean and rebuild: 'make new'
-#
-new:
-		make clean
-		make all
-
-#
-#	Make doxygen reference manuals. (in ../refman)
-#
-refman:		doxyconfig
-		doxygen doxyconfig
-
diff --git a/src/bugs.txt b/src/bugs.txt
deleted file mode 100644
index 98e77b0..0000000
--- a/src/bugs.txt
+++ /dev/null
@@ -1,119 +0,0 @@
---+++ Crititcal Bugs
-
-   * soph segfaults at no switch or -r4 (-r3 is okay??) using non-debug version.
-   * './scyther -a ../spdl/nsl3.spdl --increment-runs' segfaults. The main reason is that the Archne engine uses runs in a different way.
-     Maybe it is best to disable --increment rules for non-ModelChecker verification.
-
----+++ Bugs
-
-   * Problem with goal bindings: instantiation of variable with a tuple might
-  introduce a tuple goal, which is forbidden. We must find a way to deal with this. This typically occurs in type flaw searches.
-   * Arachne seems to trip over claims with empty prec sets. Maybe we
-  simply should not test these.
-   * Splice/AS does not work well because priority key search stumbles over the
-  public key search stuff. That is a flaw in the heuristic: we should not look
-  for anything that is in the intruder knowledge already. In fact, it is a
-  problem with branching. We should not look for PK(X), even if X is a
-  variable. Priority should go to keys of which the constructor is not in M_0,
-  maybe that heuristic works.
-  However, there seems to be an infinite loop for this in the algorithm, which
-  I did not anticipate. Investigate!
-  <br>
-  Maybe self-loops are the problem. This has to do with tuple alternation
-  decoding. Consider re-introducing explicit intruder strands OR self-loop
-  pruning.
-
----+++ Would like to have
-
----++++ ArachneEngine
-
-   * There is no good test on the correct workings of
-     add_goals/destruction of these. We can test this if after
-     termination, we have 0 goals; for this we need to store the
-     initially added goals as well. Furthermore, we can generate an
-     error when <0 goals occur.
-   * Consider where in Arachne dependency graph is used. If this is only for
-     pruning states, we can construct it there only. However, the base 'role
-     defs/bindings' graph might be re-used.
-   * Add switch for arachne to prune encryption levels when using -m2.
-   * To store attacks for arachne, maybe the following is needed:
-      * The roles for each run
-      * The variable bindings for all (local) variables
-      * The goal bindings
-   * Agent terms must have keylevel 0; enforce this!
-   * Select_goal should consider, for singular variables, whether their
-     type can be found in M_0. If so, the goal can be ignored.
-   * Fix 'never sent secrets' list, that are e.g. secret keys of regular agents
-     and such. The intruder can never learn these, we need this for pruning.
-     If a goal is such a term, we prune. Investigate how this can be incorporated.
-     Investigate also whether this actually makes a difference.
-   * Make 'generate_trace_bindings' to create the bindings for a given trace.
-     Note that there can be multiple solutions; for now, simply try to take the
-     shortest one.
-
----++++ ModelChecker
-
-   * For secrecy, one trusted agent and one untrusted agent suffices.
-     Implement this in the modelchecker.
-   * Implement delayed protocol compiler (on run demand only) for the modelchecker?
-
----++++ Misc
-
-   * Make different error codes for compilation error/ other error. This can be
-     useful for scripts. However, it might shift some constants for the Elegast
-     scripts.
-   * Rewrite termMguTerm such that it iterates and adapt all functions
-     using it. This is to allow for associative tupling later.
-   * Fix constants in intruder knowledge. Auto add single one of each type,
-     when typed expl. Add single constant when untyped. Fix this also in
-     semantics, and add proof to establish sufficiency.
-   * Fix function handling (signatures).
-   * Move initial intruder knowledge maybe into the title of the MSC.
-   * Implement run knowledge, and use this in protocol compiler.
-   * Introduce 'Ticket' default type in the compiler, along with some
-     handling for that.
-   * The 'choose' operator must always be typed, I think. Yes.
-   * The woolam-ce is incorrect because it is illegal to have a variable
-     term in a key that is read, by CMV semantics. I don't know what it
-     means for CE semantics (yet).
-   * Idea: run bla.bla(params) [compromised <localterm> [,<localterm>] ];
-      1. These local terms are given to the intruder. Technically this
-         should only happen _after_ they are first sent in the run. Maybe add
-         this to send semantics: if termOccurs(sendterm, compromisedterm) then
-         add compromisedterm to M, remove compromisedterm from list of terms to
-         compromise.
-      1. All claims in the run are ignored (add untrusted flag to run)
-         Alternative: run x.x(x) untrusted; or just compromised, to give up
-         all constants.
-         Note this is not sufficient yet, because it does not consider any
-         partner runs. Maybe declare a 'compromised' section first; other runs
-         will only activate after these have completed. Note this is much more
-         expensive.
-   * Woolam-ce gives nothing. But then again, it's a wrong impl.
-   * Global/protocol variables should not exist in the current system.
-   * run nsl.initiator(alice, all Agent) constructs?
-      * 'all' would generate the roles with the corresponding type.
-      * or maybe for clarity/complexity control: use 'runs' for constructs
-        with 'all' in it.
-   * Maybe function application ought to be a different basic term type.
-   * After role construction, msc consistency can be checked.
-   * Reduce knowledge to a simple term list? That would simplify a number
-     of things, and also allow for easier addition of stuff.
-   * How is % notation handled in Casper?
-   * Vernam encryption?
-
----++++ ConstraintLogic (and thus obsolete)
-
-   * CLP: variables in keys must be branched: maybe even in three situations
-     (have key and contents, have inverse key and content, nothing)
-   * How should claims behave (trusted/untrusted) wrt uninstantiated
-     agents? Branch again? That's what is causing the nsl3-var problem.
-   * Constraints might be a part of a knowledge thing, because with we
-     might now have a number of local knowledge sets, each with their own
-     constraint sets. That doesn't make it easier though :( and will cause
-     some performance loss I suppose. Each local set has to remain
-     solveable as well.
-   * Issue: how do untrusted claims work in the context of an intruder?
-     Claim must be checked if it can be solved such that at least one of
-     the agents is trusted.
-
diff --git a/src/compile.txt b/src/compile.txt
index 71e32d5..d472837 100644
--- a/src/compile.txt
+++ b/src/compile.txt
@@ -6,13 +6,19 @@ Needed:
 	
   gcc
   	If you don't know what this is, please stop reading.
-  scons
-	A Python script set to replace the make etc. toolchain.
+  cmake
+	A Makefile generator, available on almost any platform.
 
 For cross-compilation (Windows):
 
   [mingw32][universe]
   	GCC variant to compile for windows + w32 binutils.
 
-	Use 'scons arch=windows' to generate the binary.
+
+The best is to simply execute:
+
+  ./build.sh
+
+This should compile everything for your platform and will copy the
+binaries into the correct location.
 
diff --git a/src/language.txt b/src/language.txt
deleted file mode 100644
index a3e84ba..0000000
--- a/src/language.txt
+++ /dev/null
@@ -1,46 +0,0 @@
-Language
---------
-
-language	:= (<def>)*
-def		:= (<directive> | <protocol> | <rundef> | <unstrusted>)
-
-//directive	:= <dir_require>
-//dir_require	:= require <filename>;
-
-protocol	:= protocol <protocolname> ( <rolelist> ) { <roledef>* } optsc
-protocolname	:= <id>
-
-intruderknow	:= public <termlist>;
-roledef		:= role <rolename> { <actions> } optsc
-rolename	:= <id> 
-actions		:= (<action>;)+
-action		:= (<read> | <send> | <claim>)
-decl		:= (<const> | <var>)+
-const		:= const <termlist> [ : <typeterm> ];
-var		:= var <termlist> [ : <typelist> ];
-
-read		:= read [_<label>]  (<term>,<term>,<term>);
-send		:= send [_<label>]  (<term>,<term>,<term>);
-claim		:= claim [_<label>] (<term>,<termlist>);
-label		:= <id>;
-
-rundef		:= <protocolname>.<rolename> ( <instancelist> ) ;
-instancelist	:= (<agent>|<typeterm>)*
-
-agent		:= <term>
-typeterm	:= <term>
-typelist	:= <termlist>
-
-untrusted	:= untrusted <termlist>;
-
-termlist	:= <term> [, <termlist>]
-term		:= (<baseterm> | <encterm> | <tupleterm> | <function>)
-encterm		:= { <term> } <term>
-function	:= <term> ( <term> )
-baseterm	:= (<variable> | <const>)
-variable	:= <id>
-const		:= <id>
-
-optsc		:= [ ; ]
-id		:= (<digit>|<uppercase>|<lowercase>)+
-
diff --git a/src/license.txt b/src/license.txt
deleted file mode 100644
index f997d64..0000000
--- a/src/license.txt
+++ /dev/null
@@ -1,3 +0,0 @@
-- GNU getopt
-- GNU bison/flex
-- de rest (c) Cas
diff --git a/src/notes.txt b/src/notes.txt
deleted file mode 100644
index 6e52578..0000000
--- a/src/notes.txt
+++ /dev/null
@@ -1,17 +0,0 @@
-- (!!) Are the Arachne rules for keys that are variables sane? E.g. what
-  is their inverse key? Check! Intuition: one cannot know what the
-  inverse is of a non-instantiated key variable, given the current
-  semantics, if asymmetric keys are allowed.
-  Consequence: the current implementation is just fine, because
-  asymmetric key variables cannot be defined in the language. Thus, the
-  rules are fine. Investigate for the other case.
-- If no attack/state output is needed, maybe the attack heuristic should
-  be simpler (which means just weighting the trace length etc.) in order
-  to avoid uneccesary continuation of the search. Maybe even stop
-  altogether after finding *an* attack.
-- For the TimeStamps etc, we can implement an 'auto-leak' of such local
-  constants. This should works also with a modifier of sorts (e.g.
-  'predictable') and such constants should be leaked to the intruder at
-  the start of the run, possibly by prefixing a send.
-- knowledgeAddTerm might be improved by scanning through key list only with
-  things that are newly added.
diff --git a/src/problem.spdl b/src/problem.spdl
deleted file mode 100644
index 64d754f..0000000
--- a/src/problem.spdl
+++ /dev/null
@@ -1,25 +0,0 @@
-// BAN modified version of the yahalom protocol
-// Type flaw
-
-usertype Server;
-
-const a,b,c : Agent;
-const s : Server;
-secret k : Function;
-
-protocol yahalomBan(A,B,S)
-{
-	role B
-	{
-		const nb;
-		var na;
-		var kab;
-
-		read_!1(A,B, A,na,B,S);
-		send_!2(B,S, B,nb, {A,na}k(B,S) );
-		read_!4(A,B, {A,kab,nb}k(B,S) , {nb}kab );
-		claim_6(B, Secret,kab);
-	}
-}
-
-
diff --git a/src/todo.txt b/src/todo.txt
index 595b7c1..07acec6 100644
--- a/src/todo.txt
+++ b/src/todo.txt
@@ -14,9 +14,9 @@
   cumbersome and might impact on performance. Alternatively, iterators
   can be implemented as macros, which is probably the fastest, but maybe
   less readable.
-- --check is slightly f***ed up because there is no good semantics for
-  the --disable intruder check. As a result, it is now too strict can
-  cause correct protocols to fail. Fix.
+- The (currently not advised) switch --check is slightly off because
+  there is no good semantics for the --disable intruder check. As a
+  result, it is now too strict can cause correct protocols to fail. Fix.
 - When *not* asking for attack output, maybe we should default to
   --prune = 1. Then, if we ask for --xml output or --dot, we do:
   if --prune == 1 then --prune == 2 now :) unless otherwise specified.
@@ -52,3 +52,21 @@
 - SConstruct file should check whether ctags actually exists (avoiding
   errors)
 - Proof output should be XML, with an external converter to dot format.
+- Are the Arachne rules for keys that are variables sufficiently sane in
+  general? E.g. what is their inverse key? Intuition: one cannot know
+  what the inverse is of a non-instantiated key variable, given the
+  current semantics, if asymmetric keys are allowed.  Consequence: the
+  current implementation is just fine, because asymmetric key variables
+  cannot be defined in the language. Thus, the rules are fine.
+  Investigate for future extensions what the consequences of this are.
+- If no attack/state output is needed, maybe the attack heuristic should
+  be simpler (which means just weighting the trace length etc.) in order
+  to avoid uneccesary continuation of the search. Maybe even stop
+  altogether after finding *an* attack.
+- For the TimeStamps etc, we can implement an 'auto-leak' of such local
+  constants. This should works also with a modifier of sorts (e.g.
+  'predictable') and such constants should be leaked to the intruder at
+  the start of the run, possibly by prefixing a send.
+- knowledgeAddTerm might be improved by scanning through key list only with
+  things that are newly added.
+