/* 
A knows the public key of B
B knows the public key of A

1: A -> B: {NA, A}_B
2: B -> A: {NA, NB}_A
3: A -> B: {NB}_B

at the end,
A and B share a common secret
A has authenticated B
B has authenticated A
*/

mtype = {step1, step2, step3, A, NA, KA, B, NB, KB, M, NM, KM};

typedef Msg {
	mtype m1;
	mtype m2;
	mtype key
}

/* network = set of  "destination + message" */
chan network = [0] of {mtype, Msg};

mtype A_partner, B_partner;

proctype A_proc () {
	mtype partner_key, partner_nonce;
	Msg data;

	/* A can mistake and sends the message to M */
	if
	:: A_partner = B; partner_key = KB
	:: A_partner = M; partner_key = KM
	fi;

	atomic { data.m1 = NA; data.m2 = A; data.key = partner_key };

	network ! A_partner, data;

	network ? A, data;

	(data.m1 == NA) && (data.key == KA);

	partner_nonce = data.m2;

	atomic { data.m1 = partner_nonce; data.m2 = 0; data.key = partner_key };

	network ! A_partner, data
}

proctype B_proc () {
	mtype partner_key, partner_nonce;
	Msg data;

	network ? B,  data;
	
	(data.key == KB);
	B_partner = data.m2;

	atomic {
		partner_nonce = data.m1;
		
		if
		:: (B_partner == A) -> partner_key =KA
		:: (B_partner == M) -> partner_key = KM
		fi;

		data.m1 = partner_nonce;
		data.m2 = NB;
		data.key = partner_key;
	}

	network ! B_partner, data;

	network ? B, data;

	(data.key == KB) && (data.m1 == NB)
}

bool M_knows_NA = false;
bool M_knows_NB = false;

proctype M_proc () {
	Msg data, tmp;
	
	do
	:: if
		:: network ! B, tmp
		:: data.key = KB;
			if
			:: data.m1 = NM
			:: M_knows_NA == true -> data.m1 = NA
			:: M_knows_NB == true -> data.m1 = NB
			fi;
			if
			:: data.m2 = M
			:: data.m2 = A
			:: data.m2 = B
			fi;
			network ! B, data
	   fi
	:: if
		:: network ! A, tmp
		:: data.key = KA;
			if
			:: data.m1 = NM
			:: M_knows_NA == true -> data.m1 = NA
			:: M_knows_NB == true -> data.m1 = NB
			fi;
			if
			:: data.m2 = NM
			:: M_knows_NA == true -> data.m2 = NA
			:: M_knows_NB == true -> data.m2 = NB
			fi;
			network ! A, data
	   fi
	:: if
		:: network ! B, tmp
		:: data.key = KB; data.m2 = 0;
			if
			:: data.m1 = M
			:: M_knows_NA == true -> data.m1 = NA
			:: M_knows_NB == true -> data.m1 = NB	
			fi;
			network ! B, data
	   fi
	:: network ? _, data ->
		atomic { tmp.m1 = data.m1; tmp.m2 = data.m2; tmp.key = data.key };
		atomic {
		if
		:: (data.key == KM) ->
			if
			:: (data.m1 == NA || data.m2 == NA) -> M_knows_NA = true
			:: else -> skip
			fi;
			if
			:: (data.m1 == NB || data.m2 == NB) -> M_knows_NB =true
			:: else -> skip
			fi;
		:: else -> skip
		fi
		}
	od
}

init {
	run A_proc ();
	run B_proc ();
	run M_proc ();
}