/*
 * Generalized Bilateral Key Exchange protocol.
 * Four-party version.
 *
 * Specific order of interleaving in message 1-4 is required to (a)
 * avoid type flaws whilst (b) retaining BKE structure for the simple
 * case.
 *
 * Cas Cremers
 * Mon May 23 15:15:37 CEST 2005
 */

const zero;
const pk: Function;
secret sk: Function;
inversekeys (pk,sk);

protocol bkegen4(R1,R2,R3,R4)
{
	role R1
	{
		const n1: Nonce;
		var n2,n3,n4: Nonce;

		send_1(R1,R2, {n1,R1,R3,R4}pk(R2) );
		read_4(R4,R1, {n1,n2,n3,n4,R2,R3,R4}pk(R1) );
		send_5(R1,R2, {n2,n3}n4 );

		claim_r1a(R1,Secret,n1);
		claim_r1b(R1,Secret,n2);
		claim_r1c(R1,Secret,n3);
		claim_r1d(R1,Secret,n4);

		claim_r1A(R1,Niagree);
		claim_r1S(R1,Nisynch);
	}	
	
	role R2
	{
		const n2: Nonce;
		var n1,n3,n4: Nonce;

		read_1(R1,R2, {n1,R1,R3,R4}pk(R2) );
		send_2(R2,R3, {n1,R1,n2,R2,R4}pk(R3) );
		read_5(R1,R2, {n2,n3}n4 );
		send_6(R2,R3, {n3}n4 );

		claim_r2a(R2,Secret,n1);
		claim_r2b(R2,Secret,n2);
		claim_r2c(R2,Secret,n3);
		claim_r2d(R2,Secret,n4);

		claim_r2A(R2,Niagree);
		claim_r2S(R2,Nisynch);
	}

	role R3
	{
		const n3: Nonce;
		var n1,n2,n4: Nonce;

		read_2(R2,R3, {n1,R1,n2,R2,R4}pk(R3) );
		send_3(R3,R4, {n1,R1,n2,R2,n3,R3}pk(R4) );
		read_6(R2,R3, {n3}n4 );
		send_7(R3,R4, {zero}n4 );

		claim_r3a(R3,Secret,n1);
		claim_r3b(R3,Secret,n2);
		claim_r3c(R3,Secret,n3);
		claim_r3d(R3,Secret,n4);

		claim_r3A(R3,Niagree);
		claim_r3S(R3,Nisynch);
	}

	role R4
	{
		const n4: Nonce;
		var n1,n2,n3: Nonce;

		read_3(R3,R4, {n1,R1,n2,R2,n3,R3}pk(R4) );
		send_4(R4,R1, {n1,n2,n3,n4,R2,R3,R4}pk(R1) );
		read_7(R3,R4, {zero}n4 );

		claim_r4a(R4,Secret,n1);
		claim_r4b(R4,Secret,n2);
		claim_r4c(R4,Secret,n3);
		claim_r4d(R4,Secret,n4);

		claim_r4A(R4,Niagree);
		claim_r4S(R4,Nisynch);
	}
}

const Alice,Bob,Eve: Agent;

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

run bkegen4.R1(Agent,Agent,Agent,Agent);
run bkegen4.R2(Agent,Agent,Agent,Agent);
run bkegen4.R3(Agent,Agent,Agent,Agent);
run bkegen4.R4(Agent,Agent,Agent,Agent);