// BAN modified version of the yahalom protocol
// Type flaw

usertype Server;

const a,b,c : Agent;
const s : Server;
secret k : Function;

protocol yahalomBan(A,B,S)
{
	role B
	{
		const nb;
		var na;
		var kab;

		read_1(A,B, A,na,B,S);
		send_2(B,S, B,nb, {A,na}k(B,S) );
		read_4(A,B, {A,kab,nb}k(B,S) , {nb}kab );
		claim_6(B, Secret,kab);
	}
}