, BoringSSL (Chrome) for Draft-18. By implementing Node's https interface, we are able to naturally integrate RefTLS within any Node or Electron application. We demonstrate the utility of this approach by integrating RefTLS into the Brave web browser, which is written in Electron. We are able to intercept all of Brave's HTTPS requests and reliably fulfill them through RefTLS. We benchmarked RefTLS against Node.js's default OpenSSL-based HTTPS stack when run against an OpenSSL peer over TLS 1.2. Our results are shown in Figure 12. In terms of computational overhead, RefTLS is two times slower than Node's native library, which is not surprising since RefTLS is written in JavaScript, whereas OpenSSL is written in C. In exchange for speed, RefTLS offers an early implementation of TLS 1.3 and a verified protocol core. Furthermore, in many application scenarios, Fewer libraries currently implement TLS 1.3, but RefTLS participated in the IETF Hackathon and achieved interoperability with other implementations of Draft-14. It now interoperates with NSS (Firefox) and

, ProVerif and Tamarin are both state-of-the-art protocol analyzers with different strengths. Tamarin can verify arbitrary compositions of protocols by relying on user-provided lemmas, whereas ProVerif is less expressive but offers more automation. In terms of protocol features, the Tamarin analysis covered PSK and ECDHE handshakes for 0-RTT and 1-RTT in Draft-10, but did not consider 0-RTT client certificate authentication or 0.5-RTT data. On the other hand, they do consider delayed (post-handshake) authentication, which we did not consider here. The main qualitative improvement in our verification results over theirs is that we consider a richer threat model that allows for downgrade attacks, and that we analyze TLS 1.3 in composition with previous versions of the protocol, whereas they verify TLS 1.3 in isolation. Our full ProVerif development consists of 1030 lines of ProVerif; including a generic library incorporating our threat model, Discussion and Related Work Symbolic Analysis of TLS 1.3. We symbolically analyzed a composite model of TLS 1.3 Draft18 with optional client authentication, PSK-based resumption, and PSK-based 0-RTT, running alongside TLS 1.2 against a rich threat model, and we established a series of security goals, vol.39

, We prove secrecy, forward secrecy with respect to the compromise of long-term keys, authentication, replay prevention (except for 0-RTT data), and existence of a unique channel identifier for TLS 1.3 draft-18. Our analysis considers PSK modes with and without DHE key exchange, with and without client authentication

M. Abdalla, P. Fouque, and D. Pointcheval, Password-based authenticated key exchange in the three-party setting, IEE Proceedings Information Security, vol.153, issue.1, pp.27-39, 2006.
URL : https://hal.archives-ouvertes.fr/hal-00918401

D. Adrian, K. Bhargavan, Z. Durumeric, P. Gaudry, M. Green et al.,

, Diffie-Hellman fails in practice, ACM SIGSAC Conference on Computer and Communications Security (CCS), pp.5-17, 2015.

M. R. Albrecht and K. G. Paterson, Lucky microseconds: A timing attack on Amazon's S2N implementation of TLS, EUROCRYPT, pp.622-643, 2016.

N. Alfardan, D. J. Bernstein, K. G. Paterson, B. Poettering, and J. C. Schuldt, On the security of RC4 in TLS, USENIX Security Symposium, pp.305-320, 2013.

N. J. Alfardan and K. G. Paterson, Lucky thirteen: Breaking the TLS and DTLS record protocols, 2013 IEEE Symposium on Security and Privacy (SP 2013), pp.526-540, 2013.

J. B. Almeida, M. Barbosa, G. Barthe, and F. Dupressoir, Verifiable Side-Channel Security of Cryptographic Implementations: Constant-Time MEE-CBC, Fast Software Encryption (FSE), pp.163-184, 2016.

M. Avalle, A. Pironti, R. Sisto, and D. Pozza, The Java SPI framework for security protocol implementation, Availability, Reliability and Security, pp.746-751, 2011.

N. Aviram, S. Schinzel, J. Somorovsky, N. Heninger, M. Dankel et al., DROWN: breaking TLS using SSLv2. In USENIX Security Symposium, pp.689-706, 2016.

G. Barthe, F. Dupressoir, B. Grégoire, C. Kunz, B. Schmidt et al., EasyCrypt: A tutorial, Foundations of Security Analysis and Design VII (FOSAD), vol.8604, pp.146-166, 2014.
URL : https://hal.archives-ouvertes.fr/hal-01114366

