learnKey.  State  = 1 	/\ Rcv({SERVER.PK_SERVER'}_inv(PKs))
	=|> State':= 2
			/\ KeyRing':=cons(SERVER.PK_SERVER', KeyRing)
			/\ Nonce_RETRAIT':=new()
			/\ Snd({Nonce_RETRAIT'.RETRAIT}_PK_SERVER')
			/\ secret(Nonce_RETRAIT', sna, {RETRAIT,SERVER})
			/\ witness(RETRAIT, SERVER, bob_alice_na, Nonce_RETRAIT')