skip to main content
10.1145/1529282.1529409acmconferencesArticle/Chapter ViewAbstractPublication PagessacConference Proceedingsconference-collections
research-article

Certification of smart-card applications in common criteria

Published: 08 March 2009 Publication History

Abstract

This paper describes the certification of smart-card applications in the framework of Common Criteria. In this framework, a smart-card application is represented by a model of its specification, a functional specification describing an input-output relationship, a low-level design, and implementation code. The certification process consists of the following tasks: (1) prove that the model, the functional specification, the low-level design, and the code satisfy security properties in the smart-card application's specification, and (2) prove that there is a representation correspondence between each two consecutive representations. For each task, a certificate or a collection of certificates are needed to certify the accomplishment of the task. All representations of a smart-card application are essentially programs and the representation correspondences are properties relating two programs. We show that a theory of program properties can be applied to the certification process. The theory provides foundations for describing and proving properties of a single program and properties relating two programs. The theory provides a notion of certificate that is essential to the certification process.

References

[1]
Common Criteria for Information Technology Security Evaluation, 2007. Version 3.1, CCMB-2007-09-003.
[2]
C.-B. Breunesse, N. Cataño, M. Huisman, and B. Jacobs. Formal methods for smart cards: an experience report. Sci. Comput. Program., 55(1--3): 53--80, 2005.
[3]
Robert W. Floyd. Assigning meaning to programs. In J. T. Schwartz, editor, Proceedings of Symposium in Applied Mathematics, pages 19--32, 1967.
[4]
Constance L. Heitmeyer, Myla Archer, Elizabeth I. Leonard, and John McLean. Formal specification and verification of data separation in a separation kernel for an embedded system. In CCS '06: Proceedings of the 13th ACM conference on Computer and communications security, pages 346--355, New York, NY, USA, 2006. ACM.
[5]
C. A. R. Hoare. An axiomatic basis for computer programming. CACM, 12(10): 576--580, 1969.
[6]
E.-M.G.M. Hubbers and E. Poll. Reasoning about card tears and transactions in Java Card. In M. Wermelinger and T. Margaria-Steffen, editors, Fundamental Approaches to Software Engineering, 7th International Conference, FASE 2004, volume 2984 of LNCS, pages 114--128. Springer-Verlag, 2004.
[7]
E.-M.G.M. Hubbers and E. Poll. Transactions and non-atomic API methods in Java Card: specification ambiguity and strange implementation behaviors. Technical Report NIII R0438, University of Nijmegen, Toernooiveld, 6525 ED Nijmegen, The Netherlands, October 2004.
[8]
Iman Narasamdya and Michaël Périn. Certification of smart-card applications in common criteria. Technical Report TR-2008-14, Verimag, September 2008.
[9]
Sun Micro systems, Inc, Palo Alto, California. Java Card 3.0 Platform Specification, 2008. http://java.sun.com/javacard/3.0/.
[10]
Andrei Voronkov and Iman Narasamdya. Proving inter-program properties. Technical Report TR-2008-13, Verimag, September 2008.

Cited By

View all
  • (2012)Supporting Software Evolution for Open Smart Cards by Security-by-ContractDependability and Computer Engineering10.4018/978-1-60960-747-0.ch013(285-305)Online publication date: 2012
  • (2011)A Load Time Policy Checker for Open Multi-application Smart CardsProceedings of the 2011 IEEE International Symposium on Policies for Distributed Systems and Networks10.1109/POLICY.2011.40(153-156)Online publication date: 6-Jun-2011
  • (2009)Inter-program PropertiesStatic Analysis10.1007/978-3-642-03237-0_23(343-359)Online publication date: 2009
  • Show More Cited By

Index Terms

  1. Certification of smart-card applications in common criteria

      Comments

      Information & Contributors

      Information

      Published In

      cover image ACM Conferences
      SAC '09: Proceedings of the 2009 ACM symposium on Applied Computing
      March 2009
      2347 pages
      ISBN:9781605581668
      DOI:10.1145/1529282
      Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

      Sponsors

      Publisher

      Association for Computing Machinery

      New York, NY, United States

      Publication History

      Published: 08 March 2009

      Permissions

      Request permissions for this article.

      Check for updates

      Author Tags

      1. assertion functions
      2. assertions
      3. common criteria certification
      4. invariants
      5. smart-card applications
      6. specification techniques

      Qualifiers

      • Research-article

      Conference

      SAC09
      Sponsor:
      SAC09: The 2009 ACM Symposium on Applied Computing
      March 8, 2009 - March 12, 2008
      Hawaii, Honolulu

      Acceptance Rates

      Overall Acceptance Rate 1,650 of 6,669 submissions, 25%

      Upcoming Conference

      SAC '25
      The 40th ACM/SIGAPP Symposium on Applied Computing
      March 31 - April 4, 2025
      Catania , Italy

      Contributors

      Other Metrics

      Bibliometrics & Citations

      Bibliometrics

      Article Metrics

      • Downloads (Last 12 months)5
      • Downloads (Last 6 weeks)0
      Reflects downloads up to 19 Feb 2025

      Other Metrics

      Citations

      Cited By

      View all
      • (2012)Supporting Software Evolution for Open Smart Cards by Security-by-ContractDependability and Computer Engineering10.4018/978-1-60960-747-0.ch013(285-305)Online publication date: 2012
      • (2011)A Load Time Policy Checker for Open Multi-application Smart CardsProceedings of the 2011 IEEE International Symposium on Policies for Distributed Systems and Networks10.1109/POLICY.2011.40(153-156)Online publication date: 6-Jun-2011
      • (2009)Inter-program PropertiesStatic Analysis10.1007/978-3-642-03237-0_23(343-359)Online publication date: 2009
      • (2009)Certification of Smart-Card Applications in Common CriteriaFundamental Approaches to Software Engineering10.1007/978-3-642-00593-0_21(309-324)Online publication date: 2009

      View Options

      Login options

      View options

      PDF

      View or Download as a PDF file.

      PDF

      eReader

      View online with eReader.

      eReader

      Figures

      Tables

      Media

      Share

      Share

      Share this Publication link

      Share on social media