Securing the Future Internet with TLS 1.3 – SafeTLS

TLS/SSL (currently version TLS 1.2) is one of the 3 essential cryptographic protocols used today (together with SSH and IPSec). Despite its central role in securing e-commerce, Internet browsing, email, VoIP, etc., despite the fact that almost every search and connection query in every browser in the world requires its use, this protocol still presents security flaws in its conception. To overcome recent attacks, such as FREAK, LogJam, 3Shake, SLOTH, or DROWN, a new version i.e. TLS 1.3 has recently been drafted. Our project, SafeTLS, addresses the security both of TLS 1.3 and of TLS 1.2 as they are (expected to be) used, in three important ways:

(1) by providing a better understanding -- from the point of view of provable security – of the TLS 1.3 and 1.2 handshakes as they are used in real life. One important, and new aspect of our work concerns formalizing and proving the privacy properties attained by the newly-designed TLS 1.3 draft; another concerns the security of secure-channel establishment protocols against mass surveillance threats, in which a powerful adversary called Big Brother can learn "confidential" data exchanged between users. Another important, innovative goal of our work concerns understanding the degradation of security of the TLS handshake when it is used with middleware infrastructures – which is predominantly the case nowadays. Finally, we will assess and provide new primitives for use in TLS and D-TLS, by looking at the candidates of the CAESAR competition and by studying new elliptic curves fashioned specifically for use in this protocol.

(2) by providing clients with a tool that detects the quality of each TLS connection at runtime, and instructs the client what type of data can be safely exchanged across such a channel. In particular, the explanations given to the client must be understandable and as short as possible, making this tool an aid to a safer use of Internet browsing. Another aspect of our work concerns informing clients whether middleware is, in fact, being used in their TLS-secured connections. We note that, while middleware decreases latency for the client and storage and bandwidth needs for servers, it may represent an additional risk to clients, of which they are actually not informed. Indeed, most middleware is designed to pose as the original server that the client wanted to reach.

(3) by addressing the problem of secure TLS implementations. We first propose to analyze the security offered by a number of available TLS 1.2 (and earlier) implementations, such as s2n, BoringSSL, and mbedTLS. By furthermore using the automatic verification tool EasyCrypt to formulate and prove the security of the TLS 1.3 handshake (with all its modes of operation), we can also use tools that transform EasyCrypt proofs to certified code, giving explicit guidelines for a secure future TLS 1.3 implementation.

Our results will be manifested in the following types of results: (1) security proofs (using formal methods and provable security methodologies), indicating lower bounds on security; (2) impossibility results and upper bounds on security, in particular for security against mass-surveillance and for downgrading due to middleware; (3) the tool (application) designed to assess the quality of each TLS connection at runtime, which will be open-source and made available to any user; (4) the certified code corresponding to a secure implementation of TLS 1.3.