Key-exchange protocols such as TLS, SSH, IPsec, and ZRTP are highly congurable, with typical deployments supporting multiple protocol versions, cryptographic algorithms and parameters. In the rst messages of the protocol, the peers negotiate one specic combination: the protocol mode, based on their local congurations. With few notable exceptions, most cryptographic analyses of congurable protocols consider a single mode at a time. In contrast, downgrade attacks, where a network adversary forces peers to use a mode weaker than the one they would normally negotiate, are a recurrent problem in practice. How to support congurability while at the same time guaranteeing the preferred mode is negotiated? We set to answer this question by designing a formal framework to study downgrade resilience and its relation to other security properties of key-exchange protocols. First, we study the causes of downgrade attacks by dissecting and classifying known and novel attacks against widely use...