HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Conference papers

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 Nancy - Grand Est, LORIA - FM - Department of Formal Methods
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 metadata

Contributor : Frédéric Dadeau Connect in order to contact the contributor
Submitted on : Monday, October 13, 2008 - 5:11:29 PM
Last modification on : Friday, January 21, 2022 - 3:08:59 AM



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⟩



Record views