/* 
 * Coursework 2 PI protocol
*/
usertype String;
usertype Timestamp;
usertype Sessionkey;

hashfunction H1;

protocol protocolPI(Network, Application, Phone) {

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

		var SesK: SessionKey;
		var tl: Timestamp;

		var mApp: String;

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

		fresh mPhone: String;

		claim_phone1(Phone, Running, Application, mApp, SesK);

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

		claim_phone2(Phone, Secret, SesK);
		claim_application1(Phone, Commit, Application, mApp, SesK);
		//claim_network2(Phone, Commit, Network, SesK, tl);
		claim_phone3(Phone, Nisynch);

	}

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

		fresh nApp: Nonce;

		send_refreshKeys(Application,Network, Application, Phone, nApp);

		var SesK: SessionKey;
		var tl: Timestamp;

		var T1: Ticket;

		recv_keysApp(Network,Application, {H1(SesK, tl, nApp, Phone, T1)}k(Network, Application), {SesK, tl, nApp, Phone, T1}k(Network, Application));

		fresh mApp: String;
		var mPhone: String;

		claim_application1(Application, Running, Phone, mApp, SesK);

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

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

		claim_application2(Application, Secret, SesK);
		claim_phone1(Application, Commit, Phone, mApp, SesK);
		claim_network1(Application, Commit, Network, SesK, tl);

		claim_application3(Application, Nisynch);
	}

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

		var nApp: Nonce;

		recv_refreshKeys(Application,Network, Application, Phone, nApp);

		fresh SesK: SessionKey;
		fresh tl: Timestamp;

		claim_netwrok1(Network, Running, Application, SesK, tl);

		send_keysApp(Network,Application, { H1(SesK, tl, nApp, Phone, ({H1(SesK, tl, Application)}k(Network, Phone), {SesK, tl, Application}k(Network, Phone))) }k(Network, Application) , {SesK, tl, nApp, Phone, ({H1(SesK, tl, Application)}k(Network, Phone), {SesK, tl, Application}k(Network, Phone))}k(Network, Application));

		claim_network3(Network, Secret, SesK);
	}
}