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

Frédéric Dadeau, Julien Lamboley, Thierry Moutet, Marie-Laure Potet
Digital Printed Abstract View Cite
Type
Conference paper
Publication
1st International Conference on ASM, B, and Z (ABZ'08)

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É project, involving a smart card issuer, Gemalto.

Document

If you cannot see the document below, the PDF document is most likely not freely accessible. In this case, please try to access the document via this link.

Reference

% BibTex
@inproceedings{DadeauLMP08,
  author       = {Fr{\'{e}}d{\'{e}}ric Dadeau and
                  Julien Lamboley and
                  Thierry Moutet and
                  Marie{-}Laure Potet},
  editor       = {Egon B{\"{o}}rger and
                  Michael J. Butler and
                  Jonathan P. Bowen and
                  Paul Boca},
  title        = {A Verifiable Conformance Relationship between Smart Card Applets and
                  {B} Security Models},
  booktitle    = {Abstract State Machines, {B} and Z, First International Conference,
                  {ABZ} 2008, London, UK, September 16-18, 2008. Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {5238},
  pages        = {237--250},
  publisher    = {Springer},
  year         = {2008},
  url          = {https://doi.org/10.1007/978-3-540-87603-8\_19},
  doi          = {10.1007/978-3-540-87603-8\_19},
  timestamp    = {Tue, 14 May 2019 10:00:50 +0200},
  biburl       = {https://dblp.org/rec/conf/asm/DadeauLMP08.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}
ABZ'08

Related