Papers tagged as TLS
  1. DROWN: Breaking TLS using SSLv2 2016 Attacks KeyExchange Measurement Network Protocols TLS Usenix
    Nimrod Aviram, Sebastian Schinzel, Juraj Somorovsky, Nadia Heninger, Maik Dankel, Jens Steube, Luke Valenta, David Adrian, J. Alex Halderman, Viktor Dukhovni, Emilia Käsper, Shaanan Cohney, Susanne Engels, Christof Paar, and Yuval Shavitt

    We present DROWN, a novel cross-protocol attack on TLS that uses a server supporting SSLv2 as an oracle to decrypt modern TLS connections.
    We introduce two versions of the attack. The more general form exploits multiple unnoticed protocol flaws in SSLv2 to develop a new and stronger variant of the Bleichenbacher RSA padding-oracle attack. To decrypt a 2048-bit RSA TLS ciphertext, an attacker must observe
    1,000 TLS handshakes, initiate 40,000 SSLv2 connections, and perform 2^50 offline work. The victim client never initiates SSLv2 connections. We implemented the attack and can decrypt a TLS 1.2 handshake using 2048-bit RSA in under 8 hours, at a cost of $440 on Amazon EC2. Using Internet-wide scans, we find that 33% of all HTTPS servers and 22% of those with browser-trusted certificates are vulnerable to this protocol-level attack due
    to widespread key and certificate reuse.
    For an even cheaper attack, we apply our new techniques together with a newly discovered vulnerability in OpenSSL that was present in releases from 1998 to early 2015. Given an unpatched SSLv2 server to use as an oracle, we can decrypt a TLS ciphertext in one minute on a single CPU - fast enough to enable man-in-the-middle attacks against modern browsers. We find that 26% of HTTPS servers are vulnerable to this attack.
    We further observe that the QUIC protocol is vulnerable to a variant of our attack that allows an attacker to impersonate a server indefinitely after performing as few as 2^17 SSLv2 connections and 2^58 offline work.
    We conclude that SSLv2 is not only weak, but actively harmful to the TLS ecosystem.

  2. Why Banker Bob (still) can't get TLS right: A Security Analysis of TLS in Leading UK Banking Apps 2017 FinancialCryptography TLS
    Tom Chothia, Flavio Garcia, Christopher Heppel, Christopher McMahon-Stone

    This paper presents a security review of the mobile apps provided by the UK’s leading banks; we focus on the connections the apps make, and the way in which TLS is used. We apply existing TLS testing methods to the apps which only find errors in legacy apps. We then go on to look at extensions of these methods and find five of the apps have serious vulnerabilities. In particular, we find an app that pins a TLS root CA certificate, but do not verify the hostname. In this case, the use of certificate pinning means that all existing test methods would miss detecting the hostname verification flaw. We also find one app that doesn’t check the certificate hostname, but bypasses proxy settings, resulting in failed detection by pentesting tools. We find that three apps load adverts over insecure connections, which could be exploited for in-app phishing attacks. Some of the apps used the users’ PIN as authentication, for which PCI guidelines require extra security, so these apps use an additional cryptographic protocol; we study the underlying protocol of one banking app in detail and show that it provides little additional protection, meaning that an active man-in-the-middle attacker can retrieve the user’s credentials, login to the bank and perform every operation the legitimate user could.

  3. Secure Opportunistic Multipath Key Exchange 2018 CCS Certificates PKI TLS
    Sergiu Costea, Marios O. Choudary, Doru Gucea, Björn Tackmann and Costin Raiciu

    The security of today’s widely used communication security protocols is based on trust in Certificate Authorities (CAs). However, the real security of this approach is debatable, since certificate handling is tedious and many recent attacks have undermined the trust in CAs. On the other hand, opportunistic encryption protocols such as Tcpcrypt, which are currently gaining momentum as an alternative to no encryption, have similar security to using untrusted CAs or self-signed certificates: they only protect against passive attackers.

    In this paper, we present a key exchange protocol, Secure Multipath Key Exchange (SMKEX), that enables all the benefits of opportunistic encryption (no need for trusted third parties or pre-established secrets), as well as proven protection against some classes of active attackers. Furthermore, SMKEX can be easily extended to a trust-on-first-use setting and can be easily integrated with TLS, providing the highest security for opportunistic encryption to date while also increasing the security of standard TLS.

    We show that SMKEX is made practical by the current availability of path diversity between different AS-es. We also show a method to create path diversity with encrypted tunnels without relying on the network topology. These allow SMKEX to provide protection against most adversaries for a majority of Alexa top 100 web sites.

    We have implemented SMKEX using a modified Multipath TCP kernel implementation and a user library that overwrites part of the socket API, allowing unmodified applications to take advantage of the security provided by SMKEX.

  4. Partially specified channels: The TLS 1.3 record layer without elision 2018 CCS CryptoStandards TLS
    Christopher Patton and Thomas Shrimpton

    We advance the study of secure stream-based channels (Fischlin et al., CRYPTO ’15) by considering the multiplexing of many data streams over a single channel, an essential feature of real world protocols such as TLS. Our treatment adopts the definitional perspective of Rogaway and Stegers (CSF ’09), which offers an elegant way to reason about what standardizing documents actually provide: a partial specification of a protocol that admits a collection of compliant, fully realized implementations. We formalize partially specified channels as the component algorithms of two parties communicating over a channel. Each algorithm has an oracle that provides specification details; the algorithms abstract the things that must be explicitly specified, while the oracle abstracts the things that need not be. Our security notions, which capture a variety of privacy and integrity goals, allow the adversary to respond to these oracle queries; security relative to these notions implies that the channel withstands attacks in the presence of worst-case (i.e., adversarial) realizations of the specification details. We apply this framework to a formal treatment of the TLS 1.3 record and, in doing so, show that its security hinges crucially upon details left unspecified by the standard.

  5. Session Resumption Protocols and Efficient Forward Security for TLS 1.3 0-RTT 2019 Eurocrypt TLS
    Nimrod Aviram, Kai Gellert, and Tibor Jager

    The TLS 1.3 0-RTT mode enables a client reconnecting to a server to send encrypted application-layer data in “0-RTT” (“zero round-trip time”), without the need for a prior interactive handshake. This fundamentally requires the server to reconstruct the previous session’s encryption secrets upon receipt of the client’s first message. The standard techniques to achieve this are Session Caches or, alternatively, Session Tickets. The former provides forward security and resistance against replay attacks, but requires a large amount of server-side storage. The latter requires negligible storage, but provides no forward security and is known to be vulnerable to replay attacks.

    In this paper, we first formally define session resumption protocols as an abstract perspective on mechanisms like Session Caches and Session Tickets. We give a new generic construction that provably provides forward security and replay resilience, based on puncturable pseudorandom functions (PPRFs). This construction can immediately be used in TLS 1.3 0-RTT and deployed unilaterally by servers, without requiring any changes to clients or the protocol.

    We then describe two new constructions of PPRFs, which are particularly suitable for use for forward-secure and replay-resilient session resumption in TLS~1.3. The first construction is based on the strong RSA assumption. Compared to standard Session Caches, for “128-bit security” it reduces the required server storage by a factor of almost 20, when instantiated in a way such that key derivation and puncturing together are cheaper on average than one full exponentiation in an RSA group. Hence, a 1 GB Session Cache can be replaced with only about 51 MBs of storage, which significantly reduces the amount of secure memory required. For larger security parameters or in exchange for more expensive computations, even larger storage reductions are achieved. The second construction combines a standard binary tree PPRF with a new “domain extension” technique. For a reasonable choice of parameters, this reduces the required storage by a factor of up to 5 compared to a standard Session Cache. It employs only symmetric cryptography, is suitable for high-traffic scenarios, and can serve thousands of tickets per second.

  6. The 9 Lives of Bleichenbacher's CAT: New Cache ATtacks on TLS Implementations 2019 Attacks Oakland TLS
    Eyal Ronen, Robert Gillham, Daniel Genkin, Adi Shamir, David Wong, and Yuval Yarom

    At CRYPTO’98, Bleichenbacher published his seminal paper which described a padding oracle attack against RSA implementations that follow the PKCS #1 v1.5 standard.

    Over the last twenty years researchers and implementors had spent a huge amount of effort in developing and deploying numerous mitigation techniques which were supposed to plug all the possible sources of Bleichenbacher-like leakages. However, as we show in this paper most implementations are still vulnerable to several novel types of attack based on leakage from various microarchitectural side channels: Out of nine popular implementations of TLS that we tested, we were able to break the security of seven implementations with practical proof-of-concept attacks. We demonstrate the feasibility of using those Cache-like ATacks (CATs) to perform a downgrade attack against any TLS connection to a vulnerable server, using a BEAST-like Man in the Browser attack.

    The main difficulty we face is how to perform the thousands of oracle queries required before the browser’s imposed timeout (which is 30 seconds for almost all browsers, with the exception of Firefox which can be tricked into extending this period). The attack seems to be inherently sequential (due to its use of adaptive chosen ciphertext queries), but we describe a new way to parallelize Bleichenbacher-like padding attacks by exploiting any available number of TLS servers that share the same public key certificate.

    With this improvement, we could demonstrate the feasibility of a downgrade attack which could recover all the 2048 bits of the RSA plaintext (including the premaster secret value, which suffices to establish a secure connection) from five available TLS servers in under 30 seconds. This sequential-to-parallel transformation of such attacks can be of independent interest, speeding up and facilitating other side channel attacks on RSA implementations.

  7. Stacco: Differentially Analyzing Side-Channel Traces for Detecting SSL/TLS Vulnerabilities in Secure Enclaves 2017 Attacks CCS IntelSGX SideChannels TLS
    Yuan Xiao, Mengyuan Li, Sanchuan Chen, and Yinqian Zhang

    Intel Software Guard Extension (SGX) offers software applications a shielded execution environment, dubbed enclave, to protect their confidentiality and integrity from malicious operating systems. As processors with this extended feature become commercially available, many new software applications are developed to enrich to the SGX-enabled ecosystem. One important primitive for these applications is a secure communication channel between the enclave and a remote trusted party. The SSL/TLS protocol, which is the de facto standard for protecting transport-layer network communications, has been broadly regarded a natural choice for such purposes. However, in this paper, we show that the marriage between SGX and SSL may not be smooth sailing.

    Particularly, we consider a category of side-channel attacks against SSL/TLS implementations in secure enclaves, which we call the control-flow inference attacks. In these attacks, the malicious operating system kernel may perform a powerful man-in-the-kernel attack to collect execution traces of the enclave programs at the page level, the cacheline level, or the branch level, while positioning itself in the middle of the two communicating parties. At the center of our work is a differential analysis framework, dubbed Stacco, to dynamically analyze the SSL/TLS implementations and detect vulnerabilities-discernible execution traces-that can be exploited as decryption oracles. Surprisingly, in spite of the prevailing constant-time programming paradigm adopted by many cryptographic libraries, we found exploitable vulnerabilities in the latest versions of all the SSL/TLS libraries we have examined.

    To validate the detected vulnerabilities, we developed a man-in-the-kernel adversary to demonstrate Bleichenbacher attacks against the latest OpenSSL library running in the SGX enclave (with the help of Graphene) and completely broke the PreMasterSecret encrypted by a 4096-bit RSA public key with only 57286 queries. We also conducted CBC padding oracle attacks against the latest GnuTLS running in Graphene-SGX and an open-source SGX implementation of mbedTLS (i.e., mbedTLS-SGX) that runs directly inside the enclave, and showed that it only needs 48388 and 25717 queries, respectively, to break one block of AES ciphertext. Empirical evaluation suggests these man-in-the-kernel attacks can be completed within 1 or 2 hours. Our results reveal the insufficient understanding of side-channel security in SGX settings, and our study will provoke discussions on the secure implementation and adoption of SSL/TLS in secure enclaves.

  8. Pseudo Constant Time Implementations of TLS Are Only Pseudo Secure 2018 CCS SideChannels TLS
    Eyal Ronen, Kenneth G. Paterson and Adi Shamir

    Today, about 10% of TLS connections are still using CBC-mode cipher suites, despite a long history of attacks and the availability of better options (e.g. AES-GCM). In this work, we present three new types of attack against four popular fully patched implementations of TLS (Amazon’s s2n, GnuTLS, mbed TLS and wolfSSL) which elected to use “pseudo constant time” countermeasures against the Lucky 13 attack on CBC-mode. Our attacks combine several variants of the PRIME+PROBE cache timing technique with a new extension of the original Lucky 13 attack. They apply in a cross-VM attack setting and are capable of recovering most of the plaintext whilst requiring only a moderate number of TLS connections. Along the way, we uncovered additional serious (but easy to patch) bugs in all four of the TLS implementations that we studied; in three cases, these bugs lead to Lucky 13 style attacks that can be mounted remotely with no access to a shared cache. Our work shows that adopting pseudo constant time countermeasures is not sufficient to attain real security in TLS implementations in CBC mode.

  9. One&Done: A Single-Decryption EM-Based Attack on OpenSSL’s Constant-Time Blinded RSA 2018 Attacks SideChannels TLS Usenix
    Monjur Alam, Haider Adnan Khan, Moumita Dey, Nishith Sinha, Robert Callan, Alenka Zajic, and Milos Prvulovic

    This paper presents the first side channel attack approach that, without relying on the cache organization and/or timing, retrieves the secret exponent from a single decryption on arbitrary ciphertext in a modern (current version of OpenSSL) fixed-window constant-time implementation of RSA. Specifically, the attack recovers the exponent’s bits during modular exponentiation from analog signals that are unintentionally produced by the processor as it executes the constant-time code that constructs the value of each “window” in the exponent, rather than the signals that correspond to squaring/multiplication operations and/or cache behavior during multiplicand table lookup operations. The approach is demonstrated using electromagnetic (EM) emanations on two mobile phones and an embedded system, and after only one decryption in a fixed-window RSA implementation it recovers enough bits of the secret exponents to enable very efficient (within seconds) reconstruction of the full private RSA key.

    Since the value of the ciphertext is irrelevant to our attack, the attack succeeds even when the ciphertext is unknown and/or when message randomization (blinding) is used. Our evaluation uses signals obtained by demodulating the signal from a relatively narrow band (40 MHz) around the processor’s clock frequency (around 1GHz), which is within the capabilities of compact sub-$1,000 software-defined radio (SDR) receivers.

    Finally, we propose a mitigation where the bits of the exponent are only obtained from an exponent in integer-sized groups (tens of bits) rather than obtaining them one bit at a time. This mitigation is effective because it forces the attacker to attempt recovery of tens of bits from a single brief snippet of signal, rather than having a separate signal snippet for each individual bit. This mitigation has been submitted to OpenSSL and was merged into its master source code branch prior to the publication of this paper.

  10. Return Of Bleichenbacher’s Oracle Threat (ROBOT) 2018 Attacks TLS Usenix
    Hanno Böck, Juraj Somorovsky, and Craig Young

    In 1998 Bleichenbacher presented an adaptive chosen-ciphertext attack on the RSA PKCS#1 v1.5 padding scheme. The attack exploits the availability of a server which responds with different messages based on the ciphertext validity. This server is used as an oracle and allows the attacker to decrypt RSA ciphertexts. Given the importance of this attack, countermeasures were defined in TLS and other cryptographic standards using RSA PKCS#1 v1.5.

    We perform the first large-scale evaluation of Bleichenbacher’s RSA vulnerability. We show that this vulnerability is still very prevalent in the Internet and affected almost a third of the top 100 domains in the Alexa Top 1 Million list, including Facebook and Paypal.

    We identified vulnerable products from nine different vendors and open source projects, among them F5, Citrix, Radware, Palo Alto Networks, IBM, and Cisco. These implementations provide novel side-channels for constructing Bleichenbacher oracles: TCP resets, TCP timeouts, or duplicated alert messages. In order to prove the importance of this attack, we have demonstrated practical exploitation by signing a message with the private key of \texttt{}’s HTTPS certificate. Finally, we discuss countermeasures against Bleichenbacher attacks in TLS and recommend to deprecate the RSA encryption key exchange in TLS and the RSA PKCS~#1~v1.5 standard.

  11. Scalable Scanning and Automatic Classification of TLS Padding Oracle Vulnerabilities 2019 Attacks TLS Usenix
    Robert Merget, Juraj Somorovsky, Nimrod Aviram, Craig Young, Janis Fliegenschmidt, Jörg Schwenk, and Yuval Shavitt

    The TLS protocol provides encryption, data integrity, and authentication on the modern Internet. Despite the protocol’s importance, currently-deployed TLS versions use obsolete cryptographic algorithms which have been broken using various attacks. One prominent class of such attacks is CBC padding oracle attacks. These attacks allow an adversary to decrypt TLS traffic by observing different server behaviors which depend on the validity of CBC padding.

    We present the first large-scale scan for CBC padding oracle vulnerabilities in TLS implementations on the modern Internet. Our scan revealed vulnerabilities in 1.83% of the Alexa Top Million websites, detecting nearly 100 different vulnerabilities. Our scanner observes subtle differences in server behavior, such as responding with different TLS alerts, or with different TCP header flags.

    We used a novel scanning methodology consisting of three steps. First, we created a large set of probes that detect vulnerabilities at a considerable scanning cost. We then reduced the number of probes using a preliminary scan, such that a smaller set of probes has the same detection rate but is small enough to be used in large-scale scans. Finally, we used the reduced set to scan at scale, and clustered our findings with a novel approach using graph drawing algorithms.

    Contrary to common wisdom, exploiting CBC padding oracles does not necessarily require performing precise timing measurements. We detected vulnerabilities that can be exploited simply by observing the content of different server responses. These vulnerabilities pose a significantly larger threat in practice than previously assumed.

  12. "I Have No Idea What I'm Doing" - On the Usability of Deploying HTTPS 2017 Measurement TLS Usenix
    Katharina Krombholz, Wilfried Mayer, Martin Schmiedecker, and Edgar Weippl

    Protecting communication content at scale is a difficult task, and TLS is the protocol most commonly used to do so. However, it has been shown that deploying it in a truly secure fashion is challenging for a large fraction of online service operators. While Let’s Encrypt was specifically built and launched to promote the adoption of HTTPS, this paper aims to understand the reasons for why it has been so hard to deploy TLS correctly and studies the usability of the deployment process for HTTPS. We performed a series of experiments with 28 knowledgable participants and revealed significant usability challenges that result in weak TLS configurations. Additionally, we conducted expert interviews with 7 experienced security auditors. Our results suggest that the deployment process is far too complex even for people with proficient knowledge in the field, and that server configurations should have stronger security by default. While the results from our expert interviews confirm the ecological validity of the lab study results, they additionally highlight that even educated users prefer solutions that are easy to use. An improved and less vulnerable workflow would be very beneficial to finding stronger configurations in the wild.

  13. Measuring HTTPS Adoption on the Web 2017 Measurement TLS Usenix
    Adrienne Porter Felt, Richard Barnes, April King, Chris Palmer, Chris Bentzel, and Parisa Tabriz

    HTTPS ensures that the Web has a base level of privacy and integrity. Security engineers, researchers, and browser vendors have long worked to spread HTTPS to as much of the Web as possible via outreach efforts, developer tools, and browser changes. How much progress have we made toward this goal of widespread HTTPS adoption? We gather metrics to benchmark the status and progress of HTTPS adoption on the Web in 2017. To evaluate HTTPS adoption from a user perspective, we collect large-scale, aggregate user metrics from two major browsers (Google Chrome and Mozilla Firefox). To measure HTTPS adoption from a Web developer perspective, we survey server support for HTTPS among top and long-tail websites. We draw on these metrics to gain insight into the current state of the HTTPS ecosystem.

  14. The use of TLS in Censorship Circumvention 2019 Censorship Measurement NDSS TLS
    Sergey Frolov and Eric Wustrow

    TLS, the Transport Layer Security protocol, has
    quickly become the most popular protocol on the Internet, already
    used to load over 70% of web pages in Mozilla Firefox. Due
    to its ubiquity, TLS is also a popular protocol for censorship
    circumvention tools, including Tor and Signal, among others.

    However, the wide range of features supported in TLS makes
    it possible to distinguish implementations from one another by
    what set of cipher suites, elliptic curves, signature algorithms, and
    other extensions they support. Already, censors have used deep
    packet inspection (DPI) to identify and block popular circumven-
    tion tools based on the fingerprint of their TLS implementation.

    In response, many circumvention tools have attempted to
    mimic popular TLS implementations such as browsers, but this
    technique has several challenges. First, it is burdensome to keep
    up with the rapidly-changing browser TLS implementations, and
    know what fingerprints would be good candidates to mimic.
    Second, TLS implementations can be difficult to mimic correctly,
    as they offer many features that may not be supported by the
    relatively lightweight libraries used in typical circumvention tools.
    Finally, dependency changes and updates to the underlying li-
    braries can silently impact what an application’s TLS fingerprint
    looks like, making it difficult for tools to control.

    In this paper, we collect and analyze real-world TLS traffic
    from over 11.8 billion TLS connections over 9 months to identify
    a wide range of TLS client implementations actually used on
    the Internet. We use our data to analyze TLS implementations
    of several popular censorship circumvention tools, including
    Lantern, Psiphon, Signal, Outline, Tapdance, and Tor (Snowflake
    and meek). We find that the many of these tools use TLS
    configurations that are easily distinguishable from the real-world
    traffic they attempt to mimic, even when these tools have put
    effort into parroting popular TLS implementations.

    To address this problem, we have developed a library, uTLS,
    that enables tool maintainers to automatically mimic other pop-
    ular TLS implementations. Using our real-world traffic dataset,
    we observe many popular TLS implementations we are able to
    correctly mimic with uTLS, and we describe ways our tool can
    more flexibly adopt to the dynamic TLS ecosystem with minimal
    manual effort.

  15. maTLS: How to Make TLS middlebox-aware? 2019 NDSS TLS
    Hyunwoo Lee and Zachary Smith and Junghwan Lim and Gyeongjae Choi and Selin Chun and Taejoong Chung and Ted "Taekyoung" Kwon

    Middleboxes (MBs) are widely deployed in order to enhance security and performance in networking. However, as the communications over the TLS become increasingly common, the end-to-end channel model of the TLS undermines the efficacy of MBs. Existing solutions, such as `split TLS’ that intercepts TLS sessions, often introduce significant security risks by installing a custom root certificate or sharing a private key. Many studies have confirmed the vulnerabilities of combining the TLS with MBs, which include certificate validation failures, unwanted content modification, and using obsolete ciphersuites. To address the above issues, we introduce an MB-aware TLS protocol, dubbed maTLS, that allows MBs to participate in the TLS in a visible and accountable fashion. Every participating MB now splits a session into two segments with its own security parameters in collaboration with the two endpoints. However, the session is still secure as the maTLS protocol is designed to achieve the authentication of MBs, the audit of MBs’ operations, and the verification of security parameters of segments. We carry out testbed-based experiments to show that maTLS achieves the above security goals with marginal overhead. We also prove the security model of maTLS by using Tamarin, a security verification tool.

  16. TLS-N: Non-repudiation over TLS Enabling Ubiquitous Content Signing 2018 NDSS TLS
    Hubert Ritzdorf and Karl Wüst and Arthur Gervais and Guillaume Felley and Srdjan Capkun

    An internet user wanting to share observed content is typically restricted to primitive techniques such as screenshots, web caches or share button-like solutions. These acclaimed proofs, however, are either trivial to falsify or require trust in centralized entities (e.g., search engine caches).

    This motivates the need for a seamless and standardized internet-wide non-repudiation mechanism, allowing users to share data from news sources, social websites or financial data feeds in a provably secure manner.

    Additionally, blockchain oracles that enable data-rich smart contracts typically rely on a trusted third party (e.g., TLSNotary or Intel SGX). A decentralized method to transfer web-based content into a permissionless blockchain without additional trusted third party would allow for smart contract applications to flourish.

    In this work, we present TLS-N, the first TLS extension that provides secure non-repudiation and solves both of the mentioned challenges. TLS-N generates non-interactive proofs about the content of a TLS session that can be efficiently verified by third parties and blockchain based smart contracts. As such, TLS-N increases the accountability for content provided on the web and enables a practical and decentralized blockchain oracle for web content. TLS-N is compatible with TLS 1.3 and adds a minor overhead to a typical TLS session. When a proof is generated, parts of the TLS session (e.g., passwords, cookies) can be hidden for privacy reasons, while the remaining content can be verified.

    Practical demonstrations can be found at

  17. Verified Models and Reference Implementations for the TLS 1.3 Standard Candidate 2017 FormalVerification Oakland TLS
    Karthikeyan Bhargavan, Bruno Blanchet, and Nadim Kobeissi

    TLS 1.3 is the next version of the Transport Layer Security (TLS) protocol. Its clean-slate design is a reaction both to the increasing demand for low-latency HTTPS connections and to a series of recent high-profile attacks on TLS. The hope is that a fresh protocol with modern cryptography will prevent legacy problems, the danger is that it will expose new kinds of attacks, or reintroduce old flaws that were fixed in previous versions of TLS. After 18 drafts, the protocol is nearing completion, and the working group has appealed to researchers to analyze the protocol before publication. This paper responds by presenting a comprehensive analysis of the TLS 1.3 Draft-18 protocol. We seek to answer three questions that have not been fully addressed in previous work on TLS 1.3: (1) Does TLS 1.3 prevent well-known attacks on TLS 1.2, such as Logjam or the Triple Handshake, even if it is run in parallel with TLS 1.2? (2) Can we mechanically verify the computational security of TLS 1.3 under standard (strong) assumptions on its cryptographic primitives? (3) How can we extend the guarantees of the TLS 1.3 protocol to the details of its implementations? To answer these questions, we propose a methodology for developing verified symbolic and computational models of TLS 1.3 hand-in-hand with a high-assurance reference implementation of the protocol. We present symbolic ProVerif models for various intermediate versions of TLS 1.3 and evaluate them against a rich class of attacks to reconstruct both known and previously unpublished vulnerabilities that influenced the current design of the protocol. We present a computational CryptoVerif model for TLS 1.3 Draft-18 and prove its security. We present RefTLS, an interoperable implementation of TLS 1.0-1.3 and automatically analyze its protocol core by extracting a ProVerif model from its typed JavaScript code.

  18. Implementing and Proving the TLS 1.3 Record Layer 2017 FormalVerification Oakland TLS
    A. Delignat-Lavaud, C. Fournet, M. Kohlweiss, J. Protzenko, A. Rastogi, N. Swamy, S. Zanella-Beguelin, K. Bhargavan, J. Pan, and J. K. Zinzindohoue

    The record layer is the main bridge between TLS applications and internal sub-protocols. Its core functionality is an elaborate form of authenticated encryption: streams of messages for each sub-protocol (handshake, alert, and application data) are fragmented, multiplexed, and encrypted with optional padding to hide their lengths. Conversely, the sub-protocols may provide fresh keys or signal stream termination to the record layer. Compared to prior versions, TLS 1.3 discards obsolete schemes in favor of a common construction for Authenticated Encryption with Associated Data (AEAD), instantiated with algorithms such as AES-GCM and ChaCha20-Poly1305. It differs from TLS 1.2 in its use of padding, associated data and nonces. It also encrypts the content-type used to multiplex between sub-protocols. New protocol features such as early application data (0-RTT and 0.5-RTT) and late handshake messages require additional keys and a more general model of stateful encryption. We build and verify a reference implementation of the TLS record layer and its cryptographic algorithms in F*, a dependently typed language where security and functional guarantees can be specified as pre-and post-conditions. We reduce the high-level security of the record layer to cryptographic assumptions on its ciphers. Each step in the reduction is verified by typing an F* module, for each step that involves a cryptographic assumption, this module precisely captures the corresponding game. We first verify the functional correctness and injectivity properties of our implementations of one-time MAC algorithms (Poly1305 and GHASH) and provide a generic proof of their security given these two properties. We show the security of a generic AEAD construction built from any secure one-time MAC and PRF. We extend AEAD, first to stream encryption, then to length-hiding, multiplexed encryption. Finally, we build a security model of the record layer against an adversary that controls the TLS sub-protocols. We compute concrete security bounds for the AES_128_GCM, AES_256_GCM, and CHACHA20_POLY1305 ciphersuites, and derive recommended limits on sent data before re-keying. We plug our implementation of the record layer into the miTLS library, confirm that they interoperate with Chrome and Firefox, and report initial performance results. Combining our functional correctness, security, and experimental results, we conclude that the new TLS record layer (as described in RFCs and cryptographic standards) is provably secure, and we provide its first verified implementation.

  19. Removing Secrets from Android’s TLS 2018 Android Implementation NDSS TLS
    Jaeho Lee and Dan S. Wallach

    Cryptographic libraries that implement Transport Layer Security (TLS) have a responsibility to delete cryptographic keys once they’re no longer in use. Any key that’s left in memory can potentially be recovered through the actions of an attacker, up to and including the physical capture and forensic analysis of a device’s memory. This paper describes an analysis of the TLS library stack used in recent Android distributions, combining a C language core (BoringSSL) with multiple layers of Java code (Conscrypt, OkHttp, and Java Secure Sockets). We first conducted a black-box analysis of virtual machine images, allowing us to discover keys that might remain recoverable. After identifying several such keys, we subsequently pinpointed undesirable interactions across these layers, where the higherlevel use of BoringSSL’s reference counting features, from Java code, prevented BoringSSL from cleaning up its keys. This interaction poses a threat to all Android applications built on standard HTTPS libraries, exposing master secrets to memory disclosure attacks. We found all versions we investigated from Android 4 to the latest Android 8 are vulnerable, showing that this problem has been long overlooked. The Android Chrome application is proven to be particularly problematic. We suggest modest changes to the Android codebase to mitigate these issues, and have reported these to Google to help them patch the vulnerability in future Android systems.

  20. The Security Impact of HTTPS Interception 2017 Measurement NDSS TLS
    Z. Durumeric and Z. Ma and D. Springall and R. Barnes and N. Sullivan and E. Bursztein and M. Bailey and J. A. Halderman and V. Paxson

    As HTTPS deployment grows, middlebox and antivirus products are increasingly intercepting TLS connections to retain visibility into network traffic. In this work, we present a comprehensive study on the prevalence and impact of HTTPS interception. First, we show that web servers can detect interception by identifying a mismatch between the HTTP User-Agent header and TLS client behavior. We characterize the TLS handshakes of major browsers and popular interception products, which we use to build a set of heuristics to detect interception and identify the responsible product. We deploy these heuristics at three large network providers: (1) Mozilla Firefox update servers, (2) a set of popular e-commerce sites, and (3) the Cloudflare content distribution network. We find more than an order of magnitude more interception than previously estimated and with dramatic impact on connection security. To understand why security suffers, we investigate popular middleboxes and clientside security software, finding that nearly all reduce connection security and many introduce severe vulnerabilities. Drawing on our measurements, we conclude with a discussion on recent proposals to safely monitor HTTPS and recommendations for the security community.

  21. Measuring small subgroup attacks against Diffie-Hellman 2017 Attacks Diffie-Hellman IPSec Measurement NDSS TLS
    Luke Valenta and David Adrian and Antonio Sanso and Shaanan Cohney and Joshua Fried and Marcella Hastings and J. Alex Halderman and Nadia Heninger

    Several recent standards, including NIST SP 800- 56A and RFC 5114, advocate the use of “DSA” parameters for Diffie-Hellman key exchange. While it is possible to use such parameters securely, additional validation checks are necessary to prevent well-known and potentially devastating attacks. In this paper, we observe that many Diffie-Hellman implementations do not properly validate key exchange inputs. Combined with other protocol properties and implementation choices, this can radically decrease security. We measure the prevalence of these parameter choices in the wild for HTTPS, POP3S, SMTP with STARTTLS, SSH, IKEv1, and IKEv2, finding millions of hosts using DSA and other non-“safe” primes for Diffie-Hellman key exchange, many of them in combination with potentially vulnerable behaviors. We examine over 20 open-source cryptographic libraries and applications and observe that until January 2016, not a single one validated subgroup orders by default. We found feasible full or partial key recovery vulnerabilities in OpenSSL, the Exim mail server, the Unbound DNS client, and Amazon’s load balancer, as well as susceptibility to weaker attacks in many other applications.

  22. Indiscreet Logs: Diffie-Hellman Backdoors in TLS 2017 Backdoors DLP NDSS TLS
    Kristen Dorey and Nicholas Chang-Fong and Aleksander Essex

    Software implementations of discrete logarithm based cryptosystems over finite fields typically make the assumption that any domain parameters they encounter define cyclic groups for which the discrete logarithm problem is assumed to be hard. In this paper we explore this trust assumption and examine situations where it may not be justified. In particular we focus on groups for which the order is unknown and not easily determined, and explore the scenario in which the modulus is trapdoored to make computing discrete logarithms efficient for an entity with knowledge of the trapdoor, while simultaneously leaving its very existence as matter of speculation to everyone else.

    We conducted an investigation of discrete logarithm domain parameters in use across the Internet and discovered a multitude of instances of groups of unknown order in use in TLS and STARTTLS spanning numerous countries, organizations, and implementations. Although our disclosures resulted in a number of organizations taking down their suspicious parameters, none were able or willing to rule out the possibility that their parameters were trapdoors, and obtaining conclusive evidence in each case could be as hard as factoring an RSA modulus, highlighting a key feature of this attack method deniability.

  23. Lucky Thirteen: Breaking the TLS and DTLS Record Protocols 2013 Attacks Oakland TLS
    N. J. Al Fardan and K. G. Paterson

    The Transport Layer Security (TLS) protocol aims to provide confidentiality and integrity of data in transit across untrusted networks. TLS has become the de facto secure protocol of choice for Internet and mobile applications. DTLS is a variant of TLS that is growing in importance. In this paper, we present distinguishing and plaintext recovery attacks against TLS and DTLS. The attacks are based on a delicate timing analysis of decryption processing in the two protocols. We include experimental results demonstrating the feasibility of the attacks in realistic network environments for several different implementations of TLS and DTLS, including the leading OpenSSL implementations. We provide countermeasures for the attacks. Finally, we discuss the wider implications of our attacks for the cryptographic design used by TLS and DTLS.