Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
Formalisation and Verification of the GlobalPlatform Card Specification Using the B Method

Santiago Zanella-B├ęguelin

Abstract

We give an overview of an application of the B method to the formalisation and verification of the GlobalPlatform Card Specification. Although there exists a semi-formal specification and some effort has been put into providing formalisations of particular features of smart card platforms, this is, as far as we know, the very first attempt to provide a complete formalisation. We describe the process followed to synthesise a mathematical model of the platform in the B language, starting from requirements stated in natural language. The model consistency has been thoroughly verified using formal techniques supported by the B method. We also discuss how the smart card industry might benefit from exploiting this formal specification and outline directions for future work.

Details

Publication typeInproceedings
Published in2nd International Workshop on Construction and Analysis of Safe, Secure, and Interoperable Smart Devices, CASSIS 2005
URLhttp://dx.doi.org/10.1007/11741060_9
Pages155-173
Volume3956
SeriesLecture Notes in Computer Science
PublisherSpringer
> Publications > Formalisation and Verification of the GlobalPlatform Card Specification Using the B Method