/* 
 * BoydCliffNietoPaterson 2008
 *
 */

hashfunction Expd,Ext;
hashfunction xor;


protocol @xorhelper(H1,H2,H3)
{
	role H1
	{
		var X,Y: Ticket;

		recv_!1(H1,H1, xor(X,Y) );
		send_!2(H1,H1, xor(Y,X) );
	}
	role H2
	{
		var X,Y,Z: Ticket;

		recv_!3(H2,H2, xor(X,xor(Y,Z)) );
		send_!4(H2,H2, xor(xor(X,Y),Z) );
	}
	role H3
	{
		var X,Y: Ticket;

		recv_!5(H3,H3, X,xor(X,Y) );
		send_!6(H3,H3, Y );
	}
}

// The protocol description

protocol BCNP-1(I,R)
{
	role I
	{
		fresh Kap: Nonce;
		var Kbp: Nonce;

		send_Compromise(I,I, Kap);

		send_1(I,R, I, { Kap }pk(R) );
		recv_2(R,I, R, { Kbp }pk(I) );

		claim(I,SKR, xor( Expd( Ext(Kap), I, {Kap}pk(R), R, {Kbp}pk(I)),
		                  Expd( Ext(Kbp), I, {Kap}pk(R), R, {Kbp}pk(I))
		                )
		     );
	}	
	
	role R
	{
		var Kap: Nonce;
		fresh Kbp: Nonce;

		send_Compromise(R,R, Kbp);

		recv_1(I,R, I, { Kap }pk(R) );
		send_2(R,I, R, { Kbp }pk(I) );

		claim(R,SKR, xor( Expd( Ext(Kap), I, {Kap}pk(R), R, {Kbp}pk(I)),
		                  Expd( Ext(Kbp), I, {Kap}pk(R), R, {Kbp}pk(I))
		                )
		     );
	}
}