scyther/spdl/tmn.spdl

usertype Key;

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

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

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

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

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

		claim_6(B,Secret,Kb);
	}

	role S
	{
		var Ka,Kb: Key;

		read_1(A,S, B,{Ka}pk(S) );
		send_2(S,B, A );
		read_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;

untrusted Eve;
compromised sk(Eve);

run tmn.A (Agent,Agent,Simon);
run tmn.A (Agent,Agent,Simon);
run tmn.B (Agent,Agent,Simon);
run tmn.B (Agent,Agent,Simon);
run tmn.S (Agent,Agent,Simon);
run tmn.S (Agent,Agent,Simon);