Negotiation security

Intuitively, the goal of negotiation security is that no attacker should be able to get two parties to successfully agree upon a worse ciphersuite than the best

ciphersuite they mutually support. If an adversary succeeds in getting the parties to use a worse ciphersuite then what is prescribed by their mutual con-figurations, it is said to have performed adowngrade attack. As mentioned in Section 2.2.3, if WEP is supported alongside Robust Security Network (RSN) ciphersuites, then IEEE 802.11 cannot provide any protection against down-grade attacks. This is because when WEP is used, the 4WHS protocol is not run at all, and hence there is no way for the client and access point to ver-ify that a downgrade attack has occurred. The IEEE 802.11 standard [IEEE 802.11] requires that WEP and RSN should not be enabled together. In the remainder we only discuss the negotiation security of IEEE 802.11 when using RSN ciphersuites exclusively.

Similar to the modular composition theorem of BDKSS [Ber+14] for the multi-ciphersuite security of a protocolNP#»

Π, Dowling and Stebila [DS15] pro-posed a generic composition theorem that relates the negotiation security of NP#»

Π to the authentication security of the individual sub-protocols Π_c. How-ever, their theorem assumes that different sub-protocols use different long-term keys, and so cannot be applied to IEEE 802.11.

In contrast, Bhargavan et al. [Bha+16] formulate negotiation security in the setting of key reuse across ciphersuites. They also prove a generic theorem that allows the negotiation security ofNP#»

Π to be lifted from a simplercore negotia-tion protocolNP extracted fromNPand #»

Π. Thus, it is sufficient to focus on the negotiation security of protocolNP. Using their generic theorem, Bhargavan et al. [Bha+16] proved the negotiation security of the SSH [RFC4253] protocol under agile assumptions on its cryptographic primitives.

Admittedly, the value of applying the composition theorem of Bhargavan et al. [Bha+16] to IEEE 802.11 is rather limited, since the core negotiation pro-tocol one can extract for IEEE 802.11 is almost the same as the whole propro-tocol itself; essentially corresponding to the protocol we have shown in Figure 6.5.

A proof of negotiation security for IEEE 802.11 would thus proceed in more or less the same way as the proofs of multi-ciphersuite security—which them-selves are essentially the same as our proofs of single-ciphersuite AKE security (Theorem 6.1) and explicit entity authentication (Theorem 6.4). But again, it would require agile security assumptions on the KDFs and MACs.

As mentioned in Section 6.4.1, Bhargavan et al. [Bha+16] also analyzed the negotiation security of IKEv1-PSK in aggressive mode, which is very similar to the 4WHS protocol. However, for simplicity they assumed that only a single KDF and a single MAC algorithm was being used in order to rely on more traditional non-agile security assumptions.

Conclusions

Contents

7.1 Limitations of our results . . . 145 7.1.1 Things not covered by our analysis . . . 146 7.1.2 Tightness of security reductions . . . 147 7.2 Future work and open problems . . . 147

In recent years there has been a great interest in formally analyzing the TLS protocol. Almost every aspect of TLS have been scrutinized, ranging from the security of its core handshake protocol [MSW10, Jag+12, KPW13b, Brz+13a, KSS13, Li+14, Bha+14b] and Record Layer Protocol [Kra01, PRS11, Boy+16], to its multi-ciphersuite and (re-)negotiation (in)security [GKS13, Ber+14, DS15, Beu+15]. Even for the unfinished upcoming TLS 1.3 standard, there have already been multiple results [Bad+15b, Dow+15, KW15, Dow+16, FG17]. This analysis has greatly increased our understanding of TLS. At the same time, there are other important real-world protocols that have received much less attention. EAP, EAP-TLS and IEEE 802.11 are all examples of this.

In this thesis we have tried to remedy this state-of-affairs by conducting a for-mal security analysis of the three aforementioned protocols in the game-based setting. We have concentrated on the central cryptographic operations of each of these protocols.

Beginning with EAP in Chapter 4, we showed through two generic compo-sition theorems how the security of the overall EAP framework is sound. More specifically, these composition theorems give sufficient security requirements on the components that make up EAP in order to securely instantiate the frame-work. In this sense, they make precise the security requirements that were only informally described in [RFC5247]. A particularly interesting observation is the

144

importance of channel binding in the EAP methods. This has so far lacked any formal justification in the EAP standard, only being argued based on ad-hoc examples. Recall that our first composition theorem showed that basic EAP is a secure 3P-AKE protocol. Without channel binding this would not be true.

In Chapter 5 we analyzed the EAP-TLS protocol, which is one of the most widely supported EAP methods. We showed that it is a secure 2P-AKE proto-col. However, more interesting than this result on its own, is how it was estab-lished. Namely, our result on EAP-TLS follows as a corollary of a more general theorem that shows how almost any secure channel protocol (i.e., TLS-like ACCE protocols), can be transformed into a secure AKE protocol. Although intuitively straightforward, the proof of this was non-trivial.

Finally, in Chapter 6 we analyzed the IEEE 802.11 protocol. We first looked at the setting found in most home networks, where a common key is manually installed at all connecting devices. In this scenario we proved that the 4WHS protocol is a secure 2P-AKE with no forward secrecy, and that it additionally provides explicit entity authentication. These are also exactly the properties needed by our second composition theorem, which when combined with our 4WHS result, culminated in a first security proof of EAP + IEEE 802.11 in the computational setting. Besides our results on the 4WHS handshake, we also proved that the IEEE 802.11 channel protocol CCMP is a secure stateful authenticated encryption scheme.

7.1 Limitations of our results

There are several caveats to our results. First and foremost, all of our results are based on simplifications of the actual real-world protocols. This is always necessary in order to make any analysis feasible. Nevertheless, it opens up the possibility that our modeling does not accurately reflect the protocols as they really are. Unfortunately, this is a fundamental problem for which there is no easy solution. A recent trend in the analysis of TLS has been to introduce machine-checkable proofs, and even derive models from executable code itself, so as to mirror the real TLS protocol as closely as possible [Bha+14b, Beu+15].

But even these approaches make simplifications compared to the real protocol.

Moreover, it is not clear how this approach can be applied to the kind of generic theorems we have proven, which inherently have no implementations.

In the end, we have tried to model the protocols as faithfully as we can, but ultimately there are no guarantees that our models completely match the real-world protocols.