scyther/spdl/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
	{
		const ni: Nonce;

		send_1(I,X, ni );
		read_2(X,I, { I,ni }sk(X) );
		send_3(I,Y, ni );
		read_4(Y,I, { ni,I }sk(Y) );

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

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

	role Y
	{
		var ny: Nonce;

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

const Alice,Bob,Eve: Agent;

untrusted Eve;
const ne: Nonce;
compromised sk(Eve);