Appendix
The source code for initial phase is as follow:
 
var TM, HUB, ASF: Agent;
hashfunction g,h,cm;

macro Kta = k(TM,ASF);
macro Kha = k(HUB,ASF);
macro PMK = cm(Kta,ts);
macro MK = cm(PMK,n1,n2);

protocol @oracle(DH) {

	role DH{
		var x, y: Nonce;

		recv_!DH1( DH, DH, h(g(y),x) );
		send_!DH2( DH, DH, h(g(x),y) );
	}
}

protocol @executability(O) {

	role O {
		var n1, n2, ts, x, y: Nonce;

		recv_!O1( O, O, n2, g(x), cm(MK, TM, HUB, n2, g(x)), cm(MK,n1,n2,h(g(y),x),TM,HUB,n2,g(x),cm(MK,TM,HUB,n2,g(x))));
		send_!O2( O, O, n2, g(x), cm(MK, TM, HUB, n2, g(x)), cm(MK,n1,n2,h(g(x),y),TM,HUB,n2,g(x),cm(MK,TM,HUB,n2,g(x))));
		recv_!O3( O, O, cm(cm(MK, n1, n2, h(g(x), y)), HUB, TM));
		send_!O4( O, O, cm(cm(MK, n1, n2, h(g(y), x)), HUB, TM));
	}
}

protocol p2mp(TM, HUB, ASF) {

	role TM{
		fresh x, ts, n1: Nonce;
		var n2: Nonce;
		var Gy: Ticket;

		send_1(TM, HUB, TM, HUB, ts, n1, cm(Kta, TM, HUB, ts, n1));		
		recv_4(HUB, TM, HUB, TM, n1, n2, Gy, cm(MK, HUB, TM, n1, n2, Gy));

		claim(TM, Running, HUB, cm(MK,n1,n2,h(Gy,x)));

		send_!5(TM, HUB, TM, HUB, n2, g(x), cm(cm(MK,n1,n2,h(Gy,x)), TM, HUB, n2, g(x)), cm(MK,TM,HUB,n2,g(x),cm(cm(MK,n1,n2,h(Gy,x)),TM,HUB,n2,g(x))));
		recv_!6(HUB, TM, HUB, TM, cm(cm(cm(PMK, n1, n2), n1, n2, h(Gy, x)), HUB, TM));

		claim(TM, Alive);
		claim(TM, Nisynch);
		claim(TM, Niagree);
		claim(TM, Weakagree);
		claim(TM, Commit, HUB, cm(MK,n1,n2,h(Gy,x)));
		claim(TM, Secret, Kta);
		claim(TM, Secret, PMK);
		claim(TM, Secret, MK);
		claim(TM, SKR, cm(MK, n1, n2, h(Gy,x)));
	}

	role HUB{
		fresh y, n2 : Nonce;
		var ts, n1: Nonce;
		var Gx: Ticket;

		recv_1(TM, HUB, TM, HUB, ts, n1, cm(Kta, TM, HUB, ts, n1));
		send_2(HUB, ASF, TM, HUB, ts, n1, cm(Kta, TM, HUB, ts, n1));
		recv_3(ASF, HUB, {PMK}Kha);
		send_4(HUB, TM, HUB, TM, n1, n2, g(y), cm(MK, HUB, TM, n1, n2, g(y)));
		recv_!5(TM, HUB, TM, HUB, n2, Gx, cm(cm(MK,n1,n2,h(Gx,y)), TM, HUB, n2, Gx), cm(MK,TM,HUB,n2,Gx,cm(cm(MK,n1,n2,h(Gx,y)),TM,HUB,n2,Gx)));

		claim(HUB, Running, TM, cm(MK,n1,n2,h(Gx,y)));

		send_!6(HUB, TM, HUB, TM, cm(cm(MK, n1, n2, h(Gx, y)), HUB, TM));

		claim(HUB, Alive);
		claim(HUB, Nisynch);
		claim(HUB, Niagree);
		claim(HUB, Weakagree);
		claim(HUB, Commit, TM, cm(MK,n1,n2,h(Gx,y)));
		claim(HUB, Secret, PMK);
		claim(HUB, Secret, cm(PMK, n1, n2));
		claim(HUB, SKR, cm(MK, n1, n2, h(Gx,y)));
	}

