Skip to main content
SpringerLink
Log in

Modelling and Verification of Layered Security Protocols: A Bank Application

  • Conference paper
Computer Safety, Reliability, and Security (SAFECOMP 2003)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2788))

Included in the following conference series:

Abstract

Designing security-critical systems correctly is very difficult and there are many examples of weaknesses arising in practice. A particular challenge lies in the development of layered security protocols motivated by the need to combine existing or specifically designed protocols that each enforce a particular security requirement. Although appealing from a practical point of view, this approach raises the difficult question of the security properties guaranteed by the combined layered protocols, as opposed to each protocol in isolation. In this work, we apply a method for facilitating the development of trustworthy security-critical systems using the computer-aided systems engineering tool autofocus to the particular problem of layered security protocols. We explain our method at the example of a banking application which is currently under development by a major German bank and is about to be put to commercial use.

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 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.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. Anderson, R.: Security Engineering: A Guide to Building Dependable Distributed Systems. Wiley, Chichester (2001)

    Google Scholar 

  2. Anderson, S., Bologna, S., Felici, M. (eds.): SAFECOMP 2002. LNCS, vol. 2434. Springer, Heidelberg (2002)

    MATH  Google Scholar 

  3. Bloomfield, R.E., Craigen, D., Koob, F., Ullmann, M., Wittmann, S.: Formal methods diffusion: Past lessons and future prospects. In: Koornneef, F., van der Meulen, M.J.P. (eds.) SAFECOMP 2000. LNCS, vol. 1943, pp. 211–226. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  4. Broy, M., Dederich, F., Dendorfer, C., Fuchs, M., Gritzner, T., Weber, R.: The design of distributed systems – an introduction to FOCUS. Technical Report TUM-I9202, Technische Universität München (1992)

    Google Scholar 

  5. Broy, M., Stolen, K. (eds.): Specification and Development of Interactive Systems. Springer, Heidelberg (2001)

    MATH  Google Scholar 

  6. Burrows, M., Abadi, M., Needham, R.: A logic of authentication. Proceedings of the Royal Society of London A 426, 233–271 (1989)

    Article  MATH  MathSciNet  Google Scholar 

  7. Daniel, P.: Security of critical systems – management issues. In: Critical Systems Conference 2001, Birmingham, October 23rd–24th (2001) The Safety-Critical Systems Club and Software Reliability and Metrics Club

    Google Scholar 

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

    Article  MATH  MathSciNet  Google Scholar 

  9. Allen Emerson, E.: Temporal and modal logic. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, volume B, ch. 16, pp. 995–1072. Elsevier Science Publishers, Amsterdam (1990)

    Google Scholar 

  10. Fredriksen, R., Kristiansen, M., Gran, B., Stolen, K., Opperud, T., Dimitrakos, T.: The CORAS framework for a model-based risk management process. In: Anderson, S., et al. (eds.) [2], pp. 94–105.

    Google Scholar 

  11. Gollmann, D.: Computer Security. J. Wiley, Chichester (1999)

    Google Scholar 

  12. Grünbauer, J.: Modellbasierte Sicherheitsanalyse einer Bankapplikation. Master’s thesis, Technische Universität München (2003)

    Google Scholar 

  13. Guttman, J.D.: Security goals: Packet trajectories and strand spaces. In: Focardi, R., Gorrieri, R. (eds.) FOSAD 2000. LNCS, vol. 2171, p. 197. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  14. Huber, F., Molterer, S., Rausch, A., Schätz, B., Sihling, M., Slotosch, O.: Tool supported Specification and Simulation of Distributed Systems. In: International Symposium on Software Engineering for Parallel and Distributed Systems, pp. 155–164 (1998)

    Google Scholar 

  15. Huber, F., Molterer, S., Schätz, B., Slotosch, O., Vilbig, A.: Traffic Lights – An AutoFocus Case Study. In: 1998 International Conference on Application of Concurrency to System Design, pp. 282–294. IEEE Computer Society, Los Alamitos (1998)

    Chapter  Google Scholar 

  16. ITU. ITU-TS Recommendation Z.120: Message Sequence Chart (MSC). ITU-TS, Geneva (1996)

    Google Scholar 

  17. Jürjens, J.: Critical Systems Development with UML. In: Anderson, S., Bologna, S., Felici, M. (eds.) SAFECOMP 2002. LNCS, vol. 2434, Springer, Heidelberg (2002)

    Google Scholar 

  18. Jürjens, J.: Secure Systems Development with UML. Springer, Berlin (2003) (to be published)

    Google Scholar 

  19. Jürjens, J., Wimmel, G.: Security modelling for electronic commerce: The Common Electronic Purse Specifications. In: First IFIP conference on e-commerce, e-business, and e-government (I3E). Kluwer, Dordrecht (2001)

    Google Scholar 

  20. Koob, F., Ullmann, M., Wittmann, S.: The new topicality of using formal models of security policy within the security engineering process. In: Hutter, D., Traverso, P. (eds.) FM-Trends 1998. LNCS, vol. 1641, pp. 302–310. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  21. Lano, K., Clark, D., Androutsopoulos, K.: Safety and security analysis of objectoriented models. In: Anderson, S., et al. (eds.) [2]

    Google Scholar 

  22. 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 

  23. McMillan, K.L.: Symbolic Model Checking. Kluwer Academic Publishers, Boston (1993)

    MATH  Google Scholar 

  24. Mitchell, J.C., Shmatikov, V., Stern, U.: Finite-state analysis of ssl 3.0. In: Seventh USENIX Security Symposium, pp. 201–216 (1998)

    Google Scholar 

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

    Google Scholar 

  26. Philipps, J., Slotosch, O.: The Quest for Correct Systems: Model Checking of Diagrams and Datatypes. In: Asia Pacific Software Engineering Conference 1999 (1999)

    Google Scholar 

  27. Rottke, T., Hatebur, D., Heisel, M., Heiner, M.: A problem-oriented approach to common criteria certification. In: Anderson, S., et al. (eds.) [2]

    Google Scholar 

  28. Santen, T., Pfitzmann, A., Heisel, M.: Specification and refinement of secure it systems. In: Muntean, T., Butler, M. (eds.) International Workshop on Refinement of Critical Systems: Methods, Tools and Experience, RCS 2002 (2002)

    Google Scholar 

  29. Slotosch, O.: Quest: Overview over the Project. In: Hutter, D., Traverso, P. (eds.) FM-Trends 1998. LNCS, vol. 1641, pp. 346–350. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  30. Thompson, S.: Haskell: The Craft of Functional Programming. Addison-Wesley Longman, Amsterdam (1999)

    Google Scholar 

  31. Wimmel, G., Wißpeintner, A.: Extended Description Techniques for Security Engineering. In: Trusted Information, the New Decade Challege. 16th International Conference on Information Security, IFIP/Sec (2001)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, Munich University of Technology, Boltzmannstr. 3, D-85748, Garching, Germany

    Johannes Grünbauer, Jan Jürjens & Guido Wimmel

  2. Secaron AG, Ludwigstrasse 55, D-85399, Hallbergmoos, Germany

    Helia Hollmann

Authors
  1. Johannes Grünbauer
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Helia Hollmann
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Jan Jürjens
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Guido Wimmel
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. School of Informatics, The University of Edinburgh LFCS, Mayfield Road, EH9 3JZ, Edinburgh, UK

    Stuart Anderson

  2. School of Informatics, The University of Edinburgh, EH9 3JZ, Edinburgh, UK

    Massimo Felici

  3. Centre for Software Reliability, City University, Northampton Square, EC1V 0HB, London, UK

    Bev Littlewood

Rights and permissions

Reprints and permissions

Copyright information

© 2003 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Grünbauer, J., Hollmann, H., Jürjens, J., Wimmel, G. (2003). Modelling and Verification of Layered Security Protocols: A Bank Application. In: Anderson, S., Felici, M., Littlewood, B. (eds) Computer Safety, Reliability, and Security. SAFECOMP 2003. Lecture Notes in Computer Science, vol 2788. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-39878-3_10

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-39878-3_10

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-20126-7

  • Online ISBN: 978-3-540-39878-3

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation