diff --git a/dist/NewVersion.txt b/dist/NewVersion.txt
index fe83179..ccec53b 100644
--- a/dist/NewVersion.txt
+++ b/dist/NewVersion.txt
@@ -1,7 +1,7 @@
 Where are the version numbers? (way too distributed)
 
-- Gui has a version number in Version.py
-- Scyther has release.h
+- Gui has a version number in Version.py. This is propagated into the
+  binary and into the archive name as well.
 - ChangeLog
 - Readme.txt
 
diff --git a/dist/makedist.sh b/dist/makedist.sh
index 2dab6b3..d86e3bb 100755
--- a/dist/makedist.sh
+++ b/dist/makedist.sh
@@ -18,11 +18,6 @@
 #
 #	Parameters
 
-RELEASE="scyther-1.0-beta6"
-
-ARCHIVE="$RELEASE.tgz"
-ZIPPED="$RELEASE.zip"
-
 #	Creates a temporary subdirectory here.
 TMPDIR=/tmp/scytherdist
 WORKNAME=scyther
@@ -40,8 +35,6 @@ MANUAL=scyther-manual.pdf
 
 WORKDIR=$TMPDIR/$WORKNAME
 CURDIR=$PWD
-DEST=$PWD/$ARCHIVE
-ZIPDEST=$PWD/$ZIPPED
 DOCDEST=$WORKDIR/doc
 
 #------------------------------------------------------------------------------
@@ -69,6 +62,14 @@ svn cat $DOCROOT/$MANUAL >$WORKDIR/$MANUAL
 #
 #	Collected all needed data, finish up
 
+TAGVERSION=`awk 'BEGIN { FS="\""; } { print $2; }' ../gui/Gui/Version.py`
+RELEASE="scyther-$TAGVERSION"
+
+ARCHIVE="$RELEASE.tgz"
+ZIPPED="$RELEASE.zip"
+DEST=$PWD/$ARCHIVE
+ZIPDEST=$PWD/$ZIPPED
+
 #	Compress
 cd $TMPDIR
 tar zcvf $DEST $WORKNAME
diff --git a/gui/Scyther/Bin/scyther-linux b/gui/Scyther/Bin/scyther-linux
index 9aa976d..d5f1a5f 100755
Binary files a/gui/Scyther/Bin/scyther-linux and b/gui/Scyther/Bin/scyther-linux differ
diff --git a/gui/Scyther/Bin/scyther-w32.exe b/gui/Scyther/Bin/scyther-w32.exe
index c05dfc9..450e684 100755
Binary files a/gui/Scyther/Bin/scyther-w32.exe and b/gui/Scyther/Bin/scyther-w32.exe differ
diff --git a/spdl/SPORE/neumannstub.spdl b/spdl/SPORE/neumannstub.spdl
index 14bef8a..a4c7ea1 100644
--- a/spdl/SPORE/neumannstub.spdl
+++ b/spdl/SPORE/neumannstub.spdl
@@ -13,8 +13,6 @@ usertype ExpiredTimeStamp;
 secret k: Function;
 
 const Alice, Bob, Simon, Eve: Agent;
-const Fresh: Function;
-const Compromised: Function;
 
 const ne: Nonce;
 const kee: SessionKey;
@@ -38,7 +36,6 @@ protocol neustub^Repeat(I,R,S)
         claim_I1(I,Secret, Kir);
         claim_I2(I,Niagree);
         claim_I3(I,Nisynch);
-        claim_I4(I,Empty,(Fresh,Kir));
     }
 
     role R
@@ -54,7 +51,6 @@ protocol neustub^Repeat(I,R,S)
         claim_R1(R,Secret, Kir);
         claim_R2(R,Niagree);
         claim_R3(R,Nisynch);
-        claim_R4(R,Empty,(Fresh,Kir));
     }
 
     role S 
@@ -78,7 +74,6 @@ protocol neustub(I,R,S)
         claim_I1(I,Secret, Kir);
         claim_I2(I,Niagree);
         claim_I3(I,Nisynch);
-        claim_I4(I,Empty,(Fresh,Kir));
     }
 
     role R
@@ -96,7 +91,6 @@ protocol neustub(I,R,S)
         claim_R1(R,Secret, Kir);
         claim_R2(R,Niagree);
         claim_R3(R,Nisynch);
-        claim_R4(R,Empty,(Fresh,Kir));
     }
 
     role S
diff --git a/spdl/SPORE/yahalom.spdl b/spdl/SPORE/yahalom.spdl
index a8a9d96..056db46 100644
--- a/spdl/SPORE/yahalom.spdl
+++ b/spdl/SPORE/yahalom.spdl
@@ -8,30 +8,6 @@
 secret k : Function;
 
 usertype SessionKey;
