Article

FLEXTLS: a tool for testing TLS implementations

Authors:

Benjamin Beurdouche,

Antoine Delignat-Lavaud,

Nadim Kobeissi,

Alfredo Pironti,

Karthikeyan BhargavanAuthors Info & Claims

WOOT'15: Proceedings of the 9th USENIX Conference on Offensive Technologies

Page 1

Published: 10 August 2015 Publication History

Publisher Site

Abstract

We present FLEXTLS, a tool for rapidly prototyping and testing implementations of the Transport Layer Security (TLS) protocol. FLEXTLS is built upon MITLS, a verified implementation of TLS, and hence protocol scenarios written in FLEXTLS can benefit from robust libraries for messaging and cryptography. Conversely, attack scripts in FLEXTLS can be used to evaluate and communicate the impact of new protocol vulnerabilities.

FLEXTLS was used to discover recent attacks on TLS implementations, such as SKIP and FREAK, as well as to program the first proof-of-concept demos for FREAK and Logjam. It is also being used to experiment with proposed designs of the upcoming version 1.3 of TLS. Our goal is to create a common platform where protocol analysts and practitioners can easily test TLS implementations and share protocol designs, attacks or proofs.

References

[1]

D. Adrian, K. Bhargavan, Z. Durumeric, P. Gaudry, M. Green, J.A. Halderman, N. Heninger, D. Springall, E. Thomé, L. Valenta, B. VanderSloot, E. Wustrow, S. Zanella-Béguelin, and P. Zimmermann. Imperfect Forward Secrecy: How Diffie-Hellman Fails in Practice. https://weakdh.org, May 2015.

Google Scholar

[2]

B. Beurdouche, K. Bhargavan, A. Delignat-Lavaud, C. Fournet, M. Kohlweiss, A. Pironti, P-Y Strub, and J-K Zinzindohoué. A messy state of the union: Taming the composite state machines of TLS. In IEEE S&P (Oakland), 2015.

Google Scholar

[3]

K. Bhargavan, A. Delignat-Lavaud, C. Fournet, A. Pironti, and P-Y. Strub. Triple handshakes and cookie cutters: Breaking and fixing authentication over TLS. In IEEE S&P (Oakland), 2014.

Crossref

Google Scholar

[4]

K. Bhargavan, A. Delignat-Lavaud, A. Pironti, A. Langley, and M. Ray. Transport Layer Security (TLS) Session Hash and Extended Master Secret Extension. IETF Internet Draft, 2014.

Google Scholar

[5]

K. Bhargavan, C. Fournet, M. Kohlweiss, A. Pironti, and P-Y Strub. Implementing TLS with verified cryptographic security. In IEEE S&P (Oakland), 2013.

Crossref

Google Scholar

[6]

K. Bhargavan, C. Fournet, M. Kohlweiss, A. Pironti, P-Y Strub, and S. Zanella-Béguelin. Proving the TLS handshake secure (as it is). In CRYPTO, 2014.

Google Scholar

[7]

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

Google Scholar

[8]

D.K. Gillmor. Negotiated finite field Diffie-Hellman ephemeral parameters for TLS. IETF Internet Draft, May 2015.

Google Scholar

[9]

M. Kikuchi. How I discovered CCS Injection Vulnerability (CVE-2014-0224), June 2014.

Google Scholar

[10]

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

Google Scholar

[11]

A. Langley, N. Modadugu, and B. Moeller. Transport layer security (TLS) false start. IETF Internet Draft, 2015.

Google Scholar

[12]

E. Rescorla. The Transport Layer Security (TLS) Protocol Version 1.3. Internet Draft, 2015.

Google Scholar

Cited By

View all

Swierzy BBoes FPohl TBungartz CMeier M(2024)SoK: Automated Software Testing for TLS LibrariesProceedings of the 19th International Conference on Availability, Reliability and Security10.1145/3664476.3670871(1-12)Online publication date: 30-Jul-2024
https://dl.acm.org/doi/10.1145/3664476.3670871
Ramananandro TDelignat-Lavaud AFournet CSwamy NChajed TKobeissi NProtzenko JHeninger NTraynor P(2019)EverparseProceedings of the 28th USENIX Conference on Security Symposium10.5555/3361338.3361440(1465-1482)Online publication date: 14-Aug-2019
https://dl.acm.org/doi/10.5555/3361338.3361440
Simos DBozic JGarn BLeithner MDuan FKleine KLei YWotawa F(2019)Testing TLS using planning-based combinatorial methods and execution frameworkSoftware Quality Journal10.1007/s11219-018-9412-z27:2(703-729)Online publication date: 1-Jun-2019
https://dl.acm.org/doi/10.1007/s11219-018-9412-z
Show More Cited By

Recommendations

Cryptanalysis of a new protocol of wide use for email with perfect forward secrecy

This paper considers security analysis of a cross-realm client-to-client password-authenticated key exchange C2C-PAKE protocol with indirect communication structure that was proposed for secure email. The protocol does not need any public key ...
Resource Fairness and Composability of Cryptographic Protocols

We introduce the notion of resource-fair protocols. Informally, this property states that if one party learns the output of the protocol, then so can all other parties, as long as they expend roughly the same amount of resources. As opposed to ...
Denial-of-service resistance in key establishment

Denial of Service (DoS) attacks are an increasing problem for network connected systems. Key establishment protocols are applications that are particularly vulnerable to DoS attack as they are typically required to perform computationally expensive ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

WOOT'15: Proceedings of the 9th USENIX Conference on Offensive Technologies

August 2015

18 pages

Editors:
Aurélien Francillon
EURECOM
,
Thomas Ptacek
Starfighter

Publisher

USENIX Association

United States

Publication History

Published: 10 August 2015

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

4
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 12 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Swierzy BBoes FPohl TBungartz CMeier M(2024)SoK: Automated Software Testing for TLS LibrariesProceedings of the 19th International Conference on Availability, Reliability and Security10.1145/3664476.3670871(1-12)Online publication date: 30-Jul-2024
https://dl.acm.org/doi/10.1145/3664476.3670871
Ramananandro TDelignat-Lavaud AFournet CSwamy NChajed TKobeissi NProtzenko JHeninger NTraynor P(2019)EverparseProceedings of the 28th USENIX Conference on Security Symposium10.5555/3361338.3361440(1465-1482)Online publication date: 14-Aug-2019
https://dl.acm.org/doi/10.5555/3361338.3361440
Simos DBozic JGarn BLeithner MDuan FKleine KLei YWotawa F(2019)Testing TLS using planning-based combinatorial methods and execution frameworkSoftware Quality Journal10.1007/s11219-018-9412-z27:2(703-729)Online publication date: 1-Jun-2019
https://dl.acm.org/doi/10.1007/s11219-018-9412-z
Somorovsky JWeippl EKatzenbeisser SKruegel CMyers AHalevi S(2016)Systematic Fuzzing and Testing of TLS LibrariesProceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security10.1145/2976749.2978411(1492-1504)Online publication date: 24-Oct-2016
https://dl.acm.org/doi/10.1145/2976749.2978411

Abstract

References

Cited By

Recommendations

Cryptanalysis of a new protocol of wide use for email with perfect forward secrecy

Resource Fairness and Composability of Cryptographic Protocols

Denial-of-service resistance in key establishment

Comments

Information

Published In

Publisher

Publication History

Author Tags

Qualifiers

Contributors

Other Metrics

Bibliometrics

Article Metrics

Other Metrics

Citations

Cited By

View options

Figures

Other

Share

Share this Publication link

Share on social media

Affiliations