diff --git a/spdl/SPORE/denning-sacco-lowe.spdl b/spdl/SPORE/denning-sacco-lowe.spdl
index 2c4bb10..00af7e8 100644
--- a/spdl/SPORE/denning-sacco-lowe.spdl
+++ b/spdl/SPORE/denning-sacco-lowe.spdl
@@ -5,14 +5,13 @@
 #
 # Note:
 # This protocol uses a ticket so scyther will only be able to verify
-# the protocol using the ARACHNE engine (-a) and type 2 matching (-m2)
+# the protocol using the ARACHNE engine (-a)
 #
 # Note:
 # According to SPORE there are no attacks on this protocol, scyther
 # finds one however. This has to be investigated further.
 
 usertype Key;
-usertype Ticket;
 usertype SessionKey;
 usertype TimeStamp;
 secret k: Function;
diff --git a/spdl/SPORE/denning-sacco.spdl b/spdl/SPORE/denning-sacco.spdl
index 2b27823..45af828 100644
--- a/spdl/SPORE/denning-sacco.spdl
+++ b/spdl/SPORE/denning-sacco.spdl
@@ -5,11 +5,10 @@
 #
 # Note:
 # This protocol uses a ticket so scyther will only be able to verify
-# the protocol using the ARACHNE engine (-a) and type 2 matching (-m2)
+# the protocol using the ARACHNE engine (-a) 
 #
 
 usertype Key;
-usertype Ticket;
 usertype SessionKey;
 usertype TimeStamp;
 secret k: Function;
@@ -25,7 +24,8 @@ protocol denningSacco(I,R,S)
         send_1(I,S, I,R );
         read_2(S,I, {R, Kir, T, W}k(I,S) );
         send_3(I,R, W);
-        claim_4(I,Nisynch);
+        claim_I1(I,Niagree);
+        claim_I2(I,Nisynch);
     }    
     
     role R
@@ -34,7 +34,9 @@ protocol denningSacco(I,R,S)
         var T: TimeStamp;
 
         read_3(I,R, {Kir,I,T}k(R,S));
-        claim_8(R,Nisynch);
+        claim_R1(R,Niagree);
+        claim_R2(R,Nisynch);
+
     }
     
     role S
diff --git a/spdl/SPORE/kaochow-v2.spdl b/spdl/SPORE/kaochow-v2.spdl
index b8007b3..447e6e6 100644
--- a/spdl/SPORE/kaochow-v2.spdl
+++ b/spdl/SPORE/kaochow-v2.spdl
@@ -5,11 +5,10 @@
 #
 # Note:
 # This protocol uses a ticket so scyther will only be able to verify
-# the protocol using the ARACHNE engine (-a) and type 2 matching (-m2)
+# the protocol using the ARACHNE engine (-a)
 #
 
 usertype Sessionkey;
-usertype Ticket;
 secret k: Function;
 
 protocol kaochow2(I,R,S)
diff --git a/spdl/SPORE/kaochow-v3.spdl b/spdl/SPORE/kaochow-v3.spdl
index 11a2a3d..a01c8d8 100644
--- a/spdl/SPORE/kaochow-v3.spdl
+++ b/spdl/SPORE/kaochow-v3.spdl
@@ -5,11 +5,10 @@
 #
 # Note:
 # This protocol uses a ticket so scyther will only be able to verify
-# the protocol using the ARACHNE engine (-a) and type 2 matching (-m2)
+# the protocol using the ARACHNE engine (-a)
 #
 
 usertype Sessionkey;
-usertype Ticket;
 usertype Timestamp;
 secret k: Function;
 
diff --git a/spdl/SPORE/kaochow.spdl b/spdl/SPORE/kaochow.spdl
index c9eca39..55b1bb3 100644
--- a/spdl/SPORE/kaochow.spdl
+++ b/spdl/SPORE/kaochow.spdl
@@ -5,11 +5,10 @@
 #
 # Note:
 # This protocol uses a ticket so scyther will only be able to verify
-# the protocol using the ARACHNE engine (-a) and type 2 matching (-m2)
+# the protocol using the ARACHNE engine (-a) 
 #
 
 usertype Sessionkey;
-usertype Ticket;
 secret k: Function;
 
 protocol kaochow(I,R,S)
