scyther/testing/tls/tls-BM-1.spdl

/*
 * This is a model of a version of the TLS protocol as modeled in
 * Boyd, Mathuria "Protocols for Authentication and key establishment"
 *
 * It's a very simplified form.
 */












/* below is just Scyther input and no further macro definitions */

const pk,hash: Function;
secret sk,unhash: Function;
inversekeys(pk,sk);
inversekeys(hash,unhash);

const Alice, Bob, Eve: Agent;
const Terence: Agent;

protocol tls-bm-1(A,B)
{
	role A
	{
		fresh na: Nonce;
		fresh pmk: Nonce;
		var nb: Nonce;

		send_1( A,B, na );
		recv_2( B,A, nb );
		send_3( A,B, { pmk }pk(B),{ hash(na,nb,{ pmk }pk(B)) }sk(A),{ hash(na,nb,{ pmk }pk(B),{ hash(na,nb,{ pmk }pk(B)) }sk(A)) }hash(pmk,na,nb) );
		recv_4( B,A, { na,nb,{ pmk }pk(B),{ hash(na,nb,{ pmk }pk(B)) }sk(A),{ hash(na,nb,{ pmk }pk(B),{ hash(na,nb,{ pmk }pk(B)) }sk(A)) }hash(pmk,na,nb) }hash(pmk,na,nb) );

		claim_A1( A, Secret, hash(pmk,na,nb) );
		claim_A2( A, Nisynch );
	}	
	
	role B
	{
		var na: Nonce;
		var pmk: Nonce;
		fresh nb: Nonce;

		recv_1( A,B, na );
		send_2( B,A, nb );
		recv_3( A,B, { pmk }pk(B),{ hash(na,nb,{ pmk }pk(B)) }sk(A),{ hash(na,nb,{ pmk }pk(B),{ hash(na,nb,{ pmk }pk(B)) }sk(A)) }hash(pmk,na,nb) );
		send_4( B,A, { na,nb,{ pmk }pk(B),{ hash(na,nb,{ pmk }pk(B)) }sk(A),{ hash(na,nb,{ pmk }pk(B),{ hash(na,nb,{ pmk }pk(B)) }sk(A)) }hash(pmk,na,nb) }hash(pmk,na,nb) );

		claim_B1( B, Secret, hash(pmk,na,nb) );
		claim_B2( B, Nisynch );
	}
}