Verifying layered security protocols

Article type: Research Article

Authors: Gibson-Robinson, Thomas^{; *} | Kamil, Allaa | Lowe, Gavin

Affiliations: Department of Computer Science, University of Oxford, Oxford, UK. E-mails: thomas.gibson-robinson@cs.ox.ac.uk, gavin.lowe@cs.ox.ac.uk

Correspondence: [*] Corresponding author. E-mail: thomas.gibson-robinson@cs.ox.ac.uk.

Abstract: 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. The paper’s main contribution is a proof of the model’s 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.

Keywords: Protocol verification, strand spaces, compositional verification

DOI: 10.3233/JCS-150526

Journal: Journal of Computer Security, vol. 23, no. 3, pp. 259-307, 2015