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


protocol protocol1(A,B)
{
	role A
	{
		const Na: Nonce;
		var Nb: Nonce;
		fresh Ta: Timestamp;
		var Tb: Timestamp;
		fresh Xa, Ya: Nonce;
		var Yb, Xb: Nonce;

		send_1(A, B,  A,{Ta, Na, B, Xa, {Ya}pk(B)}sk(A));


		claim_a1(A, Secret, Ya);
		//claim_a2(A, Secret, Xa);
		claim_a4(A, Nisynch);
		claim_a5(A, Niagree);
	}

	role B
	{
		const Nb: Nonce;
		var Na: Nonce;
		fresh Ta: Timestamp;
		var Tb: Timestamp;
		fresh Xb, Yb: Nonce;
		var Ya, Xa: Nonce;

		recv_1(A,B , A,{Ta, Na, B, Xa, {Ya}pk(B)}sk(A));

		claim_b1(B, Secret, Ya);
		//claim_b2(B, Secret, Xa);
		claim_b4(B, Nisynch);
		claim_b5(B, Niagree);
	}
}

// An untrusted agent, with leaked information

const Eve: Agent;
untrusted Eve;
compromised sk(Eve);