diff --git a/spdl/SPORE/ksl-lowe.spdl b/spdl/SPORE/ksl-lowe.spdl
index 25e8da3..001bc59 100644
--- a/spdl/SPORE/ksl-lowe.spdl
+++ b/spdl/SPORE/ksl-lowe.spdl
@@ -5,13 +5,13 @@
 #
 # Note:
 # This protocol uses a ticket so scyther will only be able to verify
-# the protocol using the ARACHNE engine (-a) and type 2 matching (-m2)
+# the protocol using the ARACHNE engine (-a)
 #
 # Note:
 # According to SPORE there are no attacks on this protocol, scyther
 # finds one however. This has to be investigated further.
 
-usertype Server, SessionKey, GeneralizedTimestamp, Ticket, TicketKey;
+usertype Server, SessionKey, GeneralizedTimestamp, TicketKey;
 secret k: Function;
 
 const a, b, e: Agent;
diff --git a/spdl/SPORE/ksl.spdl b/spdl/SPORE/ksl.spdl
index bbb2c31..196bd36 100644
--- a/spdl/SPORE/ksl.spdl
+++ b/spdl/SPORE/ksl.spdl
@@ -5,11 +5,11 @@
 #
 # Note:
 # This protocol uses a ticket so scyther will only be able to verify
-# the protocol using the ARACHNE engine (-a) and type 2 matching (-m2)
+# the protocol using the ARACHNE engine (-a)
 #
 
 
-usertype Server, SessionKey, GeneralizedTimestamp, Ticket, TicketKey;
+usertype Server, SessionKey, GeneralizedTimestamp, TicketKey;
 secret k: Function;
 
 const a, b, e: Agent;
diff --git a/spdl/SPORE/needham-schroeder-sk-amend.spdl b/spdl/SPORE/needham-schroeder-sk-amend.spdl
index 656a140..b25fdec 100644
--- a/spdl/SPORE/needham-schroeder-sk-amend.spdl
+++ b/spdl/SPORE/needham-schroeder-sk-amend.spdl
@@ -6,7 +6,7 @@
 #
 # Note:
 # This protocol uses a ticket so scyther will only be able to verify
-# the protocol using the ARACHNE engine (-a) and type 2 matching (-m2)
+# the protocol using the ARACHNE engine (-a)
 #
 # Note:
 # According to SPORE there are no attacks on this protocol, scyther
@@ -19,7 +19,6 @@ secret k: Function;
 const dec,inc: Function;
 inversekeys(dec,inc);
 usertype SessionKey;
