From 15822a303f53ba6c682cbee3f6db6b0785933a1c Mon Sep 17 00:00:00 2001 From: ccremers Date: Wed, 29 Nov 2006 23:25:40 +0000 Subject: [PATCH] - New version of the protocol after communication with Anupam Datta. --- spdl/misc/tls-HSDDM05-2.cpp | 84 ++++++++++++++++++++++++++++++++++++ spdl/misc/tls-HSDDM05-2.spdl | 55 +++++++++++++++++++++++ 2 files changed, 139 insertions(+) create mode 100644 spdl/misc/tls-HSDDM05-2.cpp create mode 100644 spdl/misc/tls-HSDDM05-2.spdl diff --git a/spdl/misc/tls-HSDDM05-2.cpp b/spdl/misc/tls-HSDDM05-2.cpp new file mode 100644 index 0000000..9d21a41 --- /dev/null +++ b/spdl/misc/tls-HSDDM05-2.cpp @@ -0,0 +1,84 @@ +/* + * This is an improved 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". + * + * Modeled by: Cas Cremers + * + * The original model was broken: the secret was not part of the + * handshake, and the handshakes were not hashed. After an e-mail + * exchange with Anupam Datta this was cleared up. + * + * The .cpp file cannot be fed into scyther directly; rather, one needs + * to type: (for *nix type systems with cpp) + * + * cpp tls-HSDDM05-2.cpp >tls-HSDDM05-2.spdl + * + * in order to generate a valid spdl file for the Scyther. + * + * This allows for macro expansion, as seen in the next part, which is + * particularly useful for expanding the handshakes. + * + */ +#define CERT(a) { a,pk(a) }sk(Terence) +#define msg1 X,Nx,pa +#define msg2 Ny,pb,CERT(Y) +#define handShake1 hash(msg1,msg2,msecret) +#define msg3 CERT(X),{handShake1}sk(X),{msecret}pk(Y),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-HSDDM05-2.spdl b/spdl/misc/tls-HSDDM05-2.spdl new file mode 100644 index 0000000..c1ab0e9 --- /dev/null +++ b/spdl/misc/tls-HSDDM05-2.spdl @@ -0,0 +1,55 @@ +# 1 "tls-HSDDM05-2.cpp" +# 1 "" +# 1 "" +# 1 "tls-HSDDM05-2.cpp" +# 34 "tls-HSDDM05-2.cpp" +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),{hash(X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),msecret)}sk(X),{msecret}pk(Y),hash(msecret,hash(X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),msecret),clientstring) ); + read_4( Y,X, hash(msecret,hash(X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),{ X,pk(X) }sk(Terence),{hash(X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),msecret)}sk(X),{msecret}pk(Y),hash(msecret,hash(X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),msecret),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),{hash(X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),msecret)}sk(X),{msecret}pk(Y),hash(msecret,hash(X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),msecret),clientstring) ); + send_4( Y,X, hash(msecret,hash(X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),{ X,pk(X) }sk(Terence),{hash(X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),msecret)}sk(X),{msecret}pk(Y),hash(msecret,hash(X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),msecret),clientstring)),serverstring) ); + + claim_Y1( Y, Secret, msecret ); + } +} + + +untrusted Eve; +compromised sk(Eve);