The Transport Layer Security (TLS) protocol is the most widely used security protocol on the Internet. It supports negotiation of a wide variety of cryptographic primitives through different cipher suites, various modes of client authentication, and additional features such as session resumption and renegotiation. Despite its widespread use, only recently has the full TLS protocol been proven secure, and only then a single ciphersuite family (TLS_DHE_DSS_WITH_3DES_EDE_CBC_SHA) with no additional features. These additional features have been the cause of practical attacks on TLS. In 2009, Ray and Dispensa demonstrated how TLS renegotiation allows an attacker to splice together its own session with that of a victim, resulting in a man-in-the-middle attack on TLS-reliant applications such as HTTP. TLS was subsequently patched with two defence mechanisms for protection against this attack.
We present the first formal treatment of renegotiation in secure channel establishment protocols. We add optional renegotiation to the authenticated and confidential channel establishment model of Jager et al., an adaptation of the Bellare--Rogaway authenticated key exchange model. We describe the attack of Ray and Dispensa on TLS within our model. Although the two proposed fixes for TLS do not achieve our strongest notion of security, they do achieve a weaker but still reasonable security notion, and TLS can be easily adjusted to achieve that stronger level of security.