We report ongoing work towards a verified reference
\nimplementation of TLS 1.3 in the F* programming language. Our
\ncode supports selected ciphersuites for all versions of TLS from
\n1.0 to 1.3. It is being developed on http:\/\/github.com\/mitls as the
\nnext version of MITLS, written in F? instead of F#. We intend to
\nprove a strong, joint cryptographic security theorem for TLS 1.3
\nclients and servers, even when they run alongside older versions
\nof the protocol with weaker security. Our verification approach
\nadapts and extends that of MITLS in several ways: (1) we adopt
\nan idiomatic stateful style that promises higher performance than
\nthe pure functional style of MITLS; (2) we seek to prove stronger
\nsecurity properties with fewer ad hoc assumptions; (3) we rely on
\nadvanced F? type inference to substantially reduce both the code
\nbase and the typed proof annotations. This paper describes our
\nimplementation architecture, our new composite state machine
\nfor TLS 1.0\u20131.3, and our target security theorem. By the time of
\nthe TRON workshop, we will present concrete verification results
\nfor our implementation. As far as we are aware, these will be
\nthe first cryptographic proofs for an implementation of TLS 1.3,
\nand a fortiori for an implementation that is backward compatible
\nwith older versions of the protocol. We anticipate that our effort
\nwill identify early problems and offer implementation guidelines
\nfor other TLS libraries.<\/p>\n","protected":false},"excerpt":{"rendered":"
We report ongoing work towards a verified reference implementation of TLS 1.3 in the F* programming language. Our code supports selected ciphersuites for all versions of TLS from 1.0 to 1.3. It is being developed on http:\/\/github.com\/mitls as the next version of MITLS, written in F? instead of F#. We intend to prove a strong, […]<\/p>\n","protected":false},"featured_media":0,"template":"","meta":{"msr-url-field":"","msr-podcast-episode":"","msrModifiedDate":"","msrModifiedDateEnabled":false,"ep_exclude_from_search":false,"_classifai_error":"","msr-author-ordering":[{"type":"user_nicename","value":"antdl","user_id":"31056"},{"type":"user_nicename","value":"fournet","user_id":"31819"},{"type":"user_nicename","value":"markulf","user_id":"32818"},{"type":"user_nicename","value":"protz","user_id":"33286"},{"type":"user_nicename","value":"nswamy","user_id":"33138"},{"type":"user_nicename","value":"santiago","user_id":"33518"}],"msr_publishername":"","msr_publisher_other":"","msr_booktitle":"","msr_chapter":"","msr_edition":"TRON Workshop","msr_editors":"","msr_how_published":"","msr_isbn":"","msr_issue":"","msr_journal":"","msr_number":"","msr_organization":"","msr_pages_string":"","msr_page_range_start":"","msr_page_range_end":"","msr_series":"","msr_volume":"","msr_copyright":"","msr_conference_name":"TRON Workshop","msr_doi":"","msr_arxiv_id":"","msr_s2_paper_id":"","msr_mag_id":"","msr_pubmed_id":"","msr_other_authors":"","msr_other_contributors":"","msr_speaker":"","msr_award":"","msr_affiliation":"","msr_institution":"","msr_host":"","msr_version":"","msr_duration":"","msr_original_fields_of_study":"","msr_release_tracker_id":"","msr_s2_match_type":"","msr_citation_count_updated":"","msr_published_date":"2016-07-01","msr_highlight_text":"","msr_notes":"","msr_longbiography":"","msr_publicationurl":"","msr_external_url":"","msr_secondary_video_url":"","msr_conference_url":"","msr_journal_url":"","msr_s2_pdf_url":"","msr_year":0,"msr_citation_count":0,"msr_influential_citations":0,"msr_reference_count":0,"msr_s2_match_confidence":0,"msr_microsoftintellectualproperty":true,"msr_s2_open_access":false,"msr_s2_author_ids":[],"msr_pub_ids":[],"msr_hide_image_in_river":0,"footnotes":""},"msr-research-highlight":[],"research-area":[13560],"msr-publication-type":[193716],"msr-publisher":[],"msr-focus-area":[],"msr-locale":[268875],"msr-post-option":[],"msr-field-of-study":[],"msr-conference":[],"msr-journal":[],"msr-impact-theme":[],"msr-pillar":[],"class_list":["post-325655","msr-research-item","type-msr-research-item","status-publish","hentry","msr-research-area-programming-languages-software-engineering","msr-locale-en_us"],"msr_publishername":"","msr_edition":"TRON Workshop","msr_affiliation":"","msr_published_date":"2016-07-01","msr_host":"","msr_duration":"","msr_version":"","msr_speaker":"","msr_other_contributors":"","msr_booktitle":"","msr_pages_string":"","msr_chapter":"","msr_isbn":"","msr_journal":"","msr_volume":"","msr_number":"","msr_editors":"","msr_series":"","msr_issue":"","msr_organization":"","msr_how_published":"","msr_notes":"","msr_highlight_text":"","msr_release_tracker_id":"","msr_original_fields_of_study":"","msr_download_urls":"","msr_external_url":"","msr_secondary_video_url":"","msr_longbiography":"","msr_microsoftintellectualproperty":1,"msr_main_download":"325658","msr_publicationurl":"","msr_doi":"","msr_publication_uploader":[{"type":"file","title":"tron16","viewUrl":"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2016\/11\/tron16.pdf","id":325658,"label_id":0}],"msr_related_uploader":"","msr_citation_count":0,"msr_citation_count_updated":"","msr_s2_paper_id":"","msr_influential_citations":0,"msr_reference_count":0,"msr_arxiv_id":"","msr_s2_author_ids":[],"msr_s2_open_access":false,"msr_s2_pdf_url":null,"msr_attachments":[],"msr-author-ordering":[{"type":"user_nicename","value":"antdl","user_id":31056,"rest_url":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/microsoft-research\/v1\/researchers?person=antdl"},{"type":"user_nicename","value":"fournet","user_id":31819,"rest_url":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/microsoft-research\/v1\/researchers?person=fournet"},{"type":"user_nicename","value":"markulf","user_id":32818,"rest_url":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/microsoft-research\/v1\/researchers?person=markulf"},{"type":"user_nicename","value":"protz","user_id":33286,"rest_url":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/microsoft-research\/v1\/researchers?person=protz"},{"type":"user_nicename","value":"nswamy","user_id":33138,"rest_url":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/microsoft-research\/v1\/researchers?person=nswamy"},{"type":"user_nicename","value":"santiago","user_id":33518,"rest_url":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/microsoft-research\/v1\/researchers?person=santiago"}],"msr_impact_theme":[],"msr_research_lab":[199561],"msr_event":[],"msr_group":[],"msr_project":[235367],"publication":[],"video":[],"msr-tool":[],"msr_publication_type":"inproceedings","related_content":{"projects":[{"ID":235367,"post_title":"Project Everest","post_name":"project-everest-verified-secure-implementations-https-ecosystem","post_type":"msr-project","post_date":"2020-02-27 07:12:30","post_modified":"2023-02-15 01:49:37","post_status":"publish","permalink":"https:\/\/www.microsoft.com\/en-us\/research\/project\/project-everest-verified-secure-implementations-https-ecosystem\/","post_excerpt":"Project Everest aims to build and deploy a verified HTTPS stack, constructing a high-performance, standards-compliant, and\u00a0veri\ufb01ed implementation of the full HTTPS ecosystem.","_links":{"self":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project\/235367"}]}}]},"_links":{"self":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-research-item\/325655","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-research-item"}],"about":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/types\/msr-research-item"}],"version-history":[{"count":2,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-research-item\/325655\/revisions"}],"predecessor-version":[{"id":532396,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-research-item\/325655\/revisions\/532396"}],"wp:attachment":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/media?parent=325655"}],"wp:term":[{"taxonomy":"msr-research-highlight","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-research-highlight?post=325655"},{"taxonomy":"msr-research-area","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/research-area?post=325655"},{"taxonomy":"msr-publication-type","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-publication-type?post=325655"},{"taxonomy":"msr-publisher","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-publisher?post=325655"},{"taxonomy":"msr-focus-area","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-focus-area?post=325655"},{"taxonomy":"msr-locale","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-locale?post=325655"},{"taxonomy":"msr-post-option","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-post-option?post=325655"},{"taxonomy":"msr-field-of-study","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-field-of-study?post=325655"},{"taxonomy":"msr-conference","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-conference?post=325655"},{"taxonomy":"msr-journal","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-journal?post=325655"},{"taxonomy":"msr-impact-theme","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-impact-theme?post=325655"},{"taxonomy":"msr-pillar","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-pillar?post=325655"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}