scyther/protocols/misc/tls/tls-HSDDM05-fix.spdl

/*
 * 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
	{
		fresh Nx: Nonce;
		fresh msecret: Nonce;
		fresh pa: Params;
		var Ny: Nonce;
		var pb: Params;

		send_1( X,Y, X,Nx,pa );
		recv_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) );
		recv_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;
		fresh Ny: Nonce;
		fresh pb: Params;

		recv_1( X,Y, X,Nx,pa );
		send_2( Y,X, Ny,pb,{ Y,pk(Y) }sk(Terence) );
		recv_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 );
	}
}