{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,21]],"date-time":"2026-07-21T13:03:07Z","timestamp":1784638987539,"version":"3.55.0"},"reference-count":43,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2012,3,1]],"date-time":"2012-03-01T00:00:00Z","timestamp":1330560000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Inf. Syst. Secur."],"published-print":{"date-parts":[[2012,3]]},"abstract":"<jats:p>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 for interoperability testing against mainstream implementations for automated symbolic cryptographic verification and automated computational cryptographic verification. We rely on a combination of recent tools and also develop a new tool for extracting computational models from executable code. We obtain strong security guarantees for TLS as used in typical deployments.<\/jats:p>","DOI":"10.1145\/2133375.2133378","type":"journal-article","created":{"date-parts":[[2012,3,27]],"date-time":"2012-03-27T15:17:31Z","timestamp":1332861451000},"page":"1-32","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":31,"title":["Verified Cryptographic Implementations for TLS"],"prefix":"10.1145","volume":"15","author":[{"given":"Karthikeyan","family":"Bhargavan","sequence":"first","affiliation":[{"name":"Microsoft Research, Cambridge"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"C\u00e9dric","family":"Fournet","sequence":"additional","affiliation":[{"name":"Microsoft Research, Cambridge"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ricardo","family":"Corin","sequence":"additional","affiliation":[{"name":"Microsoft Research-INRIA Joint Centre, Orsay"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Eugen","family":"Z\u0103linescu","sequence":"additional","affiliation":[{"name":"Microsoft Research-INRIA Joint Centre, Orsay"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2012,3]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/360204.360213"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/1180405.1180450"},{"key":"e_1_2_1_3_1","volume-title":"Proceedings of the 16th Annual Cryptology Conference on Advances in Cryptology (CRYPTO\u201996)","author":"Bellare M.","unstructured":"Bellare , M. , Canetti , R. , and Krawczyk , H . 1996. Keying hash functions for message authentication . In Proceedings of the 16th Annual Cryptology Conference on Advances in Cryptology (CRYPTO\u201996) . Springer, 1--15. Bellare, M., Canetti, R., and Krawczyk, H. 1996. Keying hash functions for message authentication. In Proceedings of the 16th Annual Cryptology Conference on Advances in Cryptology (CRYPTO\u201996). Springer, 1--15."},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/168588.168596"},{"key":"e_1_2_1_5_1","unstructured":"Bhargavan K. Corin R. Fournet C. and Z\u0103linescu E. 2009. Automated computational verification for cryptographic protocol implementations. MSR-INRIA Tech. rep. http:\/\/msr-inria.inria.fr\/projects\/sec\/fs2cv. Bhargavan K. Corin R. Fournet C. and Z\u0103linescu E. 2009. Automated computational verification for cryptographic protocol implementations. MSR-INRIA Tech. rep. http:\/\/msr-inria.inria.fr\/projects\/sec\/fs2cv."},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSFW.2006.32"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.5555\/872752.873511"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2007.16"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/TDSC.2007.1005"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/11818175_32"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1368310.1368326"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.5555\/646763.706320"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2009.20"},{"key":"e_1_2_1_14_1","unstructured":"Cisco. 2007. SSL\/TLS certificate and SSH public key validation vulnerability. http:\/\/www.cisco.com\/warp\/public\/707\/cisco-sa-20070118-certs.shtml. Cisco . 2007. SSL\/TLS certificate and SSH public key validation vulnerability. http:\/\/www.cisco.com\/warp\/public\/707\/cisco-sa-20070118-certs.shtml."},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/11787006_22"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSFW.2006.9"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/967900.968063"},{"key":"e_1_2_1_18_1","doi-asserted-by":"crossref","unstructured":"Dierks T. and Allen C. 1999. The TLS protocol version 1.0. Dierks T. and Allen C. 1999. The TLS protocol version 1.0.","DOI":"10.17487\/rfc2246"},{"key":"e_1_2_1_19_1","doi-asserted-by":"crossref","unstructured":"Dierks T. and Rescorla E. 2006. The Transport layer security (TLS) protocol version 1.1. Dierks T. and Rescorla E. 2006. The Transport layer security (TLS) protocol version 1.1.","DOI":"10.17487\/rfc4346"},{"key":"e_1_2_1_20_1","doi-asserted-by":"crossref","unstructured":"Dierks T. and Rescorla E. 2008. The Transport layer security (TLS) protocol version 1.2. Dierks T. and Rescorla E. 2008. The Transport layer security (TLS) protocol version 1.2.","DOI":"10.17487\/rfc5246"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/TIT.1983.1056650"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/1368310.1368317"},{"key":"e_1_2_1_24_1","unstructured":"Frier A. O. Karlton P. and Kocher P. C. 1996. The SSL protocol version 3.0. Internet Draft IETF. Frier A. O. Karlton P. and Kocher P. C. 1996. The SSL protocol version 3.0. Internet Draft IETF."},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1368310.1368354"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30579-8_24"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/1102120.1102124"},{"key":"e_1_2_1_28_1","unstructured":"Hickman K. E. 1995. The SSL protocol. Draft specification Netscape. Hickman K. E. 1995. The SSL protocol. Draft specification Netscape."},{"key":"e_1_2_1_29_1","volume-title":"Proceedings of the 22nd Annual International Cryptology Conference (CRYPTO\u201902)","volume":"2442","author":"Jonsson J.","unstructured":"Jonsson , J. and Kaliski , J. B. S. 2002. On the security of RSA encryption in TLS . In Proceedings of the 22nd Annual International Cryptology Conference (CRYPTO\u201902) . Lecture Notes in Computer Science , vol. 2442 . Springer, 127--142. Jonsson, J. and Kaliski, J. B. S. 2002. On the security of RSA encryption in TLS. In Proceedings of the 22nd Annual International Cryptology Conference (CRYPTO\u201902). Lecture Notes in Computer Science, vol. 2442. Springer, 127--142."},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2006.60"},{"key":"e_1_2_1_31_1","unstructured":"Kamil A. and Lowe G. 2008. Analysing TLS in the strand spaces model. Tech. rep. Oxford University Computing Laboratory. Kamil A. and Lowe G. 2008. Analysing TLS in the strand spaces model. Tech. rep. Oxford University Computing Laboratory."},{"key":"e_1_2_1_32_1","volume-title":"Proceedings of the Workshop on Cryptographic Hardware and Embedded Systems (CHES\u201903)","volume":"2779","author":"Klima V.","unstructured":"Klima , V. , Pokorny , O. , and Rosa , T . 2003. Attacking RSA-based sessions in SSL\/TLS . In Proceedings of the Workshop on Cryptographic Hardware and Embedded Systems (CHES\u201903) . Lecture Notes in Computer Science , vol. 2779 . Springer, 426--440. Klima, V., Pokorny, O., and Rosa, T. 2003. Attacking RSA-based sessions in SSL\/TLS. In Proceedings of the Workshop on Cryptographic Hardware and Embedded Systems (CHES\u201903). Lecture Notes in Computer Science, vol. 2779. Springer, 426--440."},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.5555\/646766.704278"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/1102120.1102126"},{"key":"e_1_2_1_35_1","volume-title":"Proceedings of the 7th USENIX Security Symposium (SSYM\u201998)","author":"Mitchell J. C.","unstructured":"Mitchell , J. C. , Shmatikov , V. , and Stern , U . 1998. Finite-state analysis of SSL 3.0 . In Proceedings of the 7th USENIX Security Symposium (SSYM\u201998) . USENIX Association, 201--216. Mitchell, J. C., Shmatikov, V., and Stern, U. 1998. Finite-state analysis of SSL 3.0. In Proceedings of the 7th USENIX Security Symposium (SSYM\u201998). USENIX Association, 201--216."},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00145-009-9052-3"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/359657.359659"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICDCS.2005.32"},{"key":"e_1_2_1_39_1","unstructured":"OpenSSL. 2009. EVP_VerifyFinal function signature verification vulnerability. http:\/\/web.nvd.nist.gov\/view\/vuln\/detail?vulnId=CVE-2008-5077. OpenSSL . 2009. EVP_VerifyFinal function signature verification vulnerability. http:\/\/web.nvd.nist.gov\/view\/vuln\/detail?vulnId=CVE-2008-5077."},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/322510.322530"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30564-4_13"},{"key":"e_1_2_1_42_1","volume-title":"Proceedings of the 3rd Symposium on Trustworthy Global Computing. Lecture Notes in Computer Science","volume":"4912","author":"Tsahhirov I.","unstructured":"Tsahhirov , I. and Laud , P . 2007. Application of dependency graphs to security protocol analysis . In Proceedings of the 3rd Symposium on Trustworthy Global Computing. Lecture Notes in Computer Science , vol. 4912 . Springer, 294--311. Tsahhirov, I. and Laud, P. 2007. Application of dependency graphs to security protocol analysis. In Proceedings of the 3rd Symposium on Trustworthy Global Computing. Lecture Notes in Computer Science, vol. 4912. Springer, 294--311."},{"key":"e_1_2_1_43_1","volume-title":"Proceedings of the 2nd USENIX Workshop on Electronic Commerce (WOEC\u201996)","author":"Wagner D.","unstructured":"Wagner , D. and Schneier , B . 1996. Analysis of the SSL 3.0 protocol . In Proceedings of the 2nd USENIX Workshop on Electronic Commerce (WOEC\u201996) . USENIX Association, 29--40. Wagner, D. and Schneier, B. 1996. Analysis of the SSL 3.0 protocol. In Proceedings of the 2nd USENIX Workshop on Electronic Commerce (WOEC\u201996). USENIX Association, 29--40."},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/11502760_20"}],"container-title":["ACM Transactions on Information and System Security"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2133375.2133378","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2133375.2133378","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T10:06:05Z","timestamp":1750241165000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2133375.2133378"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,3]]},"references-count":43,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2012,3]]}},"alternative-id":["10.1145\/2133375.2133378"],"URL":"https:\/\/doi.org\/10.1145\/2133375.2133378","relation":{},"ISSN":["1094-9224","1557-7406"],"issn-type":[{"value":"1094-9224","type":"print"},{"value":"1557-7406","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,3]]},"assertion":[{"value":"2009-03-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2011-06-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2012-03-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}