Verified Contributive Channel Bindings for Compound Authentication

Compound authentication protocols, such as EAP in IKEv2 or SASL over TLS, bind application-level authentication to a transport-level authenticated channel in order to obtain strong composite authentication under weak trust assumptions. Despite their wide deployment, these protocols remain poorly understood, leading to several credential forwarding man-in-the-middle attacks. We present the first formal models for several compound authentication protocols, and analyze them against a rich threat model that includes compromised certificates, leaked session keys, and Diffie-Hellman small subgroup confinement. Our analysis uncovers new compound authentication attacks on TLS renegotiation, SSH re-exchange, IKEv2 resumption, and a number of other channel binding proposals. We propose new channel bindings and formally evaluate their effectiveness using the automated symbolic cryptographic protocol verifier, ProVerif. Our automated analysis is the first to reconstruct the recently published triple handshake attacks on TLS, and the first to provide rigorous guarantees for its proposed countermeasure.