Abstract
We have presented a method for the formal development of secure smartcard applications. The method combines and integrates different techniques (with algebraic specifications at the core) to tackle the different problems: objects and distributed systems, attackers and cryptographic protocols, JavaCard programs and limited resources. The techniques include UML models enriched by algebraic specifications, and dynamic logic for JavaCard verification. The method is tailored to take advantage of the special features of smartcard scenarios, and to make proving securityand correctness as easy as possible. The method is illustrated with a small but surprisinglyco mplex example, a copy card. The approach is implemented in the KIV specification and verification system.
http://www.informatik.uni-augsburg.de/swt/fmg/
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
J. Alves-Foss, editor. Formal Syntax and Semantics of Java. Springer LNCS 1523, 1999.
R. Anderson and R. Needham. Programming satan’s computer. In J. van Leeuwen, editor, Computer Science Today: Recent Trends and Developments. Springer LNCS 1000, 1995.
M. Balser, W. Reif, G. Schellhorn, K. Stenzel, and A. Thums. Formal system development with KIV. In T. Maibaum, editor, Fundamental Approaches to Software Engineering, number 1783 in LNCS. Springer, 2000.
B. Beckert. A dynamic logic for the formal verification of java card programs. In I. Attali and T. Jensen, editors, Java on Smart Cards. Springer LNCS 2041, 2000.
M. Burrows, M. Abadi, and R. Needham. A logic of authentication. Technical report, SRC Research Report 39, 1989.
CoFI: The Common Framework Initiative. Casl—the CoFI algebraic specification language tentative design: Language summary, 1997. http://www.brics.dk/Projects/CoFI.
R. Eshuis and R. Wieringa. A formal semantics for uml activity diagrams—formalising workflow models. Technical report, University of Twente, February 2001. http://wwwhome.cs.utwente.nl/~eshuis/adsem.pdf.
D. Harel. First Order Dynamic Logic. LNCS 68. Springer, Berlin, 1979.
International Standards Organization, Geneva. ISO 7816—Identification Cards—Integrated cicuit(s) cards with contacts. several parts, 1987–1997.
Lawrence C. Paulson. The inductive approach to verifying cryptographic protocols. Journal of Computer Security, 6:85–128, 1998.
G. Reggio, M. Cerioli, and E. Astesiano. An Algebraic Semantics of UML Supporting its Multiview Approach. In Proc. AMiLP 2000 of the Twente Workshop on Language Technology n. 16, Enschede, University of Twente, 2000.
W. Reif. The KIV-approach to Software Verification. In M. Broy and S. Jähnichen, editors, KORSO: Methods, Languages, and Tools for the Construction of Correct Software—Final Report, LNCS 1009. Springer, Berlin, 1995.
G. Schellhorn, W. Reif, A. Schairer, P. Karger, V. Austel, and D. Toll. Verification of a formal security model for multiapplicative smart cards. In Proc. of the 6 th European Symposium on Research in Computer Security (ESORICS), LNCS 1895, pages 17–36. Springer, 2000.
Kurt Stenzel. Verification of JavaCard Programs. Technical report 2001-5, Institut für Informatik, Universität Augsburg, Germany, 2001. Available at http://www.Informatik.Uni-Augsburg.DE/swt/fmg/papers/.
The Object Management Group (OMG). OMG Unified Modeling Language Specification, 1999. http://www.omg.org/technology/uml.
David von Oheimb. Axiomatic semantics for Javalight in Isabelle/HOL. In S. Drossopoulou, S. Eisenbach, B. Jacobs, G. T. Leavens, P. Müller, and A. Poetzsch-Heffter, editors, Formal Techniques for Java Programs. Technical Report 269, 5/2000, Fernuniversität Hagen, Fernuniversität Hagen, 2000.
Benkt Wangler and Lars Bergman, editors. An Overview of RoZ: A Tool for Integrating UML and Z Specifications, volume 1789 of Lecture Notes in Computer Science. Springer, 2000.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Haneberg, D., Reif, W., Stenzel, K. (2002). A Method for Secure Smartcard Applications. In: Kirchner, H., Ringeissen, C. (eds) Algebraic Methodology and Software Technology. AMAST 2002. Lecture Notes in Computer Science, vol 2422. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45719-4_22
Download citation
DOI: https://doi.org/10.1007/3-540-45719-4_22
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-44144-1
Online ISBN: 978-3-540-45719-0
eBook Packages: Springer Book Archive