/* 
 * HMQV two pass version
 *
 */

// Hash functions
hashfunction h1,h2,gexp,exp,KDF,H;

// Addition, multiplication
// For now, simply hashes
hashfunction mult,add;

/*
 * Hack to simulate public knowledge of public keys.
 */
protocol @publickeys(PK)
{
	role PK
	{
		send_!1(PK,PK, gexp(sk(PK)));
	}
}
		
/*
 * Hack to simulate g^ab = g^ba inside terms.
 * '@' prefix of protocol name denotes helper protocol, which is used by
 * Scyther for displaying, and such protocols are ignored in
 * auto-generation of protocol modifiers.
 */
protocol @exponentiation(RA,RB,RC)
{
	role RA
	{
		var X,Y, T1,T2: Ticket;

		recv_!1(RA,RA, h2(
		  exp(gexp(X),Y),
		  T1, T2, RA,RB
		  ));
		send_!2(RA,RA, h2(
		  exp(gexp(Y),X),
		  T1, T2, RA,RB
		  ));
	}
	role RB
	{
		var X,Y, T1,T2: Ticket;

		recv_!3(RB,RB, h2(
		  T1,
		  exp(gexp(X),Y),
		  T2, RA,RB
		  ));
		send_!4(RB,RB, h2(
		  T1,
		  exp(gexp(Y),X),
		  T2, RA,RB
		  ));
	}
	role RC
	{
		var X,Y, T1,T2: Ticket;

		recv_!5(RC,RC, h2(
		  T1, T2,
		  exp(gexp(X),Y),
		  RA,RB
		  ));
		send_!6(RC,RC, h2(
		  T1, T2,
		  exp(gexp(Y),X),
		  RA,RB
		  ));
	}
}

protocol @addmult(I,R)
{
	role I
	{
		var X,Y: Ticket;

		recv_!1(I,I, add(X,Y) );
		send_!2(I,I, add(Y,X) );
	}
	role R
	{
		var X,Y: Ticket;

		recv_!3(R,R, mult(X,Y) );
		send_!4(R,R, mult(Y,X) );
	}
}

protocol @keyswap(I,R)
{
	role I
	{
		var x,y: Nonce;
		recv_!1(I,I, KDF(exp(mult(gexp(y),exp(gexp(sk(R)),H(gexp(y),I))),add(x,mult(H(gexp(x),R),sk(I))))) );
		send_!2(I,I, KDF(exp(mult(gexp(x),exp(gexp(sk(I)),H(gexp(x),R))),add(y,mult(H(gexp(y),I),sk(R))))) );
	}
}

// The protocol description

symmetric-role protocol HMQV-twopass(I,R)
{
	role I
	{
		fresh x: Nonce;
		var Y: Ticket;

		send_1(I,R, gexp(x) );
		recv_2(R,I, Y );

		claim(I,SKR,    KDF(exp(mult(Y,exp(gexp(sk(R)),H(Y,I))),add(x,mult(H(gexp(x),R),sk(I))))) );
	}	
	
	role R
	{
		fresh y: Nonce;
		var X: Ticket;

		recv_1(I,R, X );
		send_2(R,I, gexp(y) );

		claim(R,SKR,    KDF(exp(mult(X,exp(gexp(sk(I)),H(X,R))),add(y,mult(H(gexp(y),I),sk(R))))) );
	}
}