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

- Added fixed version and checked it.

Browse Source
This commit is contained in:
ccremers 2006-11-30 15:28:01 +00:00
parent fe38647c06
commit f028d797d6
3 changed files with 224 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

74
spdl/misc/tls/tls-HSDDM05-fix.cpp Normal file
View File

@ -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);

75
spdl/misc/tls/tls-HSDDM05-fix.m4 Normal file
View File

@ -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);

75
spdl/misc/tls/tls-HSDDM05-fix.spdl Normal file
View File

@ -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);