State  = 0 /\ RCV(start) =|>
	State':= 1 /\ Na' := new() /\ SND({Na'.A}_Kb)
  /\ secret(Na', sna, {A,B})
  /\ witness(A,B,bob_alice_na,Na')

Et le serveur reçoit:

 0.  State = 0 /\ RCV({Na'.A}_Kb) =|>
  State':= 1 /\ Nb' := new() /\ secret(Nb', snb, {A,B}) /\ SND({Na'.Nb'.B}_Ka)