From f028d797d65cf559b9d2d8fd879be98df114b477 Mon Sep 17 00:00:00 2001 From: ccremers Date: Thu, 30 Nov 2006 15:28:01 +0000 Subject: [PATCH] - Added fixed version and checked it. --- spdl/misc/tls/tls-HSDDM05-fix.cpp | 74 +++++++++++++++++++++++++++++ spdl/misc/tls/tls-HSDDM05-fix.m4 | 75 ++++++++++++++++++++++++++++++ spdl/misc/tls/tls-HSDDM05-fix.spdl | 75 ++++++++++++++++++++++++++++++ 3 files changed, 224 insertions(+) create mode 100644 spdl/misc/tls/tls-HSDDM05-fix.cpp create mode 100644 spdl/misc/tls/tls-HSDDM05-fix.m4 create mode 100644 spdl/misc/tls/tls-HSDDM05-fix.spdl diff --git a/spdl/misc/tls/tls-HSDDM05-fix.cpp b/spdl/misc/tls/tls-HSDDM05-fix.cpp new file mode 100644 index 0000000..3b94979 --- /dev/null +++ b/spdl/misc/tls/tls-HSDDM05-fix.cpp @@ -0,0 +1,74 @@ +/* + * This is a model of a version of the TLS protocol as modeled by + * He,Sundararajan,Datta,Derek and Mitchell in the paper: "A modular + * correctness proof of IEEE 802.11i and TLS". + * + * This is the fixed version, with quite some differences: + * + * 1) new definition of handShake1 + * 2) changed order in msg3 + * + * (These are the suggestions made by Cas to Anupam Datta) + */ +#define CERT(a) { a,pk(a) }sk(Terence) +#define msg1 X,Nx,pa +#define msg2 Ny,pb,CERT(Y) +#define handShake1 msg1,msg2,{msecret}pk(Y) +#define msg3 CERT(X),{msecret}pk(Y),{handShake1}sk(X),hash(msecret,handShake1,clientstring) +#define handShake2 msg1,msg2,msg3 +#define msg4 hash(msecret,handShake2,serverstring) + + +/* below is just Scyther input and no further macro definitions */ + +usertype Params, String; + +const pk,hash: Function; +secret sk,unhash: Function; +inversekeys(pk,sk); +inversekeys(hash,unhash); + +const clientstring,serverstring: String; + +const Alice, Bob, Eve: Agent; +const Terence: Agent; + +protocol tls-HSDDM05(X,Y) +{ + role X + { + const Nx: Nonce; + const msecret: Nonce; + const pa: Params; + var Ny: Nonce; + var pb: Params; + + send_1( X,Y, msg1 ); + read_2( Y,X, msg2 ); + send_3( X,Y, msg3 ); + read_4( Y,X, msg4 ); + + claim_X1( X, Secret, msecret ); + } + + role Y + { + var Nx: Nonce; + var msecret: Nonce; + var pa: Params; + const Ny: Nonce; + const pb: Params; + + read_1( X,Y, msg1 ); + send_2( Y,X, msg2 ); + read_3( X,Y, msg3 ); + send_4( Y,X, msg4 ); + + claim_Y1( Y, Secret, msecret ); + } +} + + +untrusted Eve; +compromised sk(Eve); + diff --git a/spdl/misc/tls/tls-HSDDM05-fix.m4 b/spdl/misc/tls/tls-HSDDM05-fix.m4 new file mode 100644 index 0000000..5a96b3b --- /dev/null +++ b/spdl/misc/tls/tls-HSDDM05-fix.m4 @@ -0,0 +1,75 @@ +/* + * This is a model of a version of the TLS protocol as modeled by + * He,Sundararajan,Datta,Derek and Mitchell in the paper: "A modular + * correctness proof of IEEE 802.11i and TLS". + * + * This is the fixed version, with quite some differences: + * + * 1) new definition of handShake1 (including preceding tuples) + * 2) new definition of both handshakes (now hashed) + * 3) changed order in msg3 so msecret is part of handShake1 + * + * (These are the suggestions made by Cas to Anupam Datta) + */ +define(`CERTY',`{ Y,pk(Y) }sk(Terence)') +define(`CERTX',`{ X,pk(X) }sk(Terence)') +define(`msg1',`X,Nx,pa') +define(`msg2',`Ny,pb,CERTY') +define(`handShake1',`hash(msg1,msg2,{msecret}pk(Y))') +define(`msg3',`CERTX,{msecret}pk(Y),{handShake1}sk(X),hash(msecret,handShake1,clientstring)') +define(`handShake2',`hash(msg1,msg2,msg3)') +define(`msg4',`hash(msecret,handShake2,serverstring)') + +/* below is just Scyther input and no further macro definitions */ + +usertype Params, String; + +const pk,hash: Function; +secret sk,unhash: Function; +inversekeys(pk,sk); +inversekeys(hash,unhash); + +const clientstring,serverstring: String; + +const Alice, Bob, Eve: Agent; +const Terence: Agent; + +protocol tls-HSDDM05(X,Y) +{ + role X + { + const Nx: Nonce; + const msecret: Nonce; + const pa: Params; + var Ny: Nonce; + var pb: Params; + + send_1( X,Y, msg1 ); + read_2( Y,X, msg2 ); + send_3( X,Y, msg3 ); + read_4( Y,X, msg4 ); + + claim_X1( X, Secret, msecret ); + } + + role Y + { + var Nx: Nonce; + var msecret: Nonce; + var pa: Params; + const Ny: Nonce; + const pb: Params; + + read_1( X,Y, msg1 ); + send_2( Y,X, msg2 ); + read_3( X,Y, msg3 ); + send_4( Y,X, msg4 ); + + claim_Y1( Y, Secret, msecret ); + } +} + + +untrusted Eve; +compromised sk(Eve); + diff --git a/spdl/misc/tls/tls-HSDDM05-fix.spdl b/spdl/misc/tls/tls-HSDDM05-fix.spdl new file mode 100644 index 0000000..7bfdf81 --- /dev/null +++ b/spdl/misc/tls/tls-HSDDM05-fix.spdl @@ -0,0 +1,75 @@ +/* + * This is a model of a version of the TLS protocol as modeled by + * He,Sundararajan,Datta,Derek and Mitchell in the paper: "A modular + * correctness proof of IEEE 802.11i and TLS". + * + * This is the fixed version, with quite some differences: + * + * 1) new definition of handShake1 (including preceding tuples) + * 2) new definition of both handshakes (now hashed) + * 3) changed order in msg3 so msecret is part of handShake1 + * + * (These are the suggestions made by Cas to Anupam Datta) + */ + + + + + + + + + +/* below is just Scyther input and no further macro definitions */ + +usertype Params, String; + +const pk,hash: Function; +secret sk,unhash: Function; +inversekeys(pk,sk); +inversekeys(hash,unhash); + +const clientstring,serverstring: String; + +const Alice, Bob, Eve: Agent; +const Terence: Agent; + +protocol tls-HSDDM05(X,Y) +{ + role X + { + const Nx: Nonce; + const msecret: Nonce; + const pa: Params; + var Ny: Nonce; + var pb: Params; + + send_1( X,Y, X,Nx,pa ); + read_2( Y,X, Ny,pb,{ Y,pk(Y) }sk(Terence) ); + send_3( X,Y, { X,pk(X) }sk(Terence),{msecret}pk(Y),{hash(X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),{msecret}pk(Y))}sk(X),hash(msecret,hash(X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),{msecret}pk(Y)),clientstring) ); + read_4( Y,X, hash(msecret,hash(X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),{ X,pk(X) }sk(Terence),{msecret}pk(Y),{hash(X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),{msecret}pk(Y))}sk(X),hash(msecret,hash(X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),{msecret}pk(Y)),clientstring)),serverstring) ); + + claim_X1( X, Secret, msecret ); + } + + role Y + { + var Nx: Nonce; + var msecret: Nonce; + var pa: Params; + const Ny: Nonce; + const pb: Params; + + read_1( X,Y, X,Nx,pa ); + send_2( Y,X, Ny,pb,{ Y,pk(Y) }sk(Terence) ); + read_3( X,Y, { X,pk(X) }sk(Terence),{msecret}pk(Y),{hash(X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),{msecret}pk(Y))}sk(X),hash(msecret,hash(X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),{msecret}pk(Y)),clientstring) ); + send_4( Y,X, hash(msecret,hash(X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),{ X,pk(X) }sk(Terence),{msecret}pk(Y),{hash(X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),{msecret}pk(Y))}sk(X),hash(msecret,hash(X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),{msecret}pk(Y)),clientstring)),serverstring) ); + + claim_Y1( Y, Secret, msecret ); + } +} + + +untrusted Eve; +compromised sk(Eve); +