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.
Document type :
Conference papers
Complete list of metadatas

https://hal.inria.fr/inria-00329973
Contributor : Frédéric Dadeau <>
Submitted on : Monday, October 13, 2008 - 5:11:29 PM
Last modification on : Friday, July 6, 2018 - 3:06:09 PM

Identifiers

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. pp.141-155, ⟨10.1007/978-0-387-09699-5⟩. ⟨inria-00329973⟩

Share

Metrics

Record views

370