research-article

Cryptographically verified implementations for TLS

Authors:

Karthikeyan Bhargavan,

Cédric Fournet,

Eugen ZalinescuAuthors Info & Claims

CCS '08: Proceedings of the 15th ACM conference on Computer and communications security

Pages 459 - 468

https://doi.org/10.1145/1455770.1455828

Published: 27 October 2008 Publication History

Abstract

We intend to narrow the gap between concrete implementations of cryptographic protocols and their verified models. We develop and verify a small functional implementation of the Transport Layer Security protocol (TLS 1.0). We make use of the same executable code for interoperability testing against mainstream implementations, for automated symbolic cryptographic verification, and for automated computational cryptographic verification. We rely on a combination of recent tools, and we also develop a new tool for extracting computational models from executable code. We obtain strong security guarantees for TLS as used in typical deployments.

References

[1]

M. Abadi and C. Fournet. Mobile values, new names, and secure communication. In 28th ACM Symposium on Principles of Programming Languages (POPL'01), pages 104--115, 2001.

Digital Library

[2]

M. Bellare and P. Rogaway. Random oracles are practical: A paradigm for designing efficient protocols. In 1st ACM Conference on Computer and Communications Security (CCS'93), pages 62--73, 1993.

Digital Library

[3]

K. Bhargavan, C. Fournet, A. D. Gordon, and S. Tse. Verified interoperable implementations of security protocols. In 19th IEEE Computer Security Foundations Workshop (CSFW'06), pages 139--152, 2006.

Digital Library

[4]

B. Blanchet. An efficient cryptographic protocol verifier based on Prolog rules. In 14th IEEE Computer Security Foundations Workshop (CSFW'01), pages 82--96, 2001.

Digital Library

[5]

B. Blanchet. A computationally sound mechanized prover for security protocols. In IEEE Symposium on Security and Privacy, pages 140--154, 2006.

Digital Library

[6]

B. Blanchet and D. Pointcheval. Automated security proofs with sequences of games. In 26th Annual International Cryptology Conference (CRYPTO'06), pages 537--554, 2006.

Digital Library

[7]

D. Bleichenbacher. Chosen ciphertext attacks against protocols based on rsa encryption standard PKCS #1. In 18th Annual Cryptology Conference (CRYPTO'98), pages 1--12, 1998.

Digital Library

[8]

S. Chaki and A. Datta. Automated verification of security protocol implementations. Technical Report CMU-Cylab-08-002, Carnegie Mellon University, 2008.

[9]

T. Dierks and C. Allen. The TLS protocol version 1.0. RFC 2246, IETF, 1999.

Digital Library

[10]

T. Dierks and E. Rescorla. The Transport Layer Security (TLS) protocol version 1.1. RFC 4346, IETF, 2006.

[11]

T. Dierks and E. Rescorla. The Transport Layer Security (TLS) protocol version 1.2. Internet Draft, IETF, 2008.

Digital Library

[12]

D. Dolev and A. Yao. On the security of public key protocols. IEEE Transactions on Information Theory, IT--29(2):198--208, 1983.

Digital Library

[13]

P.-A. Fouque, D. Pointcheval, and S. Zimmer. HMAC is a randomness extractor and applications to TLS. In ACM Symposium on Information, Computer and Communications Security (ASIACCS'08), pages 21--32, 2008.

Digital Library

[14]

A. Frier, P. Karlton, and P. Kocher. The SSL protocol version 3.0. Internet Draft, IETF, 1996.

[15]

S. Gajek, M. Manulis, A.-R. Sadeghi, and J. Schwenk. Provably secure browser-based user-aware mutual authentication over TLS. In ACM Symposium on Information, Computer and Communications Security (ASIACCS'08), pages 300--311, 2008.

Digital Library

[16]

J. Goubault-Larrecq and F. Parrennes. Cryptographic protocol analysis on real C code. In 6th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'05), pages 363--379, 2005.

Digital Library

[17]

C. He, M. Sundararajan, A. Datta, A. Derek, and J. C. Mitchell. A modular correctness proof of IEEE 802.11i and TLS. In 12th ACM conference on Computer and Communications Security (CCS'05), pages 2--15, 2005.

Digital Library

[18]

K. E. Hickman. The SSL protocol. Draft specification, Netscape, 1995.

[19]

J. Jonsson and J. B. S. Kaliski. On the security of RSA encryption in TLS. In 22nd Annual International Cryptology Conference (CRYPTO'02), pages 127--142, 2002.

Digital Library

[20]

J. Jürjens. Security analysis of crypto-based java programs using automated theorem provers. In 21st IEEE/ACM International Conference on Automated Software Engineering (ASE'06), pages 167--176, 2006.

Digital Library

[21]

A. Kamil and G. Lowe. Analysing TLS in the strand spaces model. Technical report, Oxford University Computing Laboratory, 2008.

[22]

V. Klima, O. Pokorny, and T. Rosa. Attacking RSA-based sessions in SSL/TLS. In Cryptographic Hardware and Embedded Systems (CHES'03), pages 426--440, 2003.

[23]

H. Krawczyk. The order of encryption and authentication for protecting communications (or: How secure is SSL?). In 21st Annual International Cryptology Conference (CRYPTO'01), pages 310--331, 2001.

Digital Library

[24]

J. C. Mitchell, V. Shmatikov, and U. Stern. Finite-state analysis of SSL 3.0. In 7th conference on USENIX Security Symposium (SSYM'98), pages 201--216, 1998.

Digital Library

[25]

P. Morrissey, N. Smart, and B. Warinschi. A modular security analysis of the TLS handshake protocol. Cryptology ePrint Archive: Report 2008/236, 2008.

[26]

R. Needham and M. Schroeder. Using encryption for authentication in large networks of computers. Communications of the ACM, 21(12): 993--999, 1978.

Digital Library

[27]

K. Ogata and K. Futatsugi. Equational approach to formal analysis of TLS. In 25th IEEE International Conference on Distributed Computing Systems (ICSCS'05), pages 795--804, 2005.

Digital Library

[28]

L. C. Paulson. Inductive analysis of the Internet protocol TLS. ACM Transactions on Information and System Security, 2(3):332--351, 1999.

Digital Library

[29]

D. H. Phan and D. Pointcheval. About the security of ciphers (semantic security and pseudo-random permutations). In Selected Areas in Cryptography, pages 182--197, 2004.

Digital Library

[30]

D. Syme. F#, 2005. http://research.microsoft.com/fsharp/.

[31]

D. Wagner and B. Schneier. Analysis of the SSL 3.0 protocol. In 2nd USENIX Workshop on Electronic Commerce (WOEC'96), pages 29--40, 1996.

Digital Library

[32]

A. K. L. Yau, K. G. Paterson, and C. J. Mitchell. Padding oracle attacks on CBC-mode encryption with secret and random IVs. In Fast Software Encryption, pages 299--319, 2005.

Digital Library

Cited By

Tran DOgata KEscobar SAkleylek SOtmani A(2024)Formal Analysis of Post-Quantum Hybrid Key Exchange SSH Transport Layer ProtocolIEEE Access10.1109/ACCESS.2023.334791412(1672-1687)Online publication date: 2024
https://doi.org/10.1109/ACCESS.2023.3347914
Nasrabadi FKünnemann RNemati HMeng WJensen CCremers CKirda E(2023)CryptoBap: A Binary Analysis Platform for Cryptographic ProtocolsProceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security10.1145/3576915.3623090(1362-1376)Online publication date: 15-Nov-2023
https://dl.acm.org/doi/10.1145/3576915.3623090
Feng HGuan JLi HPan XZhao Z(2023)FIDO Gets Verified: A Formal Analysis of the Universal Authentication Framework ProtocolIEEE Transactions on Dependable and Secure Computing10.1109/TDSC.2022.321725920:5(4291-4310)Online publication date: 1-Sep-2023
https://doi.org/10.1109/TDSC.2022.3217259
Show More Cited By

Index Terms

Cryptographically verified implementations for TLS

Recommendations

Verified Cryptographic Implementations for TLS
Special Issue on Computer and Communications Security

We narrow the gap between concrete implementations of cryptographic protocols and their verified models. We develop and verify a small functional implementation of the Transport Layer Security protocol (TLS 1.0). We make use of the same executable code ...
Authenticated Confidential Channel Establishment and the Security of TLS-DHE

Transport Layer Security (TLS) is the most important cryptographic protocol in use today. However, finding a cryptographic security proof for the complete, unaltered protocol has proven to be a challenging task. We give the first such proof in the ...
Provably secure password-based authentication in TLS
ASIACCS '06: Proceedings of the 2006 ACM Symposium on Information, computer and communications security

In this paper, we show how to design an efficient, provably secure password-based authenticated key exchange mechanism specifically for the TLS (Transport Layer Security) protocol. The goal is to provide a technique that allows users to employ (short) ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

CCS '08: Proceedings of the 15th ACM conference on Computer and communications security

October 2008

590 pages

ISBN:9781595938107

DOI:10.1145/1455770

General Chair:
Peng Ning
North Carolina State University, USA
,
Program Chairs:
Paul Syverson
Naval Research Laboratory, USA
,
Somesh Jha
University of Wisconsin, USA

Copyright © 2008 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 27 October 2008

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

CCS08

Sponsor:

CCS08: 15th ACM Conference on Computer and Communications Security 2008

October 27 - 31, 2008

Virginia, Alexandria, USA

Acceptance Rates

CCS '08 Paper Acceptance Rate 51 of 280 submissions, 18%;

Overall Acceptance Rate 1,261 of 6,999 submissions, 18%

Upcoming Conference

CCS '25

Sponsor:
sigsac

ACM SIGSAC Conference on Computer and Communications Security

October 13 - 17, 2025

Taipei , Taiwan

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

68
Total Citations
View Citations
984
Total Downloads

Downloads (Last 12 months)20
Downloads (Last 6 weeks)1

Reflects downloads up to 17 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Tran DOgata KEscobar SAkleylek SOtmani A(2024)Formal Analysis of Post-Quantum Hybrid Key Exchange SSH Transport Layer ProtocolIEEE Access10.1109/ACCESS.2023.334791412(1672-1687)Online publication date: 2024
https://doi.org/10.1109/ACCESS.2023.3347914
Nasrabadi FKünnemann RNemati HMeng WJensen CCremers CKirda E(2023)CryptoBap: A Binary Analysis Platform for Cryptographic ProtocolsProceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security10.1145/3576915.3623090(1362-1376)Online publication date: 15-Nov-2023
https://dl.acm.org/doi/10.1145/3576915.3623090
Feng HGuan JLi HPan XZhao Z(2023)FIDO Gets Verified: A Formal Analysis of the Universal Authentication Framework ProtocolIEEE Transactions on Dependable and Secure Computing10.1109/TDSC.2022.321725920:5(4291-4310)Online publication date: 1-Sep-2023
https://doi.org/10.1109/TDSC.2022.3217259
Tran DOgata K(2022)Formal verification of TLS 1.2 by automatically generating proof scoresComputers and Security10.1016/j.cose.2022.102909123:COnline publication date: 1-Dec-2022
https://dl.acm.org/doi/10.1016/j.cose.2022.102909
Sivelle CDebbah LPuys MLafourcade PFranco-Rondisson T(2022)Automatic Implementations Synthesis of Secure Protocols and Attacks from Abstract ModelsSecure IT Systems10.1007/978-3-031-22295-5_13(234-252)Online publication date: 30-Nov-2022
https://dl.acm.org/doi/10.1007/978-3-031-22295-5_13
Schwenk JSchwenk J(2022)Transport Layer SecurityGuide to Internet Cryptography10.1007/978-3-031-19439-9_10(201-242)Online publication date: 26-Nov-2022
https://doi.org/10.1007/978-3-031-19439-9_10
Hofer-Schmitz K(2021)A Formal Analysis of EnOcean’s Teach-in and AuthenticationProceedings of the 16th International Conference on Availability, Reliability and Security10.1145/3465481.3470097(1-8)Online publication date: 17-Aug-2021
https://dl.acm.org/doi/10.1145/3465481.3470097
Delignat-Lavaud AFournet CParno BProtzenko JRamananandro TBosamiya JLallemand JRakotonirina IZhou Y(2021)A Security Model and Fully Verified Implementation for the IETF QUIC Record Layer2021 IEEE Symposium on Security and Privacy (SP)10.1109/SP40001.2021.00039(1162-1178)Online publication date: May-2021
https://doi.org/10.1109/SP40001.2021.00039
He XLiu QChen SHuang CWang DMeng B(2020)Analyzing Security Protocol Web Implementations Based on Model Extraction With Applied PI CalculusIEEE Access10.1109/ACCESS.2020.29716158(26623-26636)Online publication date: 2020
https://doi.org/10.1109/ACCESS.2020.2971615
Babenko LPisarev I(2020)Translation of Cryptographic Protocols Description from Alice-Bob Format to CAS+ Specification LanguageProceedings of the Fourth International Scientific Conference “Intelligent Information Technologies for Industry” (IITI’19)10.1007/978-3-030-50097-9_32(309-318)Online publication date: 23-Jun-2020
https://doi.org/10.1007/978-3-030-50097-9_32
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents