PACAP project

Content

Project overview
Participants
Case study
Reports, papers and presentations

Project overview

The goal of the project was to provide techniques and tools enabling a smart card issuer to verify that a new applet securely interacts with already downloaded applets. A security policy has been defined that associates levels to applet attributes and methods and defines authorized flows between levels. We propose a technique based on mdeol checking to verify that actual information flows between applets are authorized. The approach is applied to a case study (an electronic purse running on Java enabled smart cards).

Participants

Project partners :
- Gemplus
- Centre d'Étude et de Recherche de Toulouse de l'Office National d'Étude et de Recherche en Aéronautique.
Duration : 2 years from january 1999 to december 2000.
Supported by: ministère de la recherche and STTC.
Gemplus : Thierry Bressure, Eric Bretagne, Pierre Girard, Jean-Louis Lanet, Abdellah El Marouani.
ONERA : Pierre Bieber, Jacques Cazin, Virginie Wiels, Guy Zanon.

Case study: electronic purse

See this web page describing the case study (specifications, code and models available).

Reports, papers and presentations

P.Bieber, J.Cazin, P.Girard, JL.Lanet, V.Wiels, G.Zanon, Checking secure interactions of smart card applets. Proceedings of Esorics 2000. To be published in the LNCS serie , Copyright Springer-Verlag. Paper [ ps].
P.Bieber, J.Cazin, A. El Marouani, P.Girard, JL.Lanet, V.Wiels, G.Zanon, The PACAP prototype: a tool for detecting Java card illegal flow. Java Card Forum 2000, September 2000, Cannes, France. Paper [ps]
P.Bieber, J.Cazin, A. El Marouani, P.Girard, JL.Lanet, R. Muller, V.Wiels, G.Zanon, Detecting illegal information flow using abstract interpretation and model checking. Gemplus Developer Conference 2000, Juin 2000, Montpellier, France. Paper [ps]
P.Bieber, J.Cazin, V.Wiels, G.Zanon, P.Girard, JL.Lanet, Electronic Purse Applet Certification: Extended abstract. Proceedings of the workshop on secure architectures and information flow, Royal Holloway, 1-3 decembre 99. Electronic Notes in Theoretical Computer Science. Paper [ ps].
Electronic Purse Applet Certification. INRIA Javacard day, ENS, 8 december 99 and workshop on secure architectures and information flow, Royal Holloway, 1-3 decembre 99. Slides [ ppt].
Pierre Girard, Jean-Louis Lanet, Java Card or How to Cope with the New Security Issues Raised by Open Cards? Gemplus Developer Conference 99, June 21-22 1999, Paris, France. Paper [PDF, 140 Ko] - Présentation [PDF, 3298 Ko ].
Thierry Bressure, Conception et implémentation d'applications Java sur carte à puce, Rapport de DEA, 22 juin 1999. Rapport [PDF, 269 Ko]. Présentation [PDF, 3291 Ko ].
Thierry Bressure, PACAP : Implémentation du cas d'étude. Quarterly du groupe cryptographie et sécurité, 31 Mai 1999. [PDF, 2878 Ko]
Pierre Girard and Jean Louis Lanet, "New security issues raised by open cards," Information Security Technical Report, 1999. To appear. Paper [PDF, 104 Ko] - BibTeX entry.
Pierre Girard, "Which security policy for multiapplication smart cards?," in USENIX Workshop on Smartcard Technology, May 10--11, 1999, Chicago, Illinois, USA, pp. 21--28, May 1999. To appear. Paper [PDF, 147 Ko ] - BibTeX entry.