Update SPORE protocols to use new ticket mechanism:

- Use builtin Ticket type instead of user type
- Remove remark that -m2 matching is required as it no longer is

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;

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

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)

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;
 

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)

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;

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;

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)
 {

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)
 {

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;

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;

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)
 {

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;
 

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)

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)

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)

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)

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)

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;
 

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) );
     }
 }
 

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)

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)