/*usertype Timestamp;

protocol LaTe(C, S)
{
	role C {
		fresh nc: Nonce;

		var ts: Timestamp;

		send_1(C,S, C, nc);

		recv_2(S,C, nc, ts, {nc, ts}k(S, C));

		claim_C1(C,Nisynch);
		claim_C2(C,Niagree);
		claim_C3(C,Alive);
		claim_C4(C,Weakagree);
		claim_C5(C, Commit, S, nc, ts);
	}

	role S {
		var nc: Nonce;

		fresh ts: Timestamp;

		//send_!timestampSet(S,S, ts);

		recv_1(C,S, C, nc);

		claim_C5(S, Running, C, nc, ts);

		send_2(S,C, nc, ts, {nc, ts}k(S, C));

		claim_S1(S,Nisynch);
		claim_S2(S,Niagree);
		claim_S3(S,Alive);
		claim_S4(S,Weakagree);
	}
}*/

usertype TimeStamp;
hashfunction H1;


protocol LATe(I,R)
{
	role I # Time Client - Initiator
	{
		fresh Na : Nonce;
		var T : TimeStamp;
		send_1(I,R,I,Na);
		recv_2(R,I,Na,T,H1({Na,T}k(I,R)));#encrypt-then-hash
		claim_I1(I,Nisynch); #encrypt-then-hash
		claim_I2(I,Niagree);
		claim_I3(I,Alive);
		claim_I4(I,Weakagree);
		claim_I5(I, Commit, R, Na, T);
	}

	role R # Time Server - Responder
	{
		var Na : Nonce;
		fresh T : TimeStamp;
		recv_1(I,R,I,Na);
		claim_C5(R, Running, I, Na, T);
		send_2(R,I,Na,T,H1({Na,T}k(I,R)));#encrypt-then-hash
	}
}