-const Fresh: Function;
-const Compromised: Function;
-
-protocol yahalom^KeyCompromise(C)
-{
-    // Read the names of 3 agents and disclose a session between them including
-    // corresponding session key to simulate key compromise
-    role C {
-        const Ni,Nr: Nonce;
-        const Kir: SessionKey;
-        var I,R,S: Agent;
-
-        read_!C1(C,C,    I,R,S);
-        send_!C2(C,C,    I,Ni,
-                        R,{I,Ni,Nr}k(R,S),
-                        {R,Kir,Ni,Nr}k(I,S),
-                        {I,Kir}k(R,S),
-                        {Nr}Kir,
-                        Kir
-               );
-        claim_C3(C,Empty, (Compromised,Kir));
-    }
-}
-
 
 protocol yahalom(I,R,S)
 {
@@ -47,8 +23,6 @@ protocol yahalom(I,R,S)
         send_4(I,R, T, {Nr}Kir );
 
         claim_I1(I, Secret,Kir);
-        claim_I2(I, Nisynch);
-        claim_I3(I, Empty, (Fresh,Kir));
     }
 
     role R
@@ -63,8 +37,6 @@ protocol yahalom(I,R,S)
         read_4(I,R, {I,Kir}k(R,S) , {Nr}Kir );
 
         claim_R1(R, Secret,Kir);
-        claim_R2(R, Nisynch);
-        claim_R3(R, Empty, (Fresh,Kir));
     }
 
     role S
@@ -74,8 +46,16 @@ protocol yahalom(I,R,S)
 
         read_2(R,S, R, {I,Ni,Nr}k(R,S) );
         send_3(S,I, {R,Kir,Ni,Nr}k(I,S), {I,Kir}k(R,S) );
+
+        claim(S, Secret, Ni);
+        claim(S, Secret, Nr);
     }
 }
 
 const Alice,Bob,Simon : Agent;
 
+const Eve: Agent;
+untrusted Eve;
+
+compromised k(Eve,Simon);
+
diff --git a/src/SVNVersion.cmake b/src/SVNVersion.cmake
index 484748a..a8350af 100644
--- a/src/SVNVersion.cmake
+++ b/src/SVNVersion.cmake
@@ -22,14 +22,9 @@ if (SVNVERSION_EXECUTABLE)
 	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")
-		if (UNIX)
-			# Unix system
-			# mark for dynamic generation in
-			# Makefile
-			set (SVNVERSION_DYNAMIC true)
-		endif (UNIX)
+		## 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)
@@ -47,13 +42,12 @@ if (SVNVERSION_DYNAMIC)
 		# current directory)
 		DEPENDS	${Scyther_sources}
 		DEPENDS .svn
-		COMMAND	echo
-		ARGS	"\\#define SVNVERSION \\\"`${SVNVERSION_EXECUTABLE}`\\\"" >version.h
-		COMMENT	"Generating subversion version information in version.h using svnversion command"
+		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")
+	file (WRITE version.h "#define SVNVERSION \"Unknown\"\n#define TAGVERSION \"Unknown\"")
 endif (SVNVERSION_DYNAMIC)
 
 # add the version number to the sources
diff --git a/src/release.h b/src/release.h
deleted file mode 100644
index 54479e7..0000000
--- a/src/release.h
+++ /dev/null
@@ -1 +0,0 @@
-#define RELEASEVERSION "1.0-beta 6"
diff --git a/src/subbuild-version-information.sh b/src/subbuild-version-information.sh
new file mode 100755
index 0000000..843815e
--- /dev/null
+++ b/src/subbuild-version-information.sh
@@ -0,0 +1,19 @@
+#!/bin/sh
+#
+# Arguments:
+#
+# svnversion executable path
+#
+
+SVNVERSION=`svnversion`
+TAGVERSION=`awk 'BEGIN { FS="\""; } { print $2; }' ../gui/Gui/Version.py`
+
+echo $SVNVERSION
+echo $TAGVERSION
+
+# Fix svnversion information
+echo "#define SVNVERSION \"$SVNVERSION\"" >version.h
+# Fix version tag
+echo "#define TAGVERSION \"$TAGVERSION\"" >>version.h
+
+
diff --git a/src/switches.c b/src/switches.c
index 40b69dc..5b4ac9f 100644
--- a/src/switches.c
+++ b/src/switches.c
@@ -15,8 +15,6 @@
 #include "error.h"
 #include "specialterm.h"
 
-#include "release.h"
-
 // Program name
 const char *progname = "scyther";
 
@@ -1245,7 +1243,7 @@ switcher (const int process, int index, int commandline)
       else
 	{
 	  printf ("'%s' model checker for security protocols.\n", progname);
-	  printf ("Version %s.\n", RELEASEVERSION);
+	  printf ("Version %s.\n", TAGVERSION);
 	  if (switches.expert)
 	    {
 #ifdef DEBUG