-usertype Ticket;
 
 protocol needhamschroederskamend(I,R,S)
 {
diff --git a/spdl/SPORE/needham-schroeder-sk.spdl b/spdl/SPORE/needham-schroeder-sk.spdl
index 851d440..3ef425d 100644
--- a/spdl/SPORE/needham-schroeder-sk.spdl
+++ b/spdl/SPORE/needham-schroeder-sk.spdl
@@ -6,7 +6,7 @@
 #
 # Note:
 # This protocol uses a ticket so scyther will only be able to verify
-# the protocol using the ARACHNE engine (-a) and type 2 matching (-m2)
+# the protocol using the ARACHNE engine (-a)
 #
 
 
@@ -15,7 +15,6 @@ secret k: Function;
 const dec,inc: Function;
 inversekeys(dec,inc);
 usertype SessionKey;
-usertype Ticket;
 
 protocol needhamschroedersk(I,R,S)
 {
diff --git a/spdl/SPORE/neumannstub-hwang.spdl b/spdl/SPORE/neumannstub-hwang.spdl
index ed76187..42d9f02 100644
--- a/spdl/SPORE/neumannstub-hwang.spdl
+++ b/spdl/SPORE/neumannstub-hwang.spdl
@@ -5,14 +5,14 @@
 #
 # Note:
 # This protocol uses a ticket so scyther will only be able to verify
-# the protocol using the ARACHNE engine (-a) and type 2 matching (-m2)
+# the protocol using the ARACHNE engine (-a)
 #
 # Note:
 # According to SPORE there are no attacks on this protocol, scyther
 # finds one however. This has to be investigated further.
 
 
-usertype Server, SessionKey, TimeStamp, Ticket, TicketKey;
+usertype Server, SessionKey, TimeStamp, TicketKey;
 secret k: Function;
 
 const a, b, e: Agent;
diff --git a/spdl/SPORE/neumannstub.spdl b/spdl/SPORE/neumannstub.spdl
index b551818..d3edd95 100644
--- a/spdl/SPORE/neumannstub.spdl
+++ b/spdl/SPORE/neumannstub.spdl
@@ -5,11 +5,11 @@
 #
 # Note:
 # This protocol uses a ticket so scyther will only be able to verify
-# the protocol using the ARACHNE engine (-a) and type 2 matching (-m2)
+# the protocol using the ARACHNE engine (-a)
 #
 
 
-usertype Server, SessionKey, TimeStamp, Ticket, TicketKey;
+usertype Server, SessionKey, TimeStamp, TicketKey;
 secret k: Function;
 
 const a, b, e: Agent;
diff --git a/spdl/SPORE/otwayrees.spdl b/spdl/SPORE/otwayrees.spdl
index f6fd1d8..5700104 100644
--- a/spdl/SPORE/otwayrees.spdl
+++ b/spdl/SPORE/otwayrees.spdl
@@ -6,13 +6,13 @@
 #
 # Note:
 # This protocol uses a ticket so scyther will only be able to verify
-# the protocol using the ARACHNE engine (-a) and type 2 matching (-m2)
+# the protocol using the ARACHNE engine (-a)
 #
 
 
 secret const k : Function;
 
-usertype String,SessionKey,Ticket;
+usertype String,SessionKey;
 
 protocol otwayrees(I,R,S)
 {
diff --git a/spdl/SPORE/smartright.spdl b/spdl/SPORE/smartright.spdl
index d2d27cb..b533834 100644
--- a/spdl/SPORE/smartright.spdl
+++ b/spdl/SPORE/smartright.spdl
@@ -8,7 +8,7 @@
 #
 # Note:
 # This protocol uses a ticket so scyther will only be able to verify
-# the protocol using the ARACHNE engine (-a) and type 2 matching (-m2)
+# the protocol using the ARACHNE engine (-a)
 #
 # Note:
 # Scyther finds an attack because the value of VoR in te last message can
@@ -19,7 +19,6 @@ secret unhash: Function;
 secret k: Function;
 inversekeys (hash,unhash);
 usertype SessionKey;
-usertype Ticket;
 usertype XorKey;
 const Vor: XorKey;
 
diff --git a/spdl/SPORE/woo-lam-pi-1.spdl b/spdl/SPORE/woo-lam-pi-1.spdl
index 945043f..b03641e 100644
--- a/spdl/SPORE/woo-lam-pi-1.spdl
+++ b/spdl/SPORE/woo-lam-pi-1.spdl
@@ -5,11 +5,9 @@
 #
 # Note:
 # This protocol uses a ticket so scyther will only be able to verify
-# the protocol using the ARACHNE engine (-a) and type 2 matching (-m2)
+# the protocol using the ARACHNE engine (-a)
 #
 
-usertype Ticket;
-
 secret k: Function;
 
 protocol woolamPi1(I,R,S)
diff --git a/spdl/SPORE/woo-lam-pi-2.spdl b/spdl/SPORE/woo-lam-pi-2.spdl
index 11d5faf..e7d7d5a 100644
--- a/spdl/SPORE/woo-lam-pi-2.spdl
+++ b/spdl/SPORE/woo-lam-pi-2.spdl
@@ -5,11 +5,9 @@
 #
 # Note:
 # This protocol uses a ticket so scyther will only be able to verify
-# the protocol using the ARACHNE engine (-a) and type 2 matching (-m2)
+# the protocol using the ARACHNE engine (-a)
 #
 
-usertype Ticket;
-
 secret k: Function;
 
 protocol woolamPi2(I,R,S)
diff --git a/spdl/SPORE/woo-lam-pi-3.spdl b/spdl/SPORE/woo-lam-pi-3.spdl
index 06e7237..98df50f 100644
--- a/spdl/SPORE/woo-lam-pi-3.spdl
+++ b/spdl/SPORE/woo-lam-pi-3.spdl
@@ -5,11 +5,9 @@
 #
 # Note:
 # This protocol uses a ticket so scyther will only be able to verify
-# the protocol using the ARACHNE engine (-a) and type 2 matching (-m2)
+# the protocol using the ARACHNE engine (-a)
 #
 
-usertype Ticket;
-
 secret k: Function;
 
 protocol woolamPi3(I,R,S)
diff --git a/spdl/SPORE/woo-lam-pi-f.spdl b/spdl/SPORE/woo-lam-pi-f.spdl
index 72680bf..5889b20 100644
--- a/spdl/SPORE/woo-lam-pi-f.spdl
+++ b/spdl/SPORE/woo-lam-pi-f.spdl
@@ -5,11 +5,9 @@
 #
 # Note:
 # This protocol uses a ticket so scyther will only be able to verify
-# the protocol using the ARACHNE engine (-a) and type 2 matching (-m2)
+# the protocol using the ARACHNE engine (-a)
 #
 
-usertype Ticket;
-
 secret k: Function;
 
 protocol woolamPif(I,R,S)
diff --git a/spdl/SPORE/woo-lam-pi.spdl b/spdl/SPORE/woo-lam-pi.spdl
index fc8385f..7aea09a 100644
--- a/spdl/SPORE/woo-lam-pi.spdl
+++ b/spdl/SPORE/woo-lam-pi.spdl
@@ -5,15 +5,13 @@
 #
 # Note:
 # This protocol uses a ticket so scyther will only be able to verify
-# the protocol using the ARACHNE engine (-a) and type 2 matching (-m2)
+# the protocol using the ARACHNE engine (-a)
 #
 # Note:
 # Scyther finds an attack that appears to be legit, but is not present in 
 # SPORE.
 #
 
-usertype Ticket;
-
 secret k: Function;
 
 protocol woolamPi(I,R,S)
diff --git a/spdl/SPORE/woo-lam.spdl b/spdl/SPORE/woo-lam.spdl
index fc1b160..b20a259 100644
--- a/spdl/SPORE/woo-lam.spdl
+++ b/spdl/SPORE/woo-lam.spdl
@@ -5,12 +5,11 @@
 #
 # Note:
 # This protocol uses a ticket so scyther will only be able to verify
-# the protocol using the ARACHNE engine (-a) and type 2 matching (-m2)
+# the protocol using the ARACHNE engine (-a)
 #
 
 
 usertype Key;
-usertype Ticket;
 
 secret k: Function;
 
diff --git a/spdl/SPORE/yahalom-ban.spdl b/spdl/SPORE/yahalom-ban.spdl
index f4eb64e..bc973b7 100644
--- a/spdl/SPORE/yahalom-ban.spdl
+++ b/spdl/SPORE/yahalom-ban.spdl
@@ -5,12 +5,12 @@
 #
 # Note:
 # This protocol uses a ticket so scyther will only be able to verify
-# the protocol using the ARACHNE engine (-a) and type 2 matching (-m2)
+# the protocol using the ARACHNE engine (-a) 
 #
 
 secret k : Function;
 
-usertype Ticket, Key;
+usertype Key;
 
 
 protocol yahalomBAN(I,R,S)
@@ -50,8 +50,8 @@ protocol yahalomBAN(I,R,S)
         const Kir: Key;
         var Ni,Nr: Nonce;
 
-        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) );
+        read_2(R,S, R, Nr, {I,Ni}k(R,S) );
+        send_3(S,I, Nr, {R,Kir,Ni}k(I,S), {I,Kir,Nr}k(R,S) );
     }
 }
 
