Formalisation and Verification of the GlobalPlatform Card Specification Using the B Method

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.

Zanella.2006.CASSIS.pdf
PDF file

In  2nd International Workshop on Construction and Analysis of Safe, Secure, and Interoperable Smart Devices, CASSIS 2005

Publisher  Springer

Details

TypeInproceedings
URLhttp://dx.doi.org/10.1007/11741060_9
Pages155-173
Volume3956
SeriesLecture Notes in Computer Science
> Publications > Formalisation and Verification of the GlobalPlatform Card Specification Using the B Method