2r890-ex3-a.spdl

/*
 * Course 2r890
 *
 * Assignment 0405-3
 *
 * Protocol a
 *
 * nisynch, niagree
 */
const pk: Function;
secret sk: Function;
inversekeys (pk,sk);

protocol course2r890year0405ex3(X,Y,I)
{
	role I
	{
		fresh nx: Nonce;
		fresh ny: Nonce;

		send_1(I,X, nx );
		recv_2(X,I, { I,nx }sk(X) );
		send_3(I,Y, ny );
		recv_4(Y,I, { ny,I }sk(Y) );

		claim_i1(I,Niagree);
		claim_i2(I,Nisynch);
	}	
	
	role X
	{
		var nx: Nonce;

		recv_1(I,X, nx );
		send_2(X,I, { I,nx }sk(X) );
	}

	role Y
	{
		var ny: Nonce;

		recv_3(I,Y, ny );
		send_4(Y,I, { ny,I }sk(Y) );
	}
}