scyther/testing/samasc-broken.spdl

/* 
	Samasc broken
*/

usertype Key;

const pk: Function;
secret sk: Function;

inversekeys (pk,sk);

protocol samascbroken(I,R)
{
	role R
	{
		fresh nr: Nonce;
		var kir: Key;

		recv_!1a (I,R, { kir,I }pk(R) );
		send_!1b (R,I, {nr,R}pk(I) );

		/* Commenting out these two lines yields an attack: */
		recv_!2a (I,R, { nr }kir );
		send_!2b (R,I, { I,R,nr }kir );

		recv_!3 (I,R, { I,R }kir );

		claim_4 (R, Secret, kir );
	}
}


untrusted e;
compromised sk(e);