{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,3]],"date-time":"2026-05-03T10:59:28Z","timestamp":1777805968248,"version":"3.51.4"},"reference-count":26,"publisher":"SAGE Publications","issue":"3","license":[{"start":{"date-parts":[[2015,7,2]],"date-time":"2015-07-02T00:00:00Z","timestamp":1435795200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/journals.sagepub.com\/page\/policies\/text-and-data-mining-license"}],"content-domain":{"domain":["journals.sagepub.com"],"crossmark-restriction":true},"short-container-title":["Journal of Computer Security"],"published-print":{"date-parts":[[2015,7,2]]},"abstract":"<jats:p>Abstract<\/jats:p>\n                  <jats:p>Many security protocols are built as the composition of an application-layer protocol and a secure transport protocol, such as TLS. There are several approaches to proving the correctness of such protocols. One popular approach is verification by abstraction, in which the correctness of the application-layer protocol is proven under the assumption that the transport layer satisfies certain properties, such as confidentiality. Following this approach, we adapt the strand spaces model in order to analyse application-layer protocols that depend on secure transport protocols; we consider both bilaterally and unilaterally authenticating secure transport protocols, such as bilateral and unilateral TLS.<\/jats:p>\n                  <jats:p>The paper\u2019s main contribution is a proof of the model\u2019s soundness. In particular, we prove that, subject to a suitable independence assumption, if there is an attack against the application-layer protocol when layered on top of a particular secure transport protocol, then there is an attack against the abstracted model of the application-layer protocol. In contrast to existing work in this area, the independence assumption consists of eight statically checkable conditions, meaning that it is not necessary to consider all possible runs of the protocol.<\/jats:p>","DOI":"10.3233\/jcs-150526","type":"journal-article","created":{"date-parts":[[2015,7,3]],"date-time":"2015-07-03T07:55:44Z","timestamp":1435910144000},"page":"259-307","update-policy":"https:\/\/doi.org\/10.1177\/sage-journals-update-policy","source":"Crossref","is-referenced-by-count":3,"title":["Verifying layered security protocols"],"prefix":"10.1177","volume":"23","author":[{"given":"Thomas","family":"Gibson-Robinson","sequence":"first","affiliation":[{"name":"Department of Computer Science, University of Oxford, Oxford, UK. E-mails:\u00a0,\u00a0"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Allaa","family":"Kamil","sequence":"additional","affiliation":[{"name":"Department of Computer Science, University of Oxford, Oxford, UK. E-mails:\u00a0,\u00a0"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gavin","family":"Lowe","sequence":"additional","affiliation":[{"name":"Department of Computer Science, University of Oxford, Oxford, UK. E-mails:\u00a0,\u00a0"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"179","published-online":{"date-parts":[[2015,7,2]]},"reference":[{"key":"ref001","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2002.3086"},{"key":"ref002","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2007.07.002"},{"key":"ref003","doi-asserted-by":"crossref","unstructured":"[3]A.\u00a0Armando, R.\u00a0Carbone and L.\u00a0Compagna, LTL model checking for security protocols, in: Computer Security Foundations Symposium, 2007, pp.\u00a0385\u2013396.","DOI":"10.1109\/CSF.2007.24"},{"key":"ref004","doi-asserted-by":"crossref","unstructured":"[4]G.\u00a0Bella, C.\u00a0Longo and L.C.\u00a0Paulson, Verifying second-level security protocols, in: Theorem Proving in Higher Order Logics, 2003, pp.\u00a0352\u2013366.","DOI":"10.1007\/10930755_23"},{"key":"ref005","doi-asserted-by":"crossref","unstructured":"[5]B.\u00a0Blanchet, An efficient cryptographic protocol verifier based on Prolog rules, in: Proceedings of the 14th IEEE Computer Security Foundations Workshop, 2001, pp.\u00a082\u201396.","DOI":"10.1109\/CSFW.2001.930138"},{"key":"ref006","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129509990247"},{"key":"ref007","doi-asserted-by":"crossref","unstructured":"[7]S.\u00a0Ciob\u00e2c\u0103 and V.\u00a0Cortier, Protocol composition for arbitrary primitives, in: Computer Security Foundations Symposium, 2010.","DOI":"10.1109\/CSF.2010.29"},{"key":"ref008","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-008-0059-4"},{"key":"ref009","unstructured":"[9]C.J.F.\u00a0Cremers, The Scyther tool: Verification, falsification, and analysis of security protocols, in: Computer Aided Verification, 2008."},{"key":"ref010","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2007.02.012"},{"key":"ref011","unstructured":"[11]T.\u00a0Dierks and E.\u00a0Rescorla, The TLS protocol: Version 1.2, 2008."},{"key":"ref012","doi-asserted-by":"crossref","unstructured":"[12]C.\u00a0Dilloway and G.\u00a0Lowe, Specifying secure transport channels, in: Computer Security Foundations Symposium, 2008, pp.\u00a0210\u2013223.","DOI":"10.1109\/CSF.2008.14"},{"key":"ref013","doi-asserted-by":"publisher","DOI":"10.1109\/TIT.1983.1056650"},{"key":"ref014","unstructured":"[14]T.\u00a0Gibson-Robinson, Analysing layered security protocols, PhD thesis, University of Oxford, 2013."},{"key":"ref015","doi-asserted-by":"crossref","unstructured":"[15]T.\u00a0Gibson-Robinson and G.\u00a0Lowe, Analysing applications layered on unilaterally authenticating secure transport protocols, in: Formal Aspects in Security and Trust, 2011.","DOI":"10.1007\/978-3-642-29420-4_11"},{"key":"ref016","doi-asserted-by":"crossref","unstructured":"[16]T.\u00a0Gro\u00df and S.\u00a0M\u00f6dersheim, Vertical protocol composition, in: Computer Security Foundations Symposium, 2011.","DOI":"10.1109\/CSF.2011.23"},{"key":"ref017","doi-asserted-by":"crossref","unstructured":"[17]J.\u00a0Guttman and F.J.\u00a0Thayer, Protocol independence through disjoint encryption, in: Computer Security Foundations Workshop, 2000, pp.\u00a024\u201334.","DOI":"10.1109\/CSFW.2000.856923"},{"key":"ref018","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(01)00139-6"},{"key":"ref019","doi-asserted-by":"crossref","unstructured":"[19]A.\u00a0Kamil and G.\u00a0Lowe, Specifying and modelling secure channels in strand spaces, in: Formal Aspects in Security and Trust, 2009.","DOI":"10.1007\/978-3-642-12459-4_17"},{"key":"ref020","doi-asserted-by":"crossref","unstructured":"[20]A.\u00a0Kamil and G.\u00a0Lowe, Understanding abstractions of secure channels, in: Formal Aspects in Security and Trust, 2010.","DOI":"10.1007\/978-3-642-19751-2_4"},{"key":"ref021","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-2011-0429"},{"key":"ref022","doi-asserted-by":"crossref","unstructured":"[22]S.\u00a0M\u00f6dersheim and L.\u00a0Vigan\u00f2, Secure pseudonymous channels, in: European Symposium on Research in Computer Security, 2009.","DOI":"10.1007\/978-3-642-04444-1_21"},{"key":"ref023","doi-asserted-by":"crossref","unstructured":"[23]S.\u00a0M\u00f6dersheim and L.\u00a0Vigan\u00f2, Sufficient conditions for vertical composition of security protocols, in: Proceedings of the 9th ACM Symposium on Information, Computer and Communications Security, 2014, pp.\u00a0435\u2013446.","DOI":"10.1145\/2590296.2590330"},{"key":"ref024","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-1998-61-205"},{"key":"ref025","unstructured":"[25]R.\u00a0Schemers and R.\u00a0Allbery, WebAuth technical specification v.3, 2009."},{"key":"ref026","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-1999-72-304"}],"container-title":["Journal of Computer Security"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/journals.sagepub.com\/doi\/pdf\/10.3233\/JCS-150526","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/journals.sagepub.com\/doi\/full-xml\/10.3233\/JCS-150526","content-type":"application\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/journals.sagepub.com\/doi\/pdf\/10.3233\/JCS-150526","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,29]],"date-time":"2026-04-29T20:44:53Z","timestamp":1777495493000},"score":1,"resource":{"primary":{"URL":"https:\/\/journals.sagepub.com\/doi\/10.3233\/JCS-150526"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,7,2]]},"references-count":26,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2015,7,2]]}},"alternative-id":["10.3233\/JCS-150526"],"URL":"https:\/\/doi.org\/10.3233\/jcs-150526","relation":{},"ISSN":["0926-227X","1875-8924"],"issn-type":[{"value":"0926-227X","type":"print"},{"value":"1875-8924","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,7,2]]}}}