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.
Chapter PDF
Similar content being viewed by others
References
J-R. Abrial and L. Mussat. Introducing Dynamic Constrains in B. In D. Bert, editor, Proceedings of the 2nd Int. B Conference, volume 1393 of LNCS. Springer, 1998.
J.R. Abrial. The B-Book. Cambridge University Press, 1996.
P. Behm and all. M’et’eor: A Successful Application of B in a Large Project. In FM’99 - Formal Methods, volume 1708 of LNCS, pages 348–387. Springer, September 1999.
N. Benaissa, D. Cansell, and D. Mery. Integration of Security Policy into System Modeling. In Julliand and Kouchnarenko [15].
D. Bert, S. Boulm’e, M-L. Potet, A. Requet, and L. Voisin. Adaptable Translator of B Specifications to Embedded C programs. In FME 2003: Formal Methods, volume 2805 of LNCS. Springer, 2003.
F. Bouquet, F. Celletti, G. Debois, A. De Lavernette, E. Jaffuel, J. Julliand, B. Legeard, J. Lidoine, J.-C. Plessis, and P.-A. Masson. Model-based security testing, application to a smart card identity applet. In eSmart 2006, 7th Int. Conf. on Smart Cards, Sophia-Antipolis, France, September 2006.
Common Criteria for Information Technology Security Evaluation, Part 2: Security functional components. Technical Report CCMB-2006-09-002, version 3.1, sept 2006.
Common Criteria for Information Technology Security Evaluation, Part 3: Security assurance components. Technical Report CCMB-2006-09-003, version 3.1, sept 2006.
Common Criteria for Information Technology Security Evaluation, version 3.1. Technical Report CCMB-2006-09-001, sept 2006.
E.W. Dijkstra. A discipline of Programming. Prentice-Hall, 1976.
The Gixel web site. http://gixel.fr.
A. Haddad. Meca: a Tool for Access Control Models. In Julliand and Kouchnarenko [15].
Smart Card Standard: Part 4: Interindustry Commands for Interchange. Technical report, ISO/IEC, 1995.
E. Jaffuel and B. Legeard. LEIRIOS Test Generator: Automated Test Generation from B Models. In Julliand and Kouchnarenko [15].
J. Julliand and O. Kouchnarenko, editors. B 2007: Formal Specification ans Development in B, volume 4355 of LNCS. Springer, 2007.
Lamport. A temporal logic of actions. ACM Transactions on Programming Languages and Systems, 16(3):872–923, may 1994.
J-L. Lanet and A. Requet. Formal Proof of Smart Card Applets Correctness. In CARDIS’98, number 1820 in LNCS. Springer, 1998.
K. Li, L. Mounier, and R. Groz. Test Generation from Security Policies Specified in Or-BAC. In COMPSAC – IEEE International Workshop on Secuirty in Software Engineering (IWSSE’07), Beijing, July 2007.
Fred B. Schneider. Enforceable security policies. ACM Trans. Inf. Syst. Secur., 3(1):30–50, 2000.
N. Stouls and M-L. Potet. Security Policy Enforcement through Refinement Process. In Julliand and Kouchnarenko [15].
J. Tretmans. Conformance testing with labelled transition systems: Implementation relations and test generation. Computer Networks and ISDN Systems, 29(1):49–79, 1996.
M. Utting and B. Legeard. Practical Model-Based Testing - A tools approach. Elsevier Science, 2006. 550 pages.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2008 IFIP International Federation for Information Processing
About this paper
Cite this paper
Dadeau, F., Potet, ML., Tissot, R. (2008). A B Formal Framework for Security Developments in the Domain of Smart Card Applications. In: Jajodia, S., Samarati, P., Cimato, S. (eds) Proceedings of The Ifip Tc 11 23rd International Information Security Conference. SEC 2008. IFIP – The International Federation for Information Processing, vol 278. Springer, Boston, MA. https://doi.org/10.1007/978-0-387-09699-5_10
Download citation
DOI: https://doi.org/10.1007/978-0-387-09699-5_10
Publisher Name: Springer, Boston, MA
Print ISBN: 978-0-387-09698-8
Online ISBN: 978-0-387-09699-5
eBook Packages: Computer ScienceComputer Science (R0)