Browser Model for Security Analysis of Browser-Based Protocols

  • Thomas Groß
  • Birgit Pfitzmann
  • Ahmad-Reza Sadeghi
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3679)


Currently, many industrial initiatives focus on web applications. In this context an important requirement is often that the user should only rely on a standard web browser. Hence the underlying security services also rely solely on a browser for interaction with the user. Browser-based identity federation is a prominent example of such a service. Very little is still known about the security of browser-based protocols, and they seem at least as error-prone as standard security protocols. In particular, standard web browsers have limited cryptographic capabilities and thus new protocols are used. Furthermore, these protocols require certain care by the user in person, which must be modeled. In addition, browsers, unlike normal protocol principals, cannot be assumed to do nothing but execute the given security protocol.

In this paper, we lay the theoretical basis for the rigorous analysis and security proofs of browser-based protocols. We formally model web browsers, secure browser channels, and the security-relevant browsing behavior of a user as automata. As a first rigorous security proof of a browser-based protocol we prove the security of password-based user authentication in our model. This is not only the most common stand-alone type of browser authentication, but also a fundamental building block for more complex protocols like identity federation.


User Authentication Security Protocol Authentication Server Security Assertion Markup Language State Transition Function 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. 1.
    Bellare, M., Rogaway, P.: Entity authentication and key distribution. In: Stinson, D.R. (ed.) CRYPTO 1993. LNCS, vol. 773, pp. 232–249. Springer, Heidelberg (1994)Google Scholar
  2. 2.
    Canetti, R., Krawczyk, H.: Universally composable notions of key exchange and secure channels (extended abstract). In: Knudsen, L.R. (ed.) EUROCRYPT 2002. LNCS, vol. 2332, pp. 337–351. Springer, Heidelberg (2002), Extended version in IACR Cryptology ePrint Archive 2002/059,
  3. 3.
    Cantor, S., Erdos, M.: Shibboleth-architecture draft v05 (May 2002),
  4. 4.
    Dang, Z., Kemmerer, R.: Using the ASTRAL model checker for cryptographic protocol analysis. In: Proc. DIMACS Workshop on Design and Formal Verification of Security Protocols (1997),
  5. 5.
    Dierks, T., Allen, C.: RFC 2246: The TLS protocol (January 1999), Status: Standards TrackGoogle Scholar
  6. 6.
    Dolev, D., Yao, A.C.: On the security of public key protocols. IEEE Transactions on Information Theory 29(2), 198–208 (1983)zbMATHCrossRefMathSciNetGoogle Scholar
  7. 7.
    Dutertre, B., Schneider, S.: Using a PVS embedding of CSP to verify authentication protocols. In: Gunter, E.L., Felty, A.P. (eds.) TPHOLs 1997. LNCS, vol. 1275, pp. 121–136. Springer, Heidelberg (1997)CrossRefGoogle Scholar
  8. 8.
    Fielding, R.T., Gettys, J., Mogul, J.C., Frystyk, H., Masinter, L., Leach, P., Berners-Lee, T.: RFC 2616: Hypertext transfer protocol – HTTP/1.1, Status: Standards Track (June 1999)Google Scholar
  9. 9.
    Fu, K., Sit, E., Smith, K., Feamster, N.: Dos and don’ts of client authentication on the web. In: Proceedings of the 10th USENIX Security Symposium, Washington, D.C, USENIX. An extended version is available as MIT-LCS-TR-818 (August 2001)Google Scholar
  10. 10.
    Groß, T.: Security analysis of the SAML Single Sign-on Browser/Artifact profile. In: Proc. 19th Annual Computer Security Applications Conference. IEEE, Los Alamitos (2003)Google Scholar
  11. 11.
    Groß, T., Pfitzmann, B.: Proving a WS-Federation Passive Requestor profile. In: ACM Workshop on Secure Web Services (SWS), Washington, DC. ACM Press, New York (2004)Google Scholar
  12. 12.
    Groß, T., Pfitzmann, B., Sadeghi, A.-R.: Browser model for security analysis of browser-based protocols. IACR Cryptology ePrint Archive 2005/127 (May 2005),
  13. 13.
    Kaler, C., Nadalin, A. (eds.): Web Services Federation Language (WS-Federation), Version 1.0 July 2003, BEA and IBM and Microsoft and RSA Security and VeriSign,
  14. 14.
    Kaler, C., Nadalin, A. (eds.): WS-Federation: Passive Requestor Profile, Version 1.0 July 2003, BEA and IBM and Microsoft and RSA Security and VeriSign,
  15. 15.
    Kemmerer., R.A.: Using formal verification techniques to analyze encryption protocols. In: Proc. 1987 IEEE Symp. on Security and Privacy, Oakland, California, pp. 134–138. IEEE, Los Alamitos (1987)Google Scholar
  16. 16.
    Kormann, D.P., Rubin, A.D.: Risks of the Passport single signon protocol. Computer Networks 33(1–6), 51–58 (2000)CrossRefGoogle Scholar
  17. 17.
    Krawczyk, H.: SKEME: A versatile secure key exchange mechanism for the Internet. In: Proceedings of the Symposium on Network and Distributed Systems Security (NDSS 1996), San Diego, California, February 1996, pp. 114–127 (1996) Internet SocietyGoogle Scholar
  18. 18.
    Krawczyk, H.: The order of encryption and authentication for protecting communications (or: how secure is SSL?). In: Kilian, J. (ed.) CRYPTO 2001. LNCS, vol. 2139, pp. 310–331. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  19. 19.
    Liberty Alliance Project. Liberty Phase 2 final specifications (November 2003),
  20. 20.
    Lowe, G.: An attack on the Needham-Schroeder public-key authentication protocol. Information Processing Letters 56(3), 131–135 (1995)zbMATHCrossRefGoogle Scholar
  21. 21.
    Lowe, G.: Breaking and fixing the Needham-Schroeder public-key protocol using FDR. In: Margaria, T., Steffen, B. (eds.) TACAS 1996. LNCS, vol. 1055, pp. 147–166. Springer, Heidelberg (1996)Google Scholar
  22. 22.
    Lynch, N.: I/O automaton models and proofs for shared-key communication systems. In: Proc. 12th IEEE Computer Security Foundations Workshop (CSFW), pp. 14–29 (1999)Google Scholar
  23. 23.
    Meadows, C.: Using narrowing in the analysis of key management protocols. In: Proc. 10th IEEE Symposium on Security & Privacy, pp. 138–147 (1989)Google Scholar
  24. 24.
    Microsoft Corporation.NET Passport documentation, in particular Technical Overview, and SDK 2.1 Documentation (started 1999) (September 2001)Google Scholar
  25. 25.
    Millen, J.K.: The interrogator: A tool for cryptographic protocol security. In: Proc. 5th IEEE Symposium on Security & Privacy, pp. 134–141 (1984)Google Scholar
  26. 26.
    Mitchell, J., Mitchell, M., Stern, U.: Automated analysis of cryptographic protocols using murφ. In: Proc. 18th IEEE Symposium on Security & Privacy, pp. 141–151 (1997)Google Scholar
  27. 27.
    Mitchell, J.C., Shmatikov, V., Stern, U.: Finite-state analysis of SSL 3.0 and related protocols. In: DIMACS Workshop on Design and Formal Verification of Security Protocols (September 1997),
  28. 28.
    Needham, R.M., Schroeder, M.D.: Using encryption for authentication in large networks of computers. Communications of the ACM 21(12), 993–999 (1978)zbMATHCrossRefGoogle Scholar
  29. 29.
    OASIS Standard. Security assertion markup language (SAML) V1.1 (November 2002),
  30. 30.
    Object Management Group. Unified modeling language (UML) (March 2003),
  31. 31.
    Paulson, L.C.: The inductive approach to verifying cryptographic protocols. Journal of Cryptology 6(1), 85–128 (1998)Google Scholar
  32. 32.
    Paulson, L.C.: Inductive analysis of the internet protocol TLS. ACM Transactions on Information and System Security 2(3), 332–351 (1999)CrossRefGoogle Scholar
  33. 33.
    Pfitzmann, B.: Privacy in enterprise identity federation - policies for Liberty single signon. In: Dingledine, R. (ed.) PET 2003. LNCS, vol. 2760, pp. 189–204. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  34. 34.
    Pfitzmann, B.: Privacy in enterprise identity federation - policies for Liberty 2 single signon. Elsevier Information Security Technical Report (ISTR) 9(1), 45–58 (2004), CrossRefGoogle Scholar
  35. 35.
    Pfitzmann, B., Waidner, M.: A model for asynchronous reactive systems and its application to secure message transmission. In: Proc. 22nd IEEE Symposium on Security & Privacy, pp. 184–200 (2001); Extended version of the model (with Michael Backes) IACR Cryptology ePrint Archive 2004/082,
  36. 36.
    Pfitzmann, B., Waidner, M.: Privacy in browser-based attribute exchange. In: ACM Workshop on Privacy in the Electronic Society (WPES), Washington, USA, November 2002, pp. 52–62 (2002)Google Scholar
  37. 37.
    Pfitzmann, B., Waidner, M.: Analysis of Liberty single-signon with enabled clients. IEEE Internet Computing 7(6), 38–44 (2003)CrossRefGoogle Scholar
  38. 38.
    Pfitzmann, B., Waidner, M.: Federated identity-management protocols — where user authentication protocols may go. In: Christianson, B., Crispo, B., Malcolm, J.A., Roe, M. (eds.) Security Protocols 2003. LNCS, vol. 3364, pp. 153–174. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  39. 39.
    Rescorla, E.: Internet RFC 2818: HTTP over TLS (May 2000)Google Scholar
  40. 40.
    Shoup, V.: On formal models for secure key exchange. Research Report RZ 3120 (#93166), IBM Research (April 1999). Version 4 (November 1999), available from
  41. 41.
    Wagner, D., Schneier, B.: Analysis of the SSL 3.0 protocol. In: Proc. 2nd USENIX Workshop on Electronic Commerce, pp. 29–40 (1996)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Thomas Groß
    • 1
  • Birgit Pfitzmann
    • 1
  • Ahmad-Reza Sadeghi
    • 2
  1. 1.IBM Zurich Research LabRüschlikonSwitzerland
  2. 2.Ruhr-University BochumBochumGermany

Personalised recommendations