diff --git a/spdl/SPORE/yahalom-paulson.spdl b/spdl/SPORE/yahalom-paulson.spdl
index b94aa96..c2340a5 100644
--- a/spdl/SPORE/yahalom-paulson.spdl
+++ b/spdl/SPORE/yahalom-paulson.spdl
@@ -5,12 +5,12 @@
 #
 # Note:
 # This protocol uses a ticket so scyther will only be able to verify
-# the protocol using the ARACHNE engine (-a) and type 2 matching (-m2)
+# the protocol using the ARACHNE engine (-a)
 #
 
 secret k : Function;
 
-usertype Ticket, Key;
+usertype Key;
 
 
 protocol yahalomPaulson(I,R,S)
diff --git a/spdl/SPORE/yahalom.spdl b/spdl/SPORE/yahalom.spdl
index d30354c..46ee432 100644
--- a/spdl/SPORE/yahalom.spdl
+++ b/spdl/SPORE/yahalom.spdl
@@ -5,12 +5,12 @@
 #
 # Note:
 # This protocol uses a ticket so scyther will only be able to verify
-# the protocol using the ARACHNE engine (-a) and type 2 matching (-m2)
+# the protocol using the ARACHNE engine (-a) 
 #
 
 secret k : Function;
 
-usertype Ticket, Key;
+usertype Key;
 
 
 protocol yahalom(I,R,S)