andr3/scyther
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

- Improved version of tls by the Mitchell group

Browse Source
This commit is contained in:
ccremers 2006-11-24 08:10:52 +00:00
parent 6629b29559
commit 6a6e2a5834
2 changed files with 23 additions and 34 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

37
spdl/misc/tls-HSDDM05.cpp
View File

@ -6,7 +6,7 @@
* The .cpp file cannot be fed into scyther directly; rather, one needs * The .cpp file cannot be fed into scyther directly; rather, one needs
* to type: (for *nix type systems with cpp) * to type: (for *nix type systems with cpp)
* *
* cpp tls-mitchell.cpp >tls-mitchell.spdl * cpp tls-HSDDM05.cpp >tls-HSDDM05.spdl
* *
* in order to generate a valid spdl file for the Scyther. * in order to generate a valid spdl file for the Scyther.
* *
@ -15,8 +15,13 @@
* *
*/ */
#define CERT(a) { a,pk(a) }sk(Terence) #define CERT(a) { a,pk(a) }sk(Terence)
#define handShake1 X,Nx,pa,Ny,pb,CERT(Y) #define msg1 X,Nx,pa
#define handShake2 handShake1,CERT(X),{ handShake1 }sk(X),{ msecret }pk(Y), hash(msecret, handShake1, clientstring) #define msg2 Ny,pb,CERT(Y)
#define handShake1 msg1,msg2
#define msg3 CERT(X),{handShake1}sk(X),{msecret}pk(Y),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 */ /* below is just Scyther input and no further macro definitions */
@ -32,7 +37,7 @@ const clientstring,serverstring: String;
const Alice, Bob, Eve: Agent; const Alice, Bob, Eve: Agent;
const Terence: Agent; const Terence: Agent;
protocol tlsmitchell(X,Y) protocol tls-HSDDM05(X,Y)
{ {
role X role X
{ {
@ -42,14 +47,10 @@ protocol tlsmitchell(X,Y)
var Ny: Nonce; var Ny: Nonce;
var pb: Params; var pb: Params;
send_1( X,Y, X,Nx,pa ); send_1( X,Y, msg1 );
read_2( Y,X, Ny,pb,CERT(Y) ); read_2( Y,X, msg2 );
send_3( X,Y, CERT(X), send_3( X,Y, msg3 );
{ handShake1 }sk(X), read_4( Y,X, msg4 );
{ msecret }pk(Y),
hash(msecret, handShake1, clientstring)
);
read_4( Y,X, hash(msecret, handShake2, serverstring) );
claim_X1( X, Secret, msecret ); claim_X1( X, Secret, msecret );
} }
@ -62,14 +63,10 @@ protocol tlsmitchell(X,Y)
const Ny: Nonce; const Ny: Nonce;
const pb: Params; const pb: Params;
read_1( X,Y, X,Nx,pa ); read_1( X,Y, msg1 );
send_2( Y,X, Ny,pb,CERT(Y) ); send_2( Y,X, msg2 );
read_3( X,Y, CERT(X), read_3( X,Y, msg3 );
{ handShake1 }sk(X), send_4( Y,X, msg4 );
{ msecret }pk(Y),
hash(msecret, handShake1, clientstring)
);
send_4( Y,X, hash(msecret, handShake2, serverstring) );
claim_Y1( Y, Secret, msecret ); claim_Y1( Y, Secret, msecret );
} }

16
spdl/misc/tls-HSDDM05.spdl
View File

@ -2,7 +2,7 @@
# 1 "<built-in>" # 1 "<built-in>"
# 1 "<command line>" # 1 "<command line>"
# 1 "tls-HSDDM05.cpp" # 1 "tls-HSDDM05.cpp"
# 23 "tls-HSDDM05.cpp" # 28 "tls-HSDDM05.cpp"
usertype Params, String; usertype Params, String;
const pk,hash: Function; const pk,hash: Function;
@ -15,7 +15,7 @@ const clientstring,serverstring: String;
const Alice, Bob, Eve: Agent; const Alice, Bob, Eve: Agent;
const Terence: Agent; const Terence: Agent;
protocol tlsmitchell(X,Y) protocol tls-HSDDM05(X,Y)
{ {
role X role X
{ {
@ -27,11 +27,7 @@ protocol tlsmitchell(X,Y)
send_1( X,Y, X,Nx,pa ); send_1( X,Y, X,Nx,pa );
read_2( Y,X, Ny,pb,{ Y,pk(Y) }sk(Terence) ); read_2( Y,X, Ny,pb,{ Y,pk(Y) }sk(Terence) );
send_3( X,Y, { X,pk(X) }sk(Terence), send_3( X,Y, { X,pk(X) }sk(Terence),{X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence)}sk(X),{msecret}pk(Y),hash(msecret,X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),clientstring) );
{ X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence) }sk(X),
{ msecret }pk(Y),
hash(msecret, X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence), clientstring)
);
read_4( Y,X, hash(msecret,X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),{ X,pk(X) }sk(Terence),{X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence)}sk(X),{msecret}pk(Y),hash(msecret,X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),clientstring),serverstring) ); read_4( Y,X, hash(msecret,X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),{ X,pk(X) }sk(Terence),{X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence)}sk(X),{msecret}pk(Y),hash(msecret,X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),clientstring),serverstring) );
claim_X1( X, Secret, msecret ); claim_X1( X, Secret, msecret );
@ -47,11 +43,7 @@ protocol tlsmitchell(X,Y)
read_1( X,Y, X,Nx,pa ); read_1( X,Y, X,Nx,pa );
send_2( Y,X, Ny,pb,{ Y,pk(Y) }sk(Terence) ); send_2( Y,X, Ny,pb,{ Y,pk(Y) }sk(Terence) );
read_3( X,Y, { X,pk(X) }sk(Terence), read_3( X,Y, { X,pk(X) }sk(Terence),{X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence)}sk(X),{msecret}pk(Y),hash(msecret,X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),clientstring) );
{ X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence) }sk(X),
{ msecret }pk(Y),
hash(msecret, X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence), clientstring)
);
send_4( Y,X, hash(msecret,X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),{ X,pk(X) }sk(Terence),{X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence)}sk(X),{msecret}pk(Y),hash(msecret,X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),clientstring),serverstring) ); send_4( Y,X, hash(msecret,X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),{ X,pk(X) }sk(Terence),{X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence)}sk(X),{msecret}pk(Y),hash(msecret,X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),clientstring),serverstring) );
claim_Y1( Y, Secret, msecret ); claim_Y1( Y, Secret, msecret );