CINECA IRIS Institutional Research Information System
IRIS è l’archivio della produzione scientifica della Fondazione Bruno Kessler.
EnglishThis 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.
Scheda prodotto non validato
Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte di FBK.
| Titolo: | Certification of Smart-Card Applications in Common Criteria |
| Autori: | |
| Data di pubblicazione: | 2009 |
| 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. |
| Handle: | http://hdl.handle.net/11582/5261 |
| ISBN: | 9781605581668 |
| Appare nelle tipologie: | 4.1 Contributo in Atti di convegno |
File in questo prodotto:
http://hdl.handle.net/11582/5261
Copyright © 2020