Skip to main content
SpringerLink
Log in

Analysing Applications Layered on Unilaterally Authenticating Protocols

  • Conference paper
Formal Aspects of Security and Trust (FAST 2011)

Part of the book series: Lecture Notes in Computer Science ((LNSC,volume 7140))

Included in the following conference series:

Abstract

There are many approaches to proving the correctness of application-layer protocols that are layered on secure transport protocols, such as TLS. 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. Following this approach, we adapt the strand spaces model in order to analyse application-layer protocols that depend on unilaterally authenticating secure transport protocols, such as unilateral TLS. We develop proof rules that enable us to prove the correctness of application-layer protocols that use either unilateral or bilateral secure transport protocols, and illustrate them by proving the correctness of WebAuth, a single-sign-on protocol that makes extensive use of unilateral TLS.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 54.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 69.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Dierks, T., Rescorla, E.: The TLS Protocol: Version 1.2 (2008), http://tools.ietf.org/html/rfc5246

  2. Bella, G., Longo, C., Paulson, L.: Verifying Second-Level Security Protocols. In: Theorem Proving in Higher Order Logics (2003)

    Google Scholar 

  3. Dilloway, C., Lowe, G.: Specifying Secure Transport Channels. In: Computer Security Foundations Symposium (2008)

    Google Scholar 

  4. Armando, A., Carbone, R., Compagna, L.: LTL Model Checking for Security Protocols. In: Computer Security Foundations Symposium (2007)

    Google Scholar 

  5. Armando, A., Carbone, R., Compagna, L., Cuellar, J., Tobarra, L.: Formal Analysis of SAML 2.0 Web Browser Single Sign-On: Breaking the SAML-based Single Sign-On for Google Apps. In: Formal Methods in Security Engineering (2008)

    Google Scholar 

  6. Bugliesi, M., Focardi, R.: Language Based Secure Communication. In: Computer Security Foundations Symposium (2008)

    Google Scholar 

  7. Mödersheim, S., Viganò, L.: Secure Pseudonymous Channels. In: Backes, M., Ning, P. (eds.) ESORICS 2009. LNCS, vol. 5789, pp. 337–354. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  8. Kamil, A., Lowe, G.: Specifying and Modelling Secure Channels in Strand Spaces. In: Degano, P., Guttman, J.D. (eds.) FAST 2009. LNCS, vol. 5983, pp. 233–247. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  9. Kamil, A.: The Modelling and Analysis of Layered Security Architectures in Strand Spaces. DPhil Thesis. University of Oxford (2010)

    Google Scholar 

  10. Thayer Fábrega, F.J., Herzog, J., Guttman, J.: Strand spaces: Proving Security Protocols Correct. Journal of Computer Security (1999)

    Google Scholar 

  11. Schemers, R., Allbery, R.: WebAuth Technical Specification v.3 (2009), http://webauth.stanford.edu/protocol

  12. Fitzpatrick, B., Recordon, D., Hardt, D., Bufu, J., Hoyt, J.: OpenID Authentication 2.0, http://openid.net/specs/openid-authentication-2_0.html

  13. Leach, P.J., Berners-Lee, T., Mogul, J.C., Masinter, L., Fielding, R.T., Gettys, J.: Hypertext Transfer Protocol – HTTP/1.1 (2004), http://tools.ietf.org/html/rfc2616

  14. Rescorla, E.: HTTP Over TLS (2000), http://tools.ietf.org/html/rfc2818

  15. Guttman, J.D., Thayer, F.J.: Authentication tests and the structure of bundles. Theoretical Computer Science (2002)

    Google Scholar 

  16. Groß, T., Mödersheim, S.: Vertical Protocol Composition. In: Computer Security Foundations Symposium (2011)

    Google Scholar 

  17. Kamil, A., Lowe, G.: Analysing TLS in the Strand Spaces Model. To appear in Journal of Computer Security (2011)

    Google Scholar 

  18. Kamil, A., Lowe, G.: Understanding Abstractions of Secure Channels. In: Degano, P., Etalle, S., Guttman, J. (eds.) FAST 2010. LNCS, vol. 6561, pp. 50–64. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  19. Doghmi, S., Guttman, J., Thayer, F.J.: Searching for Shapes in Cryptographic Protocols. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 523–537. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, University of Oxford, Wolfson Building, Parks Road, Oxford, OX1 3QD, UK

    Thomas Gibson-Robinson & Gavin Lowe

Authors
  1. Thomas Gibson-Robinson
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Gavin Lowe
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. IMDEA Software Institute, Universidad Politecnica de Madrid, Campus Montegancedo, 28660, Boadilla del Monte, Madrid, Spain

    Gilles Barthe

  2. Carnegie Mellon University, NASA Research Park, Bldg. 23 (MS 23-11), P.O. Box 1, 94035-0001, Moffet Field, CA, USA

    Anupam Datta

  3. Faculty of Mathematics and Computer Science, Embedded Systems Security Group, Technical University of Eindhoven, P.O. Box 513, 5600 MB, Eindhoven, The Netherlands

    Sandro Etalle

Rights and permissions

Reprints and permissions

Copyright information

© 2012 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Gibson-Robinson, T., Lowe, G. (2012). Analysing Applications Layered on Unilaterally Authenticating Protocols. In: Barthe, G., Datta, A., Etalle, S. (eds) Formal Aspects of Security and Trust. FAST 2011. Lecture Notes in Computer Science, vol 7140. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-29420-4_11

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-29420-4_11

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-29419-8

  • Online ISBN: 978-3-642-29420-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation