Automated analysis of TLS 1.3: 0-RTT, resumption and delayed authentication
<p>After a development process of many months, the TLS 1.3 specification is nearly complete. To prevent past mistakes, this crucial security protocol must be thoroughly scrutinised prior to deployment.</p> <br/> <p>In this work we model and analyse revision 10 of the TLS 1.3...
| Main Authors: | , , , |
|---|---|
| Format: | Conference item |
| Published: |
Institute of Electrical and Electronics Engineers
2016
|
| _version_ | 1797100550987186176 |
|---|---|
| author | Cremers, C Horvat, M Scott, S van der Merwe, T |
| author_facet | Cremers, C Horvat, M Scott, S van der Merwe, T |
| author_sort | Cremers, C |
| collection | OXFORD |
| description | <p>After a development process of many months, the TLS 1.3 specification is nearly complete. To prevent past mistakes, this crucial security protocol must be thoroughly scrutinised prior to deployment.</p> <br/> <p>In this work we model and analyse revision 10 of the TLS 1.3 specification using the Tamarin prover, a tool for the automated analysis of security protocols. We specify and analyse the interaction of various handshake modes for an unbounded number of concurrent TLS sessions. We show that revision 10 meets the goals of authenticated key exchange in both the unilateral and mutual authentication cases.</p> <br/> <p>We extend our model to incorporate the desired delayed client authentication mechanism, a feature that is likely to be included in the next revision of the specification, and uncover a potential attack in which an adversary is able to successfully impersonate a client during a PSK-resumption handshake. This observation was reported to, and confirmed by, the IETF TLS Working Group.</p> <br/> <p>Our work not only provides the first supporting evidence for the security of several complex protocol mode interactions in TLS 1.3, but also shows the strict necessity of recent suggestions to include more information in the protocol’s signature contents.</p> |
| first_indexed | 2024-03-07T05:39:07Z |
| format | Conference item |
| id | oxford-uuid:e4f30b61-e0d6-4550-9aa9-cae2066f7af9 |
| institution | University of Oxford |
| last_indexed | 2024-03-07T05:39:07Z |
| publishDate | 2016 |
| publisher | Institute of Electrical and Electronics Engineers |
| record_format | dspace |
| spelling | oxford-uuid:e4f30b61-e0d6-4550-9aa9-cae2066f7af92022-03-27T10:20:19ZAutomated analysis of TLS 1.3: 0-RTT, resumption and delayed authenticationConference itemhttp://purl.org/coar/resource_type/c_5794uuid:e4f30b61-e0d6-4550-9aa9-cae2066f7af9Symplectic Elements at OxfordInstitute of Electrical and Electronics Engineers2016Cremers, CHorvat, MScott, Svan der Merwe, T <p>After a development process of many months, the TLS 1.3 specification is nearly complete. To prevent past mistakes, this crucial security protocol must be thoroughly scrutinised prior to deployment.</p> <br/> <p>In this work we model and analyse revision 10 of the TLS 1.3 specification using the Tamarin prover, a tool for the automated analysis of security protocols. We specify and analyse the interaction of various handshake modes for an unbounded number of concurrent TLS sessions. We show that revision 10 meets the goals of authenticated key exchange in both the unilateral and mutual authentication cases.</p> <br/> <p>We extend our model to incorporate the desired delayed client authentication mechanism, a feature that is likely to be included in the next revision of the specification, and uncover a potential attack in which an adversary is able to successfully impersonate a client during a PSK-resumption handshake. This observation was reported to, and confirmed by, the IETF TLS Working Group.</p> <br/> <p>Our work not only provides the first supporting evidence for the security of several complex protocol mode interactions in TLS 1.3, but also shows the strict necessity of recent suggestions to include more information in the protocol’s signature contents.</p> |
| spellingShingle | Cremers, C Horvat, M Scott, S van der Merwe, T Automated analysis of TLS 1.3: 0-RTT, resumption and delayed authentication |
| title | Automated analysis of TLS 1.3: 0-RTT, resumption and delayed authentication |
| title_full | Automated analysis of TLS 1.3: 0-RTT, resumption and delayed authentication |
| title_fullStr | Automated analysis of TLS 1.3: 0-RTT, resumption and delayed authentication |
| title_full_unstemmed | Automated analysis of TLS 1.3: 0-RTT, resumption and delayed authentication |
| title_short | Automated analysis of TLS 1.3: 0-RTT, resumption and delayed authentication |
| title_sort | automated analysis of tls 1 3 0 rtt resumption and delayed authentication |
| work_keys_str_mv | AT cremersc automatedanalysisoftls130rttresumptionanddelayedauthentication AT horvatm automatedanalysisoftls130rttresumptionanddelayedauthentication AT scotts automatedanalysisoftls130rttresumptionanddelayedauthentication AT vandermerwet automatedanalysisoftls130rttresumptionanddelayedauthentication |