scyther/testing/broken1.spdl

/*
 * A broken protocol
 *
 * Cas Cremers
 * Visualization challenge of the week.
 * Can be checked withouth CL, please do so.
 */

usertype String, Key;
const PlainSight: String;
secret HelloWorld, HelloServer: String;
secret k: Key;

protocol broken1(I,R,S)
{
	role I
	{
		send_1(I, R, PlainSight, {HelloWorld, I, R}k );
		send_2(I, S, {HelloServer, I, S}k );
	}	
	role R
	{
		recv_3(S, R, {HelloWorld, S, I, R}k );
		recv_1(I, R, PlainSight, {HelloWorld, I, R}k );
		claim_4(R, Secret, PlainSight);
	}
	role S
	{
		recv_2(I, S, {HelloServer, I, S}k );
		send_3(S, R, {HelloWorld, S, I, R}k );
	}
}

const a, b, S: Agent;

run broken1.I(a, b, S);
run broken1.R(a, b, S);
run broken1.S(a, b, S);