This book constitutes the refereed proceedings of the Second International Conference on Research in Smart Cards, E-smart 2001, held in Cannes, France, in September 2001. The 20 revised full papers presented were carefully reviewed and selected from 38 submissions. Among the topics addressed are biometrics, cryptography and electronic signatures on smart card security, formal methods for smart card evaluation and certification, architectures for multi-applications and secure open platforms, and middleware for smart cards and novel applications of smart cards.

Smart cards are playing an increasingly important role in areas such as ban- 1 king,electroniccommerce,andtelecommunications. TheJavaCard language hasbeenproposedasahigh-levellanguageforprogrammingmulti-application smartcards. Theuseofahigh-levellanguagecanfacilitatethedevelopmentand veri?cation of software for smart cards. The modest code size and the imp- tanceoftheapplicationareasimpliesthatitisbothpossibleanddesirableto developandapplyformalmethodsintheconstructionofsafeandsecureJava Cardsoftware. ThepresentvolumeconstitutestheproceedingsoftheJavaCardworkshop heldinCannes,14September2000. TheworkshopgrewoutoftheINRIAAction deRechercheCoop'erative"JavaCard"andwasorganizedincollaborationwith the Java Card Forum. A call for papers resulted in 14 submissions of which theprogramcommitteeselected11papersforpresentationattheworkshop. In addition,theworkshopfeaturedaninvitedtalkbyDanielLeM'etayer,Trusted Logic,onformalmethodsandsmartcardsecurity. WewishtothankCatherine Godest and Maryse Renaud for their help with preparing the proceedings for thisworkshop. February2001IsabelleAttali ThomasJensen 1 ItshouldbenotedthatJavaCardisatrademarkofSunMicrosystems. Organization ProgramCommittee ProgramChair: IsabelleAttali(INRIA,France) ThomasJensen(IRISA/CNRS,France) Committeemembers: ChristianGoire(BullCP8,France) SebastianHans(SunMicrosystems,USA) PieterHartel(UniversityofSouthampton,UK) PeterHoneyman(UniversityofMichigan,USA) PierreParadinas(Gemplus,France) JoachimPosegga(SAPCorporateResearch,Germany) TableofContents InvitedTalk FormalMethodsinContext:SecurityandJavaCard ...1 D. Bolignano,D. LeM'etayer,C. Loiseaux ContributedPapers ADynamicLogicfortheFormalVeri?cationofJavaCardPrograms ...6 BernhardBeckert ThePACAPPrototype:AToolforDetectingJavaCardIllegalFlow ...25 P. Bieber,J. Cazin,A. ElMarouani,P. Girard,J. -L. Lanet,V. Wiels, G. Zanon CardKt:AutomatedMulti-modalDeductiononJavaCardsfor Multi-applicationSecurity...38 RajeevGor'e,LanDuyNguyen A Programming and a Modelling Perspective on the Evaluation of Java CardImplementations...52 PieterH. Hartel,EduarddeJong SecureInternetSmartcards...73 NaomaruItoi,TomokoFukuzawa,PeterHoneyman IssuesinSmartcardMiddleware...90 RogerKehr,MichaelRohs,HaraldVogt OpenPlatfomSecurity ...98 MarcKekiche?,ForoughKashef,DavidBrewer ASimple(r)InterfaceDistributionMechanismforJavaCard ...1 14 KsheerabdhiKrishna,MichaelMontgomery AutomaticTestGenerationforJavaCardApplets ...121 HuguesMartin,LydieduBousquet FormalSpeci?cationandVeri?cationofJavaCard'sApplicationIdenti?er Class...137 JoachimvandenBerg,BartJacobs,ErikPoll X TableofContents Security on Your Hand: Secure Filesystems with a "Non-cryptographic" JAVA-Ring...151 R..udigerWeis,BastiaanBakker,StefanLucks AuthorIndex ...163 Formal Methods in Context: Security and Java Card D. Bolignano, D. Le Metayer, and C. Loiseaux Trusted Logic www. trusted-logic. fr 1. Security and Java Card: An Ideal Application Area for Formal Methods The benefits of formal methods for software engineering have been described at length in many research papers. They include among others: Better understanding and improved communication through unambiguous descriptions. Early bug detection thanks to the formalisation of specifications.