- Aktuell

- Suche

- Kontakt

Go!Card

Smart cards - But only if secure!

Health insurance cards, phonecards, money cards - nowadays practically everyone has chip cards in his wallet. Most of these cards are simple memory cards, used as portable storage devices. In contrast to that, the german money card ("Geldkarte") and the Subscriber Identity Module (SIM) used in cellular phones are so called smart cards.The main characteristics of the smart cards is that they contain a small microprocessor. Thereby they can conduct calculations independently and secret information doesn't need to be disclosed in order to be processed. Therefore they are well-suited as storage for secrets or the electronic representation of economic goods and have to deal with lots of security threats. For example, customers want anonymity and protection against the loss of the digital economic goods, the service providers don't want the digital goods to be copied or manipulated.

The Go!Card project investigates methods for the development of secure smart card applications. Our goal is to provide a development method that guarantees the security of the smart card application to the best currently possible degree. The main building blocks of our method are:
  • a modelling method for smart card application scenarios using UML
  • a formal specification method using Abstract State Machines (ASM)
  • proof methodology for security properties and
  • tool support using KIV, our interactive theorem prover

The GoCard project was part of the DFG research grant "Sicherheit in der Informations- und Kommunikationstechnik"

The project is already quite elaborated and we accomplished a lot of our goals. Especially, three doctoral theses were written in the context of this project. One concerns specification, verification and modelling of smart card applications and therefore introduces the Prosecco (Protocols for Secure Communication) methodology. This is the work of Dr. Dominik Haneberg. His thesis (in German) is called "Sicherheit von Smart Card-Anwendungen" and published as a book (ISBN: 978-3-8325-1597-3). As an example of the work of Dr. Haneberg, you can take a look at the specification and modeling approach for smart card application scenarios, as well as at one of our examples, an e-commerce scenario for the sale and use of electronic tickets.

The next thesis is the work of Dr. Kurt Stenzel, which can be found here. He introduced a Calculus and Semantics for the sequential part of the Java programming language in the KIV system. This calculus was used in all our case studies for Java verification. The calculus is an extension to the calculus for the programs of dynamic logic, which were already supported by the KIV prover. The calculus is capable of verifying all sequential language constructs of the Java programming language, no abstraction is being made.

Last but not least the GoCard project aims at the verification of functional correctness and security of real running applications. We dont only want to verify abstract specifications of security protocols, but also prove that concrete implementations preserve security properties. Therefore we developed a refinement method for abstract security protocol specifications down to Java code. Security is proven on the abstract level and inherited to the implementation in terms of formal refinement. The refinement approach us using ASM Refinement and the Java Calculus mentioned above. The refinement framework is the work of Dr. Holger Grandy. His thesis is called "Formale Verifikation der Korrektheit sicherheitskritischer Java Anwendungen". It can be viewed here. There is also a special KIV projects page just for the results of the thesis.

The most comprehensive apporach to formal protocol verification done by us was the Mondex Case Study, whose tool assisted verification was announced in 2006 as one of Grand Challenges in Computing. The original case study was done by Cooper, Stepney and Woodcock in the Z specification language and using pen and paper proofs in 2000. We (amoung others) verified four layers of abstraction in the Mondex case study using the KIV prover and ASMs as the specification language, starting at very abstract specifications and continuing down to verified and running Java source code. We thereby extended the original Mondex case study by two layers: specification of cryptographic functions and a protocol using them as well as the Java implementation level. All our Mondex related projects are on this website. The Mondex work in KIV was mainly done by Dr. Gerhard Schellhorn, Dr. Dominik Haneberg, Dr. Holger Grandy and Markus Bischof.

Contacts

Case Studies

A browsable representation of the formal specifications as well as the theorem bases and the proofs of some of our recent case studies, which were verified with the KIV system, can be found on our KIV projects page.

All our Mondex related projects are on this website.

