A definition of secure multi-party key exchange in the Canetti-Krawczyk proof model is proposed, followed by a proof of the security of the Joux tripartite key agreement protocol according to that definition. The Joux protocol is then combined with two authentication mechanisms to produce a variety of provably secure key agreement protocols. The properties and efficiency of the Joux based protocols thus derived are then compared with each other and other published tripartite key agreement protocols. It is concluded that the Joux protocol can be used to generate efficient yet provably secure protocols.