Sage Journals: Discover world-class research

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

Get full access to this article

View all access options for this article.

References

[1]

Abadi,

Fournet and

Gonthier, Secure implementation of channel abstractions, Information and Computation 174(1) (2002), 37–83.

[2]

Andova,

Cremers,

Gjøsteen,

Mauw,

S.F.

Mjølsnes and

Radomirović, A framework for compositional verification of security protocols, Information and Computation 206(2–4) (2008), 425–459.

[3]

Armando,

Carbone and

Compagna, LTL model checking for security protocols, in: Computer Security Foundations Symposium, 2007, pp. 385–396.

[4]

Bella,

Longo and

L.C.

Paulson, Verifying second-level security protocols, in: Theorem Proving in Higher Order Logics, 2003, pp. 352–366.

[5]

Blanchet, An efficient cryptographic protocol verifier based on Prolog rules, in: Proceedings of the 14th IEEE Computer Security Foundations Workshop, 2001, pp. 82–96.

[6]

Bugliesi and

Focardi, Channel abstractions for network security, Mathematical Structures in Computer Science 20(1) (2010), 3–44.

[7]

Ciobâcă and

Cortier, Protocol composition for arbitrary primitives, in: Computer Security Foundations Symposium, 2010.

[8]

Cortier and

Delaune, Safely composing security protocols, Formal Methods in System Design 34(1) (2008), 1–36.

[9]

C.J.F.

Cremers, The Scyther tool: Verification, falsification, and analysis of security protocols, in: Computer Aided Verification, 2008.

10.

[10]

Datta,

Derek,

J.C.

Mitchell and

Roy, Protocol Composition Logic (PCL), Electronic Notes in Theoretical Computer Science 172 (2007), 311–358.

11.

[11]

Dierks and

Rescorla, The TLS protocol: Version 1.2, 2008.

12.

[12]

Dilloway and

Lowe, Specifying secure transport channels, in: Computer Security Foundations Symposium, 2008, pp. 210–223.

13.

[13]

Dolev and

Yao, On the security of public key protocols, IEEE Transactions on Information Theory 29(2) (1983), 198–208.

14.

[14]

Gibson-Robinson, Analysing layered security protocols, PhD thesis, University of Oxford, 2013.

15.

[15]

Gibson-Robinson and

Lowe, Analysing applications layered on unilaterally authenticating secure transport protocols, in: Formal Aspects in Security and Trust, 2011.

16.

[16]

Groß and

Mödersheim, Vertical protocol composition, in: Computer Security Foundations Symposium, 2011.

17.

[17]

Guttman and

F.J.

Thayer, Protocol independence through disjoint encryption, in: Computer Security Foundations Workshop, 2000, pp. 24–34.

18.

[18]

Guttman and

F.J.

Thayer, Authentication tests and the structure of bundles, Theoretical Computer Science 283(2) (2002), 333–380.

19.

[19]

Kamil and

Lowe, Specifying and modelling secure channels in strand spaces, in: Formal Aspects in Security and Trust, 2009.

20.

[20]

Kamil and

Lowe, Understanding abstractions of secure channels, in: Formal Aspects in Security and Trust, 2010.

21.

[21]

Kamil and

Lowe, Analysing TLS in the strand spaces model, Journal of Computer Security 19(5) (2011), 975–1025.

22.

[22]

Mödersheim and

Viganò, Secure pseudonymous channels, in: European Symposium on Research in Computer Security, 2009.

23.

[23]

Mödersheim and

Viganò, Sufficient conditions for vertical composition of security protocols, in: Proceedings of the 9th ACM Symposium on Information, Computer and Communications Security, 2014, pp. 435–446.

24.

[24]

L.C.

Paulson, The inductive approach to verifying cryptographic protocols, Journal of Computer Security 6(1) (1998), 85–128.

25.

[25]

Schemers and

Allbery, WebAuth technical specification v.3, 2009.

26.

[26]

F.J.

Thayer Fábrega,

Herzog and

Guttman, Strand spaces: Proving security protocols correct, Journal of Computer Security 7(2,3) (1999), 191–230.

Verifying layered security protocols

Abstract

Keywords

Get full access to this article

References