Papers

  • Verification of Java Programs with Generics
    Kurt Stenzel, Holger Grandy, Wolfgang Reif
    (accepted at AMAST'08, to appear in Springer LNCS)
    abstract; Verification of Java Programs with Generics (151 KB);
  • A Concept-Driven Construction of the Mondex Protocol using Three Refinements
    Gerhard Schellhorn, Richard Banach
    (accepted at ABZ 2008, to appear in Springer LNCS)
    abstract;
  • Formale Verifikation der Korrektheit sicherheitskritischer Java Anwendungen
    H. Grandy
    Dissertation, Fakultät für Angewandte Informatik, Universität Augsburg, 2008
    abstract; dissertation-grandy
  • Verification of Mondex Electronic Purses with KIV: From a Security Protocol to Verified Code
    H. Grandy, M. Bischof, K. Stenzel, G. Schellhorn, W. Reif
    FM 2008, 15th International Symposium on Formal Methods, Springer LNCS 5018
    abstract SpringerLink;
  • Verification of Mondex electronic purses with KIV: from transactions to a security protocol
    D. Haneberg, G. Schellhorn, H. Grandy, W. Reif
    Formal Aspects of Computing (2008) 20:41-59, Springer
    abstract;     SpringerLink;
  • A Modeling Framework for the Development of Provably Secure E-Commerce Applications
    Nina Moebius, Dominik Haneberg, Wolfgang Reif, Gerhard Schellhorn
    Proceedings of the International Conference on Software Engineering Advances 2007, IEEE Computer Society Press
    **** Best Paper Award ****
    abstract; IEEExlpore;
  • Verifying Smart Card Applications: An ASM Approach.
    D. Haneberg, H. Grandy, W. Reif, G. Schellhorn
    Proceedings of the conference on integrated Formal Methods 2007 (iFM 2007), Springer LNCS 4591, Springer
    abstract; SpringerLink
  • On the Refinement of Atomic Actions
    Richard Banach and Gerhard Schellhorn
    ENTCS vol. 201, p. 3-33 Proceedings of the conference on integrated Formal Methods 2007 (iFM 2007), Springer LNCS 4591, Springer
    abstract; sciencedirect
  • ASN1-light: A Verified Message Encoding for Security Protocols
    Holger Grandy, Robert Bertossi, Kurt Stenzel, Wolfgang Reif
    Proceedings of SEFM 2007, Springer LNCS, London, England
    abstract     IEEExplore;
  • A Systematic Verification Approach for Mondex Electronic Purses using ASMs
    Gerhard Schellhorn, Holger Grandy, Dominik Haneberg, Nina Moebius, Wolfgang Reif
    Proceedings of the Dagstuhl Seminar on Rigorous Methods for Software Construction and Analysis, Springer, LNCS
    abstract
  • A Refinement Method for Java Programs
    Holger Grandy, Kurt Stenzel, Wolfgang Reif
    Proceedings of FMOODS 2007, Springer LNCS 4468, Paphos, Cyprus,
    abstract;     SpringerLink;
  • Verification of Mondex Electronic Purses with KIV: From Transactions to a Security Protocol
    Dominik Haneberg, Gerhard Schellhorn, Holger Grandy, Wolfgang Reif
    Formal Aspects of Computing, 2007
    abstract      SpringerLink;
  • Verification of Mondex Electronic Purses with KIV: From Transactions to a Security Protocol
    D. Haneberg, G. Schellhorn, H. Grandy, W. Reif
    Technical Report, Institute of Computer Science, University of Augsburg, December 2006
    abstract; Verification of Mondex Electronic Purses with KIV: From Transactions to a Security Protocol (284 KB)
  • Reasoning about Pointer Structures in Java
    Kurt Stenzel, Holger Grandy, Wolfgang Reif
    Technical Report, Institute of Computer Science, University of Augsburg, December 2006
    abstract; Reasoning about Pointer Structures in Java (202 KB);
  • The Mondex Case Study: From Specifications to Code
    H. Grandy, N. Moebius, M. Bischof, D. Haneberg, G. Schellhorn, K. Stenzel, W. Reif
    Technical Report, Institute of Computer Science, University of Augsburg, December 2006
    abstract; The Mondex Case Study: From Specifications to Code (445 KB);
  • A Refinement Method for Java Programs
    Holger Grandy, Kurt Stenzel, Wolfgang Reif
    Technical Report, Institute of Computer Science, University of Augsburg, December 2006
    abstract; A Refinement Method for Java Programs (219 KB);
  • A Systematic Verification Approach for Mondex Electronic Purses using ASMs
    G. Schellhorn, H. Grandy, D. Haneberg, N. Moebius, W. Reif
    Technical Report, Institute of Computer Science, University of Augsburg
    abstract; A Systematic Verification Approach for Mondex Electronic Purses using ASMs (279 KB);
  • The Mondex Challenge: Machine Checked Proofs for an Electronic Purse
    Gerhard Schellhorn, Holger Grandy, Dominik Haneberg, Wolfgang Reif
    Proceedings of FM 2006: Formal Methods 14th International Symposium on Formal Methods Hamilton, Canada, August 21-27, 2006, Springer LNCS 4085, Springer
    abstract;
  • Refinement of Security Protocol Data Types to Java
    Holger Grandy, Kurt Stenzel, Wolfgang Reif
    PASSWORD at ECOOP 2006, Nantes, France, July 2006
    abstract; 2006-password (0 KB)
  • Developing Provable Secure M-Commerce Applications
    Holger Grandy, Dominik Haneberg, Wolfgang Reif, Kurt Stenzel
    Emerging Trends in Information and Communication Security, Proceedings. Springer LNCS 3995, 2006.
    abstract
  • Verifying Smart Card Applications: An ASM Approach.
    Dominik Haneberg, Holger Grandy, Wolfgang Reif, Gerhard Schellhorn
    Technical Report, Institute of Computer Science, University of Augsburg
    abstract; download PDF version (767 KB);
  • The Mondex Challenge: Machine Checked Proofs for an Electronic Purse
    G. Schellhorn, H. Grandy, D. Haneberg, W. Reif
    Technical Report, Institute of Computer Science, University of Augsburg
    abstract; The Mondex Challenge: Machine Checked Proofs for an Electronic Purse (0 KB);
  • Object Oriented Verification Kernels for Secure Java Applications
    Holger Grandy, Kurt Stenzel, Wolfgang Reif
    Proceedings of the 3rd International Conference on Software Engineering and Formal Methods - SEFM 2005, September 2005, IEEE Press.
    abstract; 2005-sefm-verification-kernels (0 KB);
  • Verification of Java Card Programs
    Kurt Stenzel
    Dissertation, Fakultät für Angewandte Informatik, Universität Augsburg, 2005
    abstract; download pdf version (1110 KB)
  • ASM Refinement and Generalizations of Forward Simulation in Data Refinement: A Comparison
    G. Schellhorn
    Theoretical Computer Science, Vol. 336, No. 2-3, pp. 403-436
    abstract; download pdf draft (266 KB); download postscript draft (514 KB)
  • Verifying Security Protocols: An ASM Approach.
    Dominik Haneberg, Holger Grandy, Wolfgang Reif, Gerhard Schellhorn
    Proceedings of the 12th International Workshop on Abstract State Machines (ASM 2005)
    download pdf version (193 KB);
  • A Formally Verified Calculus for Full Java Card
    K. Stenzel
    C. Rattray, S. Maharaj, and C. Shankland (editors), Algebraic Methodology and Software Technology (AMAST) 2004 Proceedings. Stirling Scotland, July 2004. Springer LNCS 3116
    download pdf version (239 KB); download postscript version (221 KB); bibentry;
  • Electronic-Onboard-Ticketing: Software Challenges of an State-of-the-Art M-Commerce Application
    D. Haneberg, W. Reif, K. Stenzel
    K. Pousttchi, K. Turowski (Hrsg.), Mobile Economy - Transaktionen, Prozesse, Anwendungen und Dienste, Proceedings zum 4. Workshop Mobile Commerce, Lecture Notes in Informatics Vol. P-42
    download pdf version (58 KB); bibentry;
  • Design for Trust: Security im M-Commerce
    D. Haneberg, A. Kreibich, W. Reif, K. Stenzel
    K.P. Jantke, W. S. Wittig, J. Herrmann (Hrsg.), Von e-Learning bis e-Payment 2003 - Tagungsband LIT '03, Akademische Verlagsgesellschaft Aka Berlin
    bibentry;