From 635e58303977b27ddfd7d333ce7c8e2557541184 Mon Sep 17 00:00:00 2001 From: ccremers Date: Sun, 22 Feb 2004 15:22:19 +0000 Subject: [PATCH] - Modified everything for explicit usertype declarations. --- spdl/bkepk-ce.spdl | 2 ++ spdl/bkepk.spdl | 2 ++ spdl/otwayrees.spdl | 2 ++ spdl/tls-paulson.spdl | 2 ++ spdl/wmf-brutus.spdl | 1 + spdl/woolam-ce.spdl | 1 + spdl/woolam-cmv.spdl | 1 + spdl/yahalom-ban.spdl | 4 +++- spdl/yahalom-lowe.spdl | 2 ++ 9 files changed, 16 insertions(+), 1 deletion(-) diff --git a/spdl/bkepk-ce.spdl b/spdl/bkepk-ce.spdl index a3ae138..84398dc 100644 --- a/spdl/bkepk-ce.spdl +++ b/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; diff --git a/spdl/bkepk.spdl b/spdl/bkepk.spdl index 60e485d..4dff6a1 100644 --- a/spdl/bkepk.spdl +++ b/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; diff --git a/spdl/otwayrees.spdl b/spdl/otwayrees.spdl index c91d277..710285a 100644 --- a/spdl/otwayrees.spdl +++ b/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 diff --git a/spdl/tls-paulson.spdl b/spdl/tls-paulson.spdl index 24064d1..d157f6f 100644 --- a/spdl/tls-paulson.spdl +++ b/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); diff --git a/spdl/wmf-brutus.spdl b/spdl/wmf-brutus.spdl index 10f13fb..d9068a2 100644 --- a/spdl/wmf-brutus.spdl +++ b/spdl/wmf-brutus.spdl @@ -1,3 +1,4 @@ +usertype SesKey, Server; secret const k : Function; /* Version from the Brutus reports diff --git a/spdl/woolam-ce.spdl b/spdl/woolam-ce.spdl index 1eb4dbe..5d67606 100644 --- a/spdl/woolam-ce.spdl +++ b/spdl/woolam-ce.spdl @@ -1,3 +1,4 @@ +usertype Server, SessionKey, Token, SymmetricKey; secret k: Function; const Alice, Bob, Charlie, Eve: Agent; diff --git a/spdl/woolam-cmv.spdl b/spdl/woolam-cmv.spdl index 15fbec9..47407a1 100644 --- a/spdl/woolam-cmv.spdl +++ b/spdl/woolam-cmv.spdl @@ -1,3 +1,4 @@ +usertype Server, SessionKey, Token, Ticket; secret k: Function; const Alice, Bob, Charlie, Eve: Agent; diff --git a/spdl/yahalom-ban.spdl b/spdl/yahalom-ban.spdl index 17d407a..fa620c4 100644 --- a/spdl/yahalom-ban.spdl +++ b/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; diff --git a/spdl/yahalom-lowe.spdl b/spdl/yahalom-lowe.spdl index 4590210..edee78d 100644 --- a/spdl/yahalom-lowe.spdl +++ b/spdl/yahalom-lowe.spdl @@ -1,5 +1,7 @@ // Yahalom protocol +usertype Sessionkey; + const a,b,s,Eve : Agent; secret k : Function;