Abstract
In this article we present a method to avoid security problems in modern m-commerce applications. The security problems that we are addressing are breaches of security due to erroneous cryptographic protocols. We describe a specification technique that gives way to a formal, and thereby rigorous, treatment of the security protocols used in such applications. Security of communication is important in modern m-commerce applications. As parts of the specification of the security protocols, we describe how to specify the behavior of the agents, how to specify the attacker and how further aspects of the application reflect in the formal specification. The problem is that such formal specifications are difficult to get right, so we propose a construction kit for their development.
This is a preview of subscription content, log in via an institution to check access.
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., Needham, R.: Programming satan’s computer. In: van Leeuwen, J. (ed.) Computer Science Today. LNCS, vol. 1000, Springer, Heidelberg (1995)
Burrows, M., Abadi, M., Needham, R.: A logic of authentication. ACM Transactions on Computer Systems 8(1) (February 1990)
Balser, M., Reif, W., Schellhorn, G., Stenzel, K., Thums, A.: Formal system development with KIV. In: Maibaum, T. (ed.) FASE 2000. LNCS, vol. 1783, pp. 363–366. Springer, Heidelberg (2000)
Dolev, D., Yao, A.C.: On the security of public key protocols. In: Proc. 22th IEEE Symposium on Foundations of Computer Science, pp. 350–357. IEEE, Los Alamitos (1981)
EMVCo, L. E.: 4.0 Specifications Book 1 – Application independent ICC to Terminal Interface requirements (December 2000), http://www.emvco.com/documents/specification/view/book1.pdf
Freier, A.O., Karlton, P., Kocher, P.C.: The SSL Protocol Version 3.0. Netscape Communications (November 1996), http://wp.netscape.com/eng/ssl3/
Loeckx, J., Ehrich, H., Wolf, M.: Specification of Abstract Data Types. Wiley-Teubner, Chichester (1996)
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)
Meadows, C.: Formal methods for cryptographic protocol analysis: Emerging issues and trends. IEEE Journal on Selected Areas in Communication 21(1), 44–54 (2003)
The Object Management Group (OMG). OMG Unified Modeling Language Specification Version 1.5 (2003), http://www.omg.org/technology/documents/formal/uml.htm
Paulson, L.C.: The inductive approach to verifying cryptographic protocols. Journal of Computer Security 6, 85–128 (1998)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Haneberg, D., Reif, W., Stenzel, K. (2004). A Construction Kit for Modeling the Security of M-commerce Applications. In: Núñez, M., Maamar, Z., Pelayo, F.L., Pousttchi, K., Rubio, F. (eds) Applying Formal Methods: Testing, Performance, and M/E-Commerce. FORTE 2004. Lecture Notes in Computer Science, vol 3236. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-30233-9_6
Download citation
DOI: https://doi.org/10.1007/978-3-540-30233-9_6
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-23169-1
Online ISBN: 978-3-540-30233-9
eBook Packages: Springer Book Archive