- Modified everything for explicit usertype declarations.

spdl/bkepk-ce.spdl

@@ -5,6 +5,8 @@
 	Tried to stay as close as possible to compare timing results.
 */
 
+usertype Key;
+
 const pk,hash: Function;
 secret sk: Function;
 

spdl/bkepk.spdl

@@ -5,6 +5,8 @@
 	Tried to stay as close as possible to compare timing results.
 */
 
+usertype Key;
+
 const pk,hash: Function;
 secret sk,unhash: Function;
 

spdl/otwayrees.spdl

@@ -4,6 +4,8 @@ secret const k : Function;
    http://www.lsv.ens-cachan.fr/spore/otwayRees.html
 */
 
+usertype String, SesKey, Ticket, Server;
+
 protocol otwayrees(A,B,S)
 {
 	role A

spdl/tls-paulson.spdl

@@ -5,6 +5,8 @@
 #define CLIENTK hash(sid,M,na,pa,a,nb,pb,b,false)
 #define SERVERK hash(sid,M,na,pa,a,nb,pb,b,true)
 
+usertype Params, Bool, SessionID;
+
 const pk,hash: Function;
 secret sk,unhash: Function;
 inversekeys(pk,sk);

spdl/wmf-brutus.spdl

@@ -1,3 +1,4 @@
+usertype SesKey, Server;
 secret const k : Function;
 
 /* Version from the Brutus reports

spdl/woolam-ce.spdl

@@ -1,3 +1,4 @@
+usertype Server, SessionKey, Token, SymmetricKey;
 secret k: Function;
 
 const Alice, Bob, Charlie, Eve: Agent;

spdl/woolam-cmv.spdl

@@ -1,3 +1,4 @@
+usertype Server, SessionKey, Token, Ticket;
 secret k: Function;
 
 const Alice, Bob, Charlie, Eve: Agent;

spdl/yahalom-ban.spdl

@@ -2,8 +2,10 @@
 // Type flaw
 // This version actually works!
 
+usertype Server;
+
 const a,b,c : Agent;
-const s : Simon;
+const s : Server;
 secret k : Function;
 
 

spdl/yahalom-lowe.spdl

@@ -1,5 +1,7 @@
 // Yahalom protocol
 
+usertype Sessionkey;
+
 const a,b,s,Eve : Agent;
 secret k : Function;