scyther/testing/2r890-ex3-b.spdl

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

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

		send_1(I,X, ni );
		recv_2(X,I, { I,ni }sk(X) );
		send_3(I,Y, ni );
		recv_4(Y,I, { ni,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) );
	}
}