Certification of Smart-Card Applications in Common Criteria

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. T...

• Type: Conference
• Year: 2009
• Where: FASE
• Authors: Iman Narasamdya, Michaël Périn
• Keywords: Certification Process, FASE 2009, Smart-card Application Specification, Smart-card Applications, Software Engineering