/* 
 * Some authentication protocol
 * 
 * Version by Johan Selst. Seems to segfault at a simple -r4 execution
 * with the modelchecker.
 *
 * Reported on 2005-05-11.
 */

// PKI infrastructure

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

// The protocol description

protocol as3a(X, I, Y)
{
	role X
	{
		var nix: Nonce;

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

	role I
	{
		const nix, niy: Nonce;

		send_1(I, X, nix);
		read_2(X, I, {I,nix}sk(X));
		send_3(I, Y, niy);
		read_4(Y, I, {niy,I}sk(Y));
		claim_i1(I, Nisynch);
	}	

	role Y
	{
		var niy: Nonce;

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

// The trusted agents in the system

const Alice,Bob,Carol: Agent;

// An untrusted agent, with leaked information

const Eve: Agent;
untrusted Eve;
compromised sk(Eve);

// The runs (only needed for the modelchecker algorithm)

run as3a.X(Agent,Agent,Agent);
run as3a.I(Agent,Agent,Agent);
run as3a.Y(Agent,Agent,Agent);

run as3a.X(Agent,Agent,Agent);
run as3a.I(Agent,Agent,Agent);
run as3a.Y(Agent,Agent,Agent);

run as3a.X(Agent,Agent,Agent);
run as3a.I(Agent,Agent,Agent);
run as3a.Y(Agent,Agent,Agent);

run as3a.X(Agent,Agent,Agent);
run as3a.I(Agent,Agent,Agent);
run as3a.Y(Agent,Agent,Agent);

run as3a.X(Agent,Agent,Agent);
run as3a.I(Agent,Agent,Agent);
run as3a.Y(Agent,Agent,Agent);

run as3a.X(Agent,Agent,Agent);
run as3a.I(Agent,Agent,Agent);
run as3a.Y(Agent,Agent,Agent);