/* 
 * Coursework 2 PI protocol
*/

usertype Timestamp;
usertype Sessionkey;

hashfunction Mac;

protocol protocolPI(Network, Application, Phone) {

	/* Role R - Phone
	 *
	 * has keys k(N,R)
	 *
	 */
	role Phone {

		var SesK: SessionKey;
		var tl: Timestamp;

		recv_keysPhone(Network, Phone, Mac({SesK, tl}k(Network, Phone)), {SesK, tl}k(Network, Phone));

		var mApp: Nonce;

		recv_1(Application,Phone, {mApp}k(SesK));

		fresh mPhone: Nonce;

		send_2(Phone,Application, {mApp, mPhone}k(SesK));
	}

	/* Role S - Application
	 *
	 * has keys k(N,S)
	 *
	 */
	role Application {

		send_refreshKeys(Application,Network, Application, Phone);

		var SesK: SessionKey;
		var tl: Timestamp;

		recv_keysApp(Network,Application, Mac({SesK, tl}k(Network, Application)), {SesK, tl}k(Network, Application));

		fresh mApp: Nonce;
		var mPhone: Nonce;

		send_1(Application,Phone, {mApp}k(SesK));

		recv_2(Phone,Application, {mApp, mPhone}k(SesK));
	}

	/* Role N - Network
	 *
	 * has keys k(N,R) and k(N,S)
	 *
	 */
	role Network {

		recv_refreshKeys(Application,Network, Application, Phone);

		fresh SesK: SessionKey;
		fresh tl: Timestamp;

		send_keysApp(Network,Application, Mac({SesK, tl}k(Network, Application)), {SesK, tl}k(Network, Application));

		send_keysPhone(Network,Phone, Mac({SesK, tl}k(Network, Phone)), {SesK, tl}k(Network, Phone));
	}

	
}