/*
 * f5.spdl
 *
 * Tailored protocol to show that any number of runs can be required to
 * find an attack.
 *
 * For this version, -m2 and -r5 are needed.
 *
 * April 2005, Cas Cremers
 */

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

protocol f4(I,R)
{
	role I
	{
		var nr: Nonce;

		read_1(R,I, nr );
		send_2(I,R, { nr }sk(I) );
		read_3(R,I, {{{{{ nr }sk(R)}sk(R)}sk(R)}sk(R)}sk(R) );

		claim_i1(I,Niagree);
	}	

	role R
	{
		const nr: Nonce;
		send_1(R,I, nr );
	}
	
}

const Alice,Bob,Eve: Agent;

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

run f4.I(Agent,Agent);
run f4.I(Agent,Agent);
run f4.I(Agent,Agent);
run f4.I(Agent,Agent);
run f4.I(Agent,Agent);
run f4.I(Agent,Agent);