A B Formal Framework for Security Developments in the Domain of Smart Card Applications

Frédéric Dadeau 1 Régis Tissot 2 Marie-Laure Potet 3
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 in this paper a formal framework based on the B method, that supports the development of secured smart card applications. Accordingly to the Common Criteria methodology, we focus on the formal definition and modelling of access control policies by means of dedicated B models expressing, on one hand, the access control rules, and, on the other hand, the dynamics of the system. These models are then weaved to produce a security kernel. From there, we propose a conformance relationship that aims at establishing whether a concrete representation of the system complies, at the security level, with the security kernel. This embraces both a well-defined notion of security conformance as well as traceability allowing to relate basic events appearing at the level of applications with abstract security policies. This approach is put in practice on an industrial case study in the context of the POSé project, involving both academic and industrial partners.
Type de document :
Communication dans un congrès
23rd International Information Security Conference - SEC'08, Sep 2008, Milano, Italy. Springer, 278, pp.141-155, 2008, IFIP. 〈10.1007/978-0-387-09699-5〉
Liste complète des métadonnées

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

Identifiants

Citation

Frédéric Dadeau, Régis Tissot, Marie-Laure Potet. A B Formal Framework for Security Developments in the Domain of Smart Card Applications. 23rd International Information Security Conference - SEC'08, Sep 2008, Milano, Italy. Springer, 278, pp.141-155, 2008, IFIP. 〈10.1007/978-0-387-09699-5〉. 〈inria-00329973〉

Partager

Métriques

Consultations de la notice

311