A Verifiable Conformance Relationship between Smart Card Applets and B security Models

Frédéric Dadeau 1 Julien Lamboley 2 Thierry Moutet 2 Marie-Laure Potet 2
1 CASSIS - Combination of approaches to the security of infinite states systems
FEMTO-ST - Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies (UMR 6174), INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : We propose a formal framework based on the B method, that supports the development of secured smart card applications. Accordingly to the Common Criteria methodology, we start from a formal definition and modelling of security policies, as access control policies. At the end of the development process, smart card applications are implemented in a standardized way, based on both the life cycle of smart card applets and the APDU protocol. In this paper, we define a conformance relationship that aims at establishing how smart card applications can be related to security requirement models. This embraces both the notions of security conformance as well as traceability allowing to relate basic events appearing at the level of applications with abstract security policies. This approach has been developed in the RNTL POS´E project1, involving a smart card issuer, Gemalto.
Type de document :
Communication dans un congrès
Egon Börger, Michael Butler, Jonathan P. Bowen and Paul Boca. First International Conference on ASM, B and Z - ABZ'08, Sep 2008, London, United Kingdom. Springer Berlin / Heidelberg, 5238, pp.237-250, 2008, Lecture Notes in Computer Science. 〈10.1007/978-3-540-87603-8〉
Liste complète des métadonnées

https://hal.inria.fr/inria-00329966
Contributeur : Frédéric Dadeau <>
Soumis le : lundi 13 octobre 2008 - 17:06:50
Dernière modification le : vendredi 6 juillet 2018 - 15:06:09

Lien texte intégral

Identifiants

Citation

Frédéric Dadeau, Julien Lamboley, Thierry Moutet, Marie-Laure Potet. A Verifiable Conformance Relationship between Smart Card Applets and B security Models. Egon Börger, Michael Butler, Jonathan P. Bowen and Paul Boca. First International Conference on ASM, B and Z - ABZ'08, Sep 2008, London, United Kingdom. Springer Berlin / Heidelberg, 5238, pp.237-250, 2008, Lecture Notes in Computer Science. 〈10.1007/978-3-540-87603-8〉. 〈inria-00329966〉

Partager

Métriques

Consultations de la notice

293