scyther/testing/tmn.spdl

usertype Key;

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

protocol tmn(A,B,S)
{
	role A
	{
		fresh Ka: Key;
		var Kb: Key;

		send_1(A,S, B,{Ka}pk(S) );
		recv_4(S,A, B,{Kb}Ka );

		claim_5(A,Secret,Ka);
		claim_8(A,Secret,Kb);
	}	
	
	role B
	{
		fresh Kb: Key;

		recv_2(S,B, A );
		send_3(B,S, A, { Kb }pk(S) );

		claim_6(B,Secret,Kb);
	}

	role S
	{
		var Ka,Kb: Key;

		recv_1(A,S, B,{Ka}pk(S) );
		send_2(S,B, A );
		recv_3(B,S, A, { Kb }pk(S) );
		send_4(S,A, B,{Kb}Ka );

		claim_7(S,Secret,Ka);
	}
}

const Alice,Bob,Eve,Simon: Agent;