M. Bellare, New proofs for NMAC and HMAC: Security without collision-resistance, Advances in Cryptology (CRYPTO), pp.602-619, 2006.

M. Bellare, J. Kilian, and P. Rogaway, The security of the cipher block chaining message authentication code, Journal of Computer and System Sciences, vol.61, issue.3, pp.362-399, 2000.

M. Bellare and C. Namprempre, Authenticated encryption: Relations among notions and analysis of the generic composition paradigm, Advances in Cryptology-ASIACRYPT'00, pp.531-545, 2000.

M. Bellare and P. Rogaway, The security of triple encryption and a framework for code-based game-playing proofs, Advances in Cryptology (Eurocrypt), pp.409-426, 2006.

D. J. Bernstein, Curve25519: New Diffie-Hellman speed records, Public Key Cryptography (PKC), pp.207-228, 2006.

B. Beurdouche, K. Bhargavan, A. Delignat-lavaud, C. Fournet, M. Kohlweiss et al., A messy state of the union: taming the composite state machines of TLS, IEEE Symposium on Security & Privacy (Oakland), 2015.
URL : https://hal.archives-ouvertes.fr/hal-01114250

K. Bhargavan, C. Brzuska, C. Fournet, M. Green, M. Kohlweiss et al., Downgrade resilience in key-exchange protocols, IEEE Symposium on Security and Privacy (Oakland), pp.506-525, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01425962

K. Bhargavan, A. Delignat-lavaud, C. Fournet, A. Pironti, and P. Strub, Triple handshakes and cookie cutters: Breaking and fixing authentication over TLS, IEEE Symposium on Security & Privacy (Oakland), pp.98-113, 2014.
URL : https://hal.archives-ouvertes.fr/hal-01102259

K. Bhargavan, A. Delignat-lavaud, and S. Maffeis, Language-based defenses against untrusted browser origins, USENIX Security Symposium, pp.653-670, 2013.
URL : https://hal.archives-ouvertes.fr/hal-00863372

