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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Anderson, R.: Security Engineering: A Guide to Building Dependable Distributed Systems. Wiley, Chichester (2001)
Anderson, S., Bologna, S., Felici, M. (eds.): SAFECOMP 2002. LNCS, vol. 2434. Springer, Heidelberg (2002)
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)
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)
Broy, M., Stolen, K. (eds.): Specification and Development of Interactive Systems. Springer, Heidelberg (2001)
Burrows, M., Abadi, M., Needham, R.: A logic of authentication. Proceedings of the Royal Society of London A 426, 233–271 (1989)
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
Dolev, D., Yao, A.: On the security of public key protocols. IEEE Transactions on Information Theory 29(2), 198–208 (1983)
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)
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.
Gollmann, D.: Computer Security. J. Wiley, Chichester (1999)
Grünbauer, J.: Modellbasierte Sicherheitsanalyse einer Bankapplikation. Master’s thesis, Technische Universität München (2003)
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)
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)
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)
ITU. ITU-TS Recommendation Z.120: Message Sequence Chart (MSC). ITU-TS, Geneva (1996)
Jürjens, J.: Critical Systems Development with UML. In: Anderson, S., Bologna, S., Felici, M. (eds.) SAFECOMP 2002. LNCS, vol. 2434, Springer, Heidelberg (2002)
Jürjens, J.: Secure Systems Development with UML. Springer, Berlin (2003) (to be published)
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)
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)
Lano, K., Clark, D., Androutsopoulos, K.: Safety and security analysis of objectoriented models. In: Anderson, S., et al. (eds.) [2]
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)
McMillan, K.L.: Symbolic Model Checking. Kluwer Academic Publishers, Boston (1993)
Mitchell, J.C., Shmatikov, V., Stern, U.: Finite-state analysis of ssl 3.0. In: Seventh USENIX Security Symposium, pp. 201–216 (1998)
Paulson, L.C.: The inductive approach to verifying cryptographic protocols. Journal of Computer Security 6(1–2), 85–128 (1998)
Philipps, J., Slotosch, O.: The Quest for Correct Systems: Model Checking of Diagrams and Datatypes. In: Asia Pacific Software Engineering Conference 1999 (1999)
Rottke, T., Hatebur, D., Heisel, M., Heiner, M.: A problem-oriented approach to common criteria certification. In: Anderson, S., et al. (eds.) [2]
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)
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)
Thompson, S.: Haskell: The Craft of Functional Programming. Addison-Wesley Longman, Amsterdam (1999)
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)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights 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