	role ASF{
		var ts, n1: Nonce;

		recv_2(HUB, ASF, TM, HUB, ts, n1, cm(Kta, TM, HUB, ts, n1));
		send_3(ASF, HUB, {PMK}Kha);

		claim(ASF, Secret, Kta);
		claim(ASF, Secret, PMK);
	}
}

The source code for key update phase is as follow:

var TM, HUB: Agent;
hashfunction g,h,cm;

macro MK = cm(MKold,n1,n2);

protocol @oracle(DH) {

	role DH{
		var x, y: Nonce;

		recv_!DH1(DH,DH,h(g(y),x));
		send_!DH2(DH,DH,h(g(x),y));
		}
}

protocol @executability(O){

	role O{
		var n1, n2, ts, x, y, MKold: Nonce;

		recv_!O1(O,O,n1,n2,g(y),cm(cm(MK,n1,n2,h(g(x),y)),HUB,TM,n1,n2,g(y)),cm(MK,HUB,TM,n1,n2,g(y)));
		send_!O2(O,O,n1,n2,g(y),cm(cm(MK,n1,n2,h(g(y),x)),HUB,TM,n1,n2,g(y)),cm(MK,HUB,TM,n1,n2,g(y)));
		recv_!O3(O,O,n2,cm(cm(MK,n1,n2,h(g(y),x)),TM,HUB,n2));
		send_!O4(O,O,n2,cm(cm(MK,n1,n2,h(g(x),y)),TM,HUB,n2));
	}
}

protocol p2mpkeyupdate(TM,HUB) {

	role TM{
		fresh x, ts, n1: Nonce;

		var n2: Nonce;
		var Gy: Ticket;
		secret MKold, AKold;

		send_1(TM,HUB,ts,n1,g(x),cm(AKold,TM,HUB,ts,n1,g(x)));
		recv_!2(HUB,TM,n1,n2,Gy,cm(cm(MK,n1,n2,h(Gy,x)),HUB,TM,n1,n2,Gy),cm(MK,HUB,TM,n1,n2,Gy));

		claim(TM,Running,HUB, cm(MK,n1,n2,h(Gy,x)));

		send_!3(TM,HUB,n2,cm(cm(MK,n1,n2,h(Gy,x)),TM,HUB,n2));

		claim(TM, Alive);
		claim(TM, Nisynch);
		claim(TM, Niagree);
		claim(TM, Weakagree);
		claim(TM, Commit, HUB, cm(MK,n1,n2,h(Gy,x)));
		claim(TM, Secret, MKold);
		claim(TM, Secret, AKold);
		claim(TM, SKR, MK);
		claim(TM, SKR, cm(MK,n1,n2,h(Gy,x)));
	}

	role HUB{
		fresh y, n2: Nonce;
		var ts, n1: Nonce;
		var Gx: Ticket;
		secret MKold, AKold;

		recv_1(TM,HUB,ts,n1,Gx,cm(AKold,TM,HUB,ts,n1,Gx));

		claim(HUB, Running, TM, cm(MK,n1,n2,h(Gx,y)));

		send_!2(HUB,TM,n1,n2,g(y),cm(cm(MK,n1,n2,h(Gx,y)),HUB,TM,n1,n2,g(y)),cm(MK,HUB,TM,n1,n2,g(y)));
		recv_!3(TM,HUB,n2,cm(cm(MK,n1,n2,h(Gx,y)),TM,HUB,n2));

		claim(HUB, Alive);
		claim(HUB, Nisynch);
		claim(HUB, Niagree);
		claim(HUB, Weakagree);
		claim(HUB, Commit, TM, cm(MK,n1,n2,h(Gx,y)));
		claim(HUB, Secret, MKold);
		claim(HUB, Secret, AKold);
		claim(HUB, SKR, MK);
		claim(HUB, SKR, cm(MK,n1,n2,h(Gx,y)));
	}
}

