Analysing TLS in the Strand Spaces Model
In this paper, we analyse the Transport Layer Security (TLS) protocol within the strand spaces setting. In <a href='\"http://www.comlab.ox.ac.uk/people/gavin.lowe/Security/Papers/layering.ps\"' target='\"_blank\"'>[BL03]</a> Broadfoot and Lowe sugg...
| Egile Nagusiak: | , |
|---|---|
| Formatua: | Report |
| Argitaratua: |
2008
|
| _version_ | 1826258546714476544 |
|---|---|
| author | Kamil, A Lowe, G |
| author_facet | Kamil, A Lowe, G |
| author_sort | Kamil, A |
| collection | OXFORD |
| description | In this paper, we analyse the Transport Layer Security (TLS) protocol within the strand spaces setting. In <a href='\"http://www.comlab.ox.ac.uk/people/gavin.lowe/Security/Papers/layering.ps\"' target='\"_blank\"'>[BL03]</a> Broadfoot and Lowe suggested an abstraction of TLS. The abstraction models the security services that appear to be provided by the protocol to the high-level security layers. The outcome of our analysis provides a formalisation of the security services provided by TLS and proves that, under reasonable assumptions, the abstract model suggested by Broadfoot and Lowe is correct. To that end, we reduce the complexity of the protocol using safe simplifying transformations. We extend the strand spaces model in order to include the cryptographic operations used in TLS and facilitate its analysis. Finally, we use the extended strand spaces model to fully analyse TLS with its two main components: the Handshake and Record Layer protocols. |
| first_indexed | 2024-03-06T18:35:40Z |
| format | Report |
| id | oxford-uuid:0b244995-30ea-49e8-8d49-eb54abf91d63 |
| institution | University of Oxford |
| last_indexed | 2024-03-06T18:35:40Z |
| publishDate | 2008 |
| record_format | dspace |
| spelling | oxford-uuid:0b244995-30ea-49e8-8d49-eb54abf91d632022-03-26T09:27:52ZAnalysing TLS in the Strand Spaces ModelReporthttp://purl.org/coar/resource_type/c_93fcuuid:0b244995-30ea-49e8-8d49-eb54abf91d63Department of Computer Science2008Kamil, ALowe, GIn this paper, we analyse the Transport Layer Security (TLS) protocol within the strand spaces setting. In <a href='\"http://www.comlab.ox.ac.uk/people/gavin.lowe/Security/Papers/layering.ps\"' target='\"_blank\"'>[BL03]</a> Broadfoot and Lowe suggested an abstraction of TLS. The abstraction models the security services that appear to be provided by the protocol to the high-level security layers. The outcome of our analysis provides a formalisation of the security services provided by TLS and proves that, under reasonable assumptions, the abstract model suggested by Broadfoot and Lowe is correct. To that end, we reduce the complexity of the protocol using safe simplifying transformations. We extend the strand spaces model in order to include the cryptographic operations used in TLS and facilitate its analysis. Finally, we use the extended strand spaces model to fully analyse TLS with its two main components: the Handshake and Record Layer protocols. |
| spellingShingle | Kamil, A Lowe, G Analysing TLS in the Strand Spaces Model |
| title | Analysing TLS in the Strand Spaces Model |
| title_full | Analysing TLS in the Strand Spaces Model |
| title_fullStr | Analysing TLS in the Strand Spaces Model |
| title_full_unstemmed | Analysing TLS in the Strand Spaces Model |
| title_short | Analysing TLS in the Strand Spaces Model |
| title_sort | analysing tls in the strand spaces model |
| work_keys_str_mv | AT kamila analysingtlsinthestrandspacesmodel AT loweg analysingtlsinthestrandspacesmodel |