Enforcing High-Level Security Properties for Applets

Mariela Pavlova, Gilles Barthe, Lilian Burdy, Marieke Huisman, Jean-Louis Lanet

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

12 Citations (Scopus)


Smart card applications often handle privacy-sensitive information, and therefore must obey certain security policies. Typically, such policies are described as high-level security properties, stating for example that no pin verification must take place within a transaction.

Behavioural interface specification languages, such as JML (Java Modeling Language), have been successfully used to validate functional properties of smart card applications. However, high-level security properties cannot directly be expressed in such languages. Therefore, this paper proposes a method to translate high-level security properties into JML annotations. The method synthesises appropriate annotations and weaves them throughout the application. In this way, security policies can be validated using existing tools for JML. The method is general and applies to a large class of security properties.

To validate the method, it has been applied to several realistic examples of smart card applications. This allowed us to find violations against the documented security policies for some of these applications.
Original languageEnglish
Title of host publicationSmart Card Research and Advanced Applications VI, IFIP 18th World Computer Congress, TC8/WG8.8 TC11/WG11.2 Sixth International Conference on Smart Card Research and Advanced Applications (CARDIS), 22-27 August 2004, Toulouse, France
EditorsJean-Jacques Quisquater, Pierre Paradinas, Yves Deswarte, Anas Abou El Kalam
Number of pages16
Publication statusPublished - 2004
Externally publishedYes
EventIFIP 18th World Computer Congress, WCC 2004 - Toulouse, France
Duration: 22 Aug 200427 Aug 2004
Conference number: 18

Publication series

NameIFIP International Federation for Information Processing book series


ConferenceIFIP 18th World Computer Congress, WCC 2004
Abbreviated titleWCC 2004


Dive into the research topics of 'Enforcing High-Level Security Properties for Applets'. Together they form a unique fingerprint.

Cite this