K. Bhargavan, A. Delignat-lavaud, and A. Pironti, Verified contributive channel bindings for compound authentication, Network and Distributed System Security Symposium (NDSS '15), 2015.
URL : https://hal.archives-ouvertes.fr/hal-01114248

K. Bhargavan, C. Fournet, R. Corin, and E. Z?linescu, Verified cryptographic implementations for TLS, vol.15, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00863381

K. Bhargavan, C. Fournet, and A. D. Gordon, Modular verification of security protocol code by typing, ACM Symposium on Principles of Programming Languages (POPL), pp.445-456, 2010.

K. Bhargavan, C. Fournet, A. D. Gordon, and S. Tse, Verified interoperable implementations of security protocols, ACM Transactions on Programming Languages and Systems, vol.31, issue.1, 2008.

K. Bhargavan, C. Fournet, M. Kohlweiss, A. Pironti, and P. Strub, Implementing TLS with verified cryptographic security, IEEE Symposium on Security & Privacy (Oakland), 2013.
URL : https://hal.archives-ouvertes.fr/hal-00863373

K. Bhargavan and G. Leurent, On the practical (in-)security of 64-bit block ciphers: Collision attacks on HTTP over TLS and OpenVPN, ACM SIGSAC Conference on Computer and Communications Security (CCS), pp.456-467, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01404208

K. Bhargavan and G. Leurent, Transcript collision attacks: Breaking authentication in TLS, IKE, and SSH, ISOC Network and Distributed System Security Symposium (NDSS), 2016.
URL : https://hal.archives-ouvertes.fr/hal-01244855

B. Blanchet, Computationally sound mechanized proofs of correspondence assertions, IEEE Computer Security Foundations Symposium (CSF), pp.97-111, 2007.

B. Blanchet, A computationally sound mechanized prover for security protocols, IEEE Transactions on Dependable and Secure Computing, vol.5, issue.4, pp.193-207, 2008.

B. Blanchet, Automatic verification of correspondences for security protocols, Journal of Computer Security, vol.17, issue.4, pp.363-434, 2009.

B. Blanchet, Automatically verified mechanized proof of one-encryption key exchange, 25th IEEE Computer Security Foundations Symposium (CSF'12), pp.325-339, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00863386

B. Blanchet, Security protocol verification: Symbolic and computational models, Principles of Security and Trust (POST), pp.3-29, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00863388

B. Blanchet, Modeling and verifying security protocols with the applied pi calculus and ProVerif, Foundations and Trends in Privacy and Security, vol.1, issue.1-2, pp.1-135, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01423760

D. Bleichenbacher, Chosen ciphertext attacks against protocols based on the RSA encryption standard PKCS# 1, Annual International Cryptology Conference, vol.1462, pp.1-12, 1998.

M. Bodin, A. Charguéraud, D. Filaretti, P. Gardner, S. Maffeis et al., A trusted mechanised javascript specification, ACM Symposium on the Principles of Programming Languages (POPL), pp.87-100, 2014.
URL : https://hal.archives-ouvertes.fr/hal-00910135

D. Cadé and B. Blanchet, Proved generation of implementations from computationally secure protocol specifications, Journal of Computer Security, vol.23, issue.3, pp.331-402, 2015.

S. Chaki and A. Datta, Aspier: An automated framework for verifying security protocol implementations, 22nd IEEE Computer Security Foundations Symposium, pp.172-185, 2009.

A. Chaudhuri, Flow: Abstract interpretation of javascript for type checking and beyond, ACM Workshop on Programming Languages and Analysis for Security (PLAS), 2016.

J. Coron, Y. Dodis, C. Malinaud, and P. Puniya, Merkle-Damgård revisited: How to construct a hash function, Advances in Cryptology (CRYPTO), pp.430-448, 2005.

V. Cortier, S. Kremer, and B. Warinschi, A survey of symbolic methods in computational analysis of cryptographic systems, Journal of Automated Reasoning, vol.46, issue.3-4, pp.225-259, 2011.
URL : https://hal.archives-ouvertes.fr/inria-00379776

C. Cremers, M. Horvat, S. Scott, and T. Van-der-merwe, Automated analysis and verification of TLS 1.3: 0-RTT, resumption and delayed authentication, IEEE Symposium on Security and Privacy (Oakland), pp.470-485, 2016.

I. B. Damgård, A design principle for hash functions, Advances in CryptologyCRYPTO'89, pp.416-427, 1989.

T. Dierks and E. Rescorla, The Transport Layer Security (TLS) Protocol Version 1.2. IETF RFC 5246, 2008.

Y. Dodis, T. Ristenpart, J. Steinberger, and S. Tessaro, To hash or not to hash again? (In)differentiability results for H 2 and HMAC, Advances in Cryptology (Crypto), pp.348-366, 2012.

D. Dolev and A. C. Yao, On the security of public key protocols, IEEE Transactions on Information Theory, vol.29, issue.2, pp.198-207, 1983.

B. Dowling, M. Fischlin, F. Günther, and D. Stebila, A cryptographic analysis of the TLS 1.3 handshake protocol candidates, ACM Conference on Computer and Communications Security (CCS), pp.1197-1210, 2015.

M. Fischlin and F. Günther, Multi-stage key exchange and the case of Google's QUIC protocol, ACM SIGSAC Conference on Computer and Communications Security (CCS), pp.1193-1204, 2014.

M. Fischlin, F. Günther, B. Schmidt, and B. Warinschi, Key confirmation in key exchange: A formal treatment and implications for TLS 1.3, IEEE Symposium on Security and Privacy (Oakland), pp.452-469, 2016.

D. Gillmor, Negotiated finite field Diffie-Hellman ephemeral parameters for Transport Layer Security (TLS), 2016.

S. Goldwasser, S. Micali, and R. Rivest, A digital signature scheme secure against adaptive chosen-message attacks, SIAM Journal of Computing, vol.17, issue.2, pp.281-308, 1988.

M. Hamburg, Ed448-Goldilocks, a new elliptic curve, Cryptology ePrint Archive, vol.625, 2015.

R. Hamilton, J. Iyengar, I. Swett, and A. Wilk, QUIC: A UDP-based multiplexed and secure transport, 2016.

K. E. Hickman, The SSL protocol, IETF Internet Draft, 1995.

T. Jager, F. Kohlar, S. Schäge, and J. Schwenk, On the security of TLS-DHE in the standard model, CRYPTO 2012, pp.273-293, 2012.

T. Jager, J. Schwenk, and J. Somorovsky, On the security of TLS 1.3 and QUIC against weaknesses in PKCS#1 v1.5 encryption, ACM SIGSAC Conference on Computer and Communications Security (CCS), pp.1185-1196, 2015.

N. Kobeissi, K. Bhargavan, and B. Blanchet, Automated verification for secure messaging protocols and their implementations: A symbolic and computational approach, IEEE European Symposium on Security and Privacy, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01575923

H. Krawczyk, Cryptographic extraction and key derivation: The HKDF scheme, Advances in Cryptology (CRYPTO), vol.6223, pp.631-648, 2010.

H. Krawczyk, A unilateral-to-mutual authentication compiler for key exchange (with applications to client authentication in tls 1.3), ACM SIGSAC Conference on Computer and Communications Security (CCS), pp.1438-1450, 2016.

H. Krawczyk, K. G. Paterson, and H. Wee, On the security of the TLS protocol: A systematic analysis, CRYPTO 2013, pp.429-448, 2013.

H. Krawczyk and H. Wee, The OPTLS protocol and TLS 1.3, IEEE European Symposium on Security & Privacy (Euro S&P), 0978.
URL : https://hal.archives-ouvertes.fr/hal-01378195

R. Küsters, T. Truderung, and J. Graf, A framework for the cryptographic verification of Java-like programs, IEEE Computer Security Foundations Symposium (CSF), pp.198-212, 2012.

A. Langley, M. Hamburg, and S. Turner, Elliptic curves for security, IRTF RFC, vol.7748, 2016.

X. Li, J. Xu, Z. Zhang, D. Feng, and H. Hu, Multiple handshakes security of TLS 1.3 candidates, IEEE Symposium on Security and Privacy (Oakland), pp.486-505, 2016.

R. Lychev, S. Jero, A. Boldyreva, and C. Nita-rotaru, How secure and quick is QUIC? provable security and performance analyses, IEEE Symposium on Security & Privacy (Oakland), pp.214-231, 2015.

U. Maurer and B. Tackmann, On the soundness of authenticate-then-encrypt: formalizing the malleability of symmetric encryption, ACM SIGSAC Conference on Computer and Communications Security (CCS), pp.505-515, 2010.

N. Mavrogiannopoulos, F. Vercauteren, V. Velichkov, and B. Preneel, A cross-protocol attack on the TLS protocol, ACM CCS, 2012.

C. Meyer, J. Somorovsky, E. Weiss, J. Schwenk, S. Schinzel et al., Revisiting SSL/TLS implementations: New Bleichenbacher side channels and attacks, 23rd USENIX Security Symposium, pp.733-748, 2014.

B. Möller, T. Duong, and K. Kotowicz, This POODLE bites: exploiting the SSL 3.0 fallback, 2014.

N. Fips, , 2009.

T. Okamoto and D. Pointcheval, The gap-problems: a new class of problems for the security of cryptographic schemes, Practice and Theory in Public Key Cryptography (PKC), pp.104-118, 2001.

K. G. Paterson, T. Ristenpart, and T. Shrimpton, Tag size does matter: Attacks and proofs for the TLS record protocol, ASIACRYPT, pp.372-389, 2011.

K. G. Paterson and T. Van-der-merwe, Reactive and proactive standardisation of TLS, Security Standardisation Research (SSR), pp.160-186, 2016.

M. Ray, A. Pironti, A. Langley, K. Bhargavan, and A. Delignat-lavaud, Transport Layer Security (TLS) session hash and extended master secret extension

E. Rescorla.-0-rtt and A. , , 2015.

E. Rescorla, PR#875: Additional Derive-Secret stage, 2017.

E. Rescorla, M. Ray, S. Dispensa, and N. Oskov, TLS renegotiation indication extension, IETF RFC, vol.5746, 2010.

B. Schmidt, S. Meier, C. Cremers, and D. Basin, Automated analysis of Diffie-Hellman protocols and advanced security properties, IEEE Computer Security Foundations Symposium (CSF), pp.78-94, 2012.

V. Shoup, Sequences of games: a tool for taming complexity in security proofs. IACR Cryptology ePrint Archive, 2004.

D. Stefan, Espectro project description, 2016.

N. Swamy, C. Hri?cu, C. Keller, A. Rastogi, A. Delignat-lavaud et al., Dependent types and multi-monadic effects in F*, ACM Symposium on Principles of Programming Languages (POPL), pp.256-270, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01265793

M. Vanhoef and F. Piessens, All your biases belong to us: Breaking RC4 in WPA-TKIP and TLS, USENIX Security Symposium, pp.97-112, 2015.

D. Wagner and B. Schneier, Analysis of the SSL 3.0 protocol, USENIX Electronic Commerce, 1996.

T. Y. Woo and S. S. Lam, A semantic model for authentication protocols, Proceedings IEEE Symposium on Research in Security and Privacy, pp.178-194, 1993.