/* 
	Samasc broken
*/

usertype Key;

const pk: Function;
secret sk: Function;

inversekeys (pk,sk);

protocol bkepk(I,R)
{
	role R
	{
		const nr: Nonce;
		var kir: Key;

		read_1a (I,R, { kir,I }pk(R) );
		send_1b (R,I, {nr,R}pk(I) );

		/* Commenting out these two lines yields an attack: */
		read_2a (I,R, { nr }kir );
		send_2b (R,I, { I,R,nr }kir );

		read_3 (I,R, { I,R }kir );

		claim_4 (R, Secret, kir );
	}
}

const a,b,e: Agent;

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