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