The source code for policy update phase is as follow:

var TM, HUB, ASF: Agent;
hashfunction g,h,cm;

macro MK = cm(MKold,n1,n2);

protocol @oracle(DH) {

	role DH{
		var x, y: Nonce;

		recv_!DH1( DH, DH, h(g(y),x) );
		send_!DH2( DH, DH, h(g(x),y) );
	}
}

protocol @executability(O) {

	role O {
		var n1, n2, ts, x, y, MKold: Nonce;

		recv_!O1( O, O, n1,n2,g(x),cm(cm(MK,n1,n2,h(g(y),x)),TM,HUB,n1,n2,g(x)),cm(MK,TM,HUB,n1,n2,g(x),cm(cm(MK,n1,n2,h(g(y),x)),TM,HUB,n1,n2,g(x))));
		send_!O2( O, O, n1,n2,g(x),cm(cm(MK,n1,n2,h(g(x),y)),TM,HUB,n1,n2,g(x)),cm(MK,TM,HUB,n1,n2,g(x),cm(cm(MK,n1,n2,h(g(x),y)),TM,HUB,n1,n2,g(x))));
		recv_!O3( O, O, n2,cm(cm(MK,n1,n2,h(g(x),y)),HUB,TM,n2));
		send_!O4( O, O, n2,cm(cm(MK,n1,n2,h(g(y),x)),HUB,TM,n2));
	}
}

protocol p2mppolicyupdate(TM,HUB){

	role TM{
		fresh x, n2: Nonce;
		var ts, n1: Nonce;
		var Gy: Ticket;
		secret AKold, MKold, policy;

		recv_1(HUB,TM,ts,n1,policy,Gy,cm(AKold,HUB,TM,ts,n1,policy,Gy));

		claim(TM,Running,HUB, cm(MK,n1,n2,h(Gy,x)));

		send_!2(TM,HUB,n1,n2,g(x),cm(cm(MK,n1,n2,h(Gy,x)),TM,HUB,n1,n2,g(x)),cm(MK,TM,HUB,n1,n2,g(x),cm(cm(MK,n1,n2,h(Gy,x)),TM,HUB,n1,n2,g(x))));
		recv_!3(HUB,TM,n2,cm(cm(MK,n1,n2,h(Gy,x)),HUB,TM,n2));

		claim(TM, Alive);
		claim(TM, Nisynch);
		claim(TM, Niagree);
		claim(TM, Weakagree);
		claim(TM, Commit, HUB, cm(MK,n1,n2,h(Gy,x)));
		claim(TM, Secret, MKold);
		claim(TM, Secret, AKold);
		claim(TM, SKR, MK);
		claim(TM, SKR, cm(MK,n1,n2,h(Gy,x)));
	}

	role HUB{
		fresh ts, y, n1: Nonce;
		var n2: Nonce;
		var Gx: Ticket;
		secret AKold, MKold, policy;

		send_1(HUB,TM,ts,n1,policy,g(y),cm(AKold,HUB,TM,ts,n1,policy,g(y)));
		recv_!2(TM,HUB,n1,n2,Gx,cm(cm(MK,n1,n2,h(Gx,y)),TM,HUB,n1,n2,Gx),cm(MK,TM,HUB,n1,n2,Gx,cm(cm(MK,n1,n2,h(Gx,y)),TM,HUB,n1,n2,Gx)));

		claim(HUB, Running, TM, cm(MK,n1,n2,h(Gx,y)));

		send_!3(HUB,TM,n2,cm(cm(MK,n1,n2,h(Gx,y)),HUB,TM,n2));

		claim(HUB, Alive);
		claim(HUB, Nisynch);
		claim(HUB, Niagree);
		claim(HUB, Weakagree);
		claim(HUB, Commit, TM, cm(MK,n1,n2,h(Gx,y)));
		claim(HUB, Secret, MKold);
		claim(HUB, Secret, AKold);
		claim(HUB, SKR, MK);
		claim(HUB, SKR, cm(MK,n1,n2,h(Gx,y)));
	}
}