The paper presents a formalism for analyzing key-exchange (KE) protocols, combining previous definitional approaches to define security in a way that offers significant analytical benefits. Key features include: 1. **Security Definition**: Any KE protocol that satisfies the security definition can be composed with symmetric encryption and authentication functions to provide provably secure communication channels. 2. **Modular Proofs**: The definition allows for simple modular proofs of security, where protocols can be designed and proven secure in an idealized model with perfectly authenticated communication links, and then translated to realistic settings using general tools. The authors exemplify their results by applying the formalism to two classes of KE protocols: Diffie-Hellman and key-transport, authenticated via symmetric or asymmetric techniques. They demonstrate that SK-secure KE protocols can be used to establish secure channels by combining them with secure MAC and encryption functions. The paper also introduces a methodology for designing and analyzing KE protocols in a simplified adversarial setting (authenticated-links model) and transforming these protocols into secure versions in realistic settings using authenticators. This approach simplifies the design and analysis of KE protocols while ensuring their security in practical scenarios. The formalism is based on the indistinguishability approach, which defines security as the infeasibility for an attacker to distinguish the value of a key generated by the protocol from an independent random value. The authors extend this approach to a more general model for analyzing security protocols, capturing the specific needs of KE protocols. The paper includes a detailed discussion of the adversarial model, session-key security, and the concept of perfect forward secrecy. It also provides a formal definition of SK-security and demonstrates its application to the Diffie-Hellman protocol and a key-transport protocol based on public-key encryption. Finally, the paper shows how SK-secure KE protocols can be used to realize secure channels by combining them with secure MAC and encryption functions, ensuring both authentication and secrecy of transmitted data.The paper presents a formalism for analyzing key-exchange (KE) protocols, combining previous definitional approaches to define security in a way that offers significant analytical benefits. Key features include: 1. **Security Definition**: Any KE protocol that satisfies the security definition can be composed with symmetric encryption and authentication functions to provide provably secure communication channels. 2. **Modular Proofs**: The definition allows for simple modular proofs of security, where protocols can be designed and proven secure in an idealized model with perfectly authenticated communication links, and then translated to realistic settings using general tools. The authors exemplify their results by applying the formalism to two classes of KE protocols: Diffie-Hellman and key-transport, authenticated via symmetric or asymmetric techniques. They demonstrate that SK-secure KE protocols can be used to establish secure channels by combining them with secure MAC and encryption functions. The paper also introduces a methodology for designing and analyzing KE protocols in a simplified adversarial setting (authenticated-links model) and transforming these protocols into secure versions in realistic settings using authenticators. This approach simplifies the design and analysis of KE protocols while ensuring their security in practical scenarios. The formalism is based on the indistinguishability approach, which defines security as the infeasibility for an attacker to distinguish the value of a key generated by the protocol from an independent random value. The authors extend this approach to a more general model for analyzing security protocols, capturing the specific needs of KE protocols. The paper includes a detailed discussion of the adversarial model, session-key security, and the concept of perfect forward secrecy. It also provides a formal definition of SK-security and demonstrates its application to the Diffie-Hellman protocol and a key-transport protocol based on public-key encryption. Finally, the paper shows how SK-secure KE protocols can be used to realize secure channels by combining them with secure MAC and encryption functions, ensuring both authentication and secrecy of transmitted data.