Formal Model of GlobalPlatform Card Specification v2.1.1 Completed
Card Specification Model Based on Formal Logic Now Available at www.globalplatform.org
2 November 2004 – A formal model of the GlobalPlatform Card Specification v2.1.1 has been developed by the EVEREST Project team at the French Institute for Research in Computer Science and Automation (INRIA) and is now available, royalty free, at www.globalplatform.org.
The formal model provides an abstract reference implementation of the card specification, by defining it using formal logic and thereby eliminating any ambiguity that may exist in the natural English language used in the documentation.
The model will also potentially facilitate GlobalPlatform’s future development of functional tests for the specification by automating the generation of tests and will allow card vendors to derive high level security evaluations of their GlobalPlatform compliant card products.
Marc Kekicheff, GlobalPlatform’s Technical Director and Chair of the GlobalPlatform Card Committee, comments: “This formal model is a useful tool for anyone wishing to implement the GlobalPlatform Card Specification v2.1.1, as it provides a rigorous and unambiguous description of the specification using an abstract language based on formal logic.
“It is also of extreme value to GlobalPlatform because it offers formal proof of our Card Specification as well as the potential automation of the generation of our compliance tests. Currently, the GlobalPlatform Card Committee generates these test suites manually, so an automated system will expedite this process and make it less time consuming.
“The model will strengthen security evaluations of GlobalPlatform cards. We hope that it will eventually end up supporting the highest levels of security evaluations such as Common Criteria EAL6 or EAL7. On behalf of GlobalPlatform, I’d like to offer thanks to INRIA for their efforts on this project.”
Gilles Kahn, CEO of INRIA, adds: “Our collaboration with GlobalPlatform is a perfect illustration that formal verification techniques, emerging from fundamental research, may bring a deeper understanding and increase confidence in complex security architectures that are widely used in industry.”
For further information on GlobalPlatform, please visit www.globalplatform.org
For further information on INRIA, please visit www.inria.fr
For further media information on GlobalPlatform, contact Lee’ann Connell at Sinclair Mason on Tel: + 44 (0) 113 237 0777 or e-mail: firstname.lastname@example.org
For further media information on INRIA, please contact Rose-Marie Cornus on Tel: + 33 4 92 38 76 27 or e-mail: email@example.com
NOTES TO EDITORS:
GlobalPlatform is the global leader in smart card infrastructure development and its proven, technical specifications for cards, devices and systems are known as the standard for smart card infrastructure. GlobalPlatform has over 50 cross-industry members with representation from all world continents.
INRIA, the national institute for research in computer science and control, is dedicated to fundamental and applied research in information and communication science and technology (ICST). Throughout its six research units located in nine major regions*, the Institute has a workforce of 3,200, 2,250 of whom are scientists from INRIA and its partner organizations. INRIA has an annual budget of 125 million euros, one quarter of which comes from its own research contracts and development products. The Institute plays a crucial role in five areas of research: communicating systems, cognitive systems, symbolic systems, numerical systems and biological systems.
INRIA develops many partnerships with industry and fosters technology transfer and company foundation in the field of ICST – some seventy companies have been founded. Startups are financed in particular by INRIA-Transfert, a subsidiary of INRIA that supports four startup funds, for it, multimedia and telecommunications.
The international collaborations are based on an incentive strategy of welcoming and recruiting foreign students as well as developing strong exchanges between research scientists. Priority is given to geographic zones with strong growth: Europe, Asia and North America while maintaining reasonable cooperation with South America, Africa and Middle-East.
* Aquitaine, Bretagne, Lorraine et Franche Comté, Île-de-France, Nord Pas de Calais, Provence Alpes Côte d’Azur et Languedoc Roussillon, Rhône-Alpes.