We present a method for proving representation correspondences in the Common Criteria (CC) certification of smart-card applications. For security policy enforcement, the CC defines a chain of requirements: a security policy model (SPM), a functional specification (FSP), and a target-of-evaluation design (TDS). In our approach to the CC certification, these requirements are models of applications that can have different representations. A representation correspondence (RCR) describes a correlation between the representations of two adjacent requirements. One task in the CC certification is to demonstrate formal proofs of RCRs. We first develop a modelling framework by which the representations of SPM, FSP and TDS can be described uniformly as models of an application. We then define RCRs as mutual simulations between two application models over sets of observable events and variables. We describe a proof technique for proving RCRs and providing certificates about them based on assertions relating two models at specific locations. We show how RCRs can help us prove property preservation from the SPM to the FSP and the TDS.

Certification of Smart-Card Applications in Common Criteria: Proving Representation Correspondences

Narasamdya, Iman;
2009

Abstract

We present a method for proving representation correspondences in the Common Criteria (CC) certification of smart-card applications. For security policy enforcement, the CC defines a chain of requirements: a security policy model (SPM), a functional specification (FSP), and a target-of-evaluation design (TDS). In our approach to the CC certification, these requirements are models of applications that can have different representations. A representation correspondence (RCR) describes a correlation between the representations of two adjacent requirements. One task in the CC certification is to demonstrate formal proofs of RCRs. We first develop a modelling framework by which the representations of SPM, FSP and TDS can be described uniformly as models of an application. We then define RCRs as mutual simulations between two application models over sets of observable events and variables. We describe a proof technique for proving RCRs and providing certificates about them based on assertions relating two models at specific locations. We show how RCRs can help us prove property preservation from the SPM to the FSP and the TDS.
9783642005923
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: http://hdl.handle.net/11582/5260
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
social impact