76 lines
2.2 KiB
Plaintext
76 lines
2.2 KiB
Plaintext
/*
|
|
* 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);
|
|
|