Karthikeyan Bhargavan
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.
- 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. Google Scholar
Digital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- B. Blanchet. An efficient cryptographic protocol verifier based on Prolog rules. In 14th IEEE Computer Security Foundations Workshop (CSFW'01), pages 82--96, 2001. Google ScholarDigital Library
- B. Blanchet. A computationally sound mechanized prover for security protocols. In IEEE Symposium on Security and Privacy, pages 140--154, 2006. Google ScholarDigital Library
- B. Blanchet and D. Pointcheval. Automated security proofs with sequences of games. In 26th Annual International Cryptology Conference (CRYPTO'06), pages 537--554, 2006.Google ScholarDigital Library
- 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. Google ScholarDigital Library
- S. Chaki and A. Datta. Automated verification of security protocol implementations. Technical Report CMU-Cylab-08-002, Carnegie Mellon University, 2008.Google Scholar
- T. Dierks and C. Allen. The TLS protocol version 1.0. RFC 2246, IETF, 1999. Google ScholarDigital Library
- T. Dierks and E. Rescorla. The Transport Layer Security (TLS) protocol version 1.1. RFC 4346, IETF, 2006.Google Scholar
- T. Dierks and E. Rescorla. The Transport Layer Security (TLS) protocol version 1.2. Internet Draft, IETF, 2008.Google ScholarDigital Library
- D. Dolev and A. Yao. On the security of public key protocols. IEEE Transactions on Information Theory, IT--29(2):198--208, 1983.Google ScholarDigital Library
- 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. Google ScholarDigital Library
- A. Frier, P. Karlton, and P. Kocher. The SSL protocol version 3.0. Internet Draft, IETF, 1996.Google Scholar
- 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. Google ScholarDigital Library
- 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.Google ScholarDigital Library
- 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. Google ScholarDigital Library
- K. E. Hickman. The SSL protocol. Draft specification, Netscape, 1995.Google Scholar
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- A. Kamil and G. Lowe. Analysing TLS in the strand spaces model. Technical report, Oxford University Computing Laboratory, 2008.Google Scholar
- 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.Google ScholarCross Ref
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- P. Morrissey, N. Smart, and B. Warinschi. A modular security analysis of the TLS handshake protocol. Cryptology ePrint Archive: Report 2008/236, 2008.Google Scholar
- R. Needham and M. Schroeder. Using encryption for authentication in large networks of computers. Communications of the ACM, 21(12): 993--999, 1978. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- L. C. Paulson. Inductive analysis of the Internet protocol TLS. ACM Transactions on Information and System Security, 2(3):332--351, 1999. Google ScholarDigital Library
- 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.Google ScholarDigital Library
- D. Syme. F#, 2005. http://research.microsoft.com/fsharp/.Google Scholar
- 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. Google ScholarDigital Library
- 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.Google ScholarDigital Library
Index Terms
- Cryptographically verified implementations for TLS
Recommendations
Verified Cryptographic Implementations for TLS
Special Issue on Computer and Communications SecurityWe 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 securityIn 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