This paper presents a formalism for analyzing key-exchange (KE) protocols that combines previous approaches to define a security notion with important analytical benefits. The security definition allows KE protocols to be composed with symmetric encryption and authentication functions to provide provably secure communication channels. It also enables simple modular proofs of security by designing and proving security in an idealized model with perfectly authenticated links, then translating them to realistic settings with adversary-controlled links using general tools. The paper applies this formalism to prove the security of two classes of KE protocols: Diffie-Hellman and key-transport protocols, authenticated via symmetric or asymmetric techniques. The security definition, called SK-security, ensures that KE protocols can be used to provide secure channels by guaranteeing authentication and secrecy of transmitted data. This is achieved by proving that if an SK-secure KE protocol is used with secure MAC and encryption functions, the resulting channel provides both authentication and secrecy. The paper also introduces an adversarial model (UM) where an attacker can control communication links and perform various attacks, including session-state reveals, session-key queries, and party corruption. The paper then presents a methodology for designing and analyzing KE protocols under the assumption that communication links are perfectly authenticated, and then transforming these protocols into secure ones in the realistic UM model using an "authenticator" tool. The paper demonstrates that the SK-security definition is suitable for ensuring secure channels when used with secure cryptographic functions. It also shows that the SK-security definition can be applied to prove the security of important protocols like the two-move Diffie-Hellman protocol under the Decisional Diffie-Hellman assumption. The paper further discusses the concept of "perfect forward secrecy" and defines a weaker notion of SK-security without PFS by disallowing key expiration. The paper concludes that the SK-security definition is a powerful and practical approach for analyzing KE protocols and ensuring secure communication channels. It provides a formal framework for proving the security of KE protocols and their use in building secure channels, and demonstrates its applicability to important protocols like Diffie-Hellman and key-transport.This paper presents a formalism for analyzing key-exchange (KE) protocols that combines previous approaches to define a security notion with important analytical benefits. The security definition allows KE protocols to be composed with symmetric encryption and authentication functions to provide provably secure communication channels. It also enables simple modular proofs of security by designing and proving security in an idealized model with perfectly authenticated links, then translating them to realistic settings with adversary-controlled links using general tools. The paper applies this formalism to prove the security of two classes of KE protocols: Diffie-Hellman and key-transport protocols, authenticated via symmetric or asymmetric techniques. The security definition, called SK-security, ensures that KE protocols can be used to provide secure channels by guaranteeing authentication and secrecy of transmitted data. This is achieved by proving that if an SK-secure KE protocol is used with secure MAC and encryption functions, the resulting channel provides both authentication and secrecy. The paper also introduces an adversarial model (UM) where an attacker can control communication links and perform various attacks, including session-state reveals, session-key queries, and party corruption. The paper then presents a methodology for designing and analyzing KE protocols under the assumption that communication links are perfectly authenticated, and then transforming these protocols into secure ones in the realistic UM model using an "authenticator" tool. The paper demonstrates that the SK-security definition is suitable for ensuring secure channels when used with secure cryptographic functions. It also shows that the SK-security definition can be applied to prove the security of important protocols like the two-move Diffie-Hellman protocol under the Decisional Diffie-Hellman assumption. The paper further discusses the concept of "perfect forward secrecy" and defines a weaker notion of SK-security without PFS by disallowing key expiration. The paper concludes that the SK-security definition is a powerful and practical approach for analyzing KE protocols and ensuring secure communication channels. It provides a formal framework for proving the security of KE protocols and their use in building secure channels, and demonstrates its applicability to important protocols like Diffie-Hellman and key-transport.