Compositional Verification of Secure Applet Interactions

Gilles Barthe, Dilian Gurov, Marieke Huisman

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

11 Citations (Scopus)
1 Downloads (Pure)


Recent developments in mobile code and embedded systems have led to an increased interest in open platforms, i.e. platforms which enable different applications to interact in a dynamic environment. However, the flexibility of open platforms presents major difficulties for the (formal) verification of secure interaction between the different applications. To overcome these difficulties, compositional verification techniques are required.

This paper presents a compositional approach to the specification and verification of secure applet interactions. This approach involves a compositional model of the interface behavior of applet interactions, a temporal logic property specification language, and a proof system for proving correctness of property decompositions. The usability of the approach is demonstrated on a realistic smartcard case study.
Original languageEnglish
Title of host publicationFundamental Approaches to Software Engineering, 5th International Conference, FASE 2002, held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2002, Grenoble, France, April 8-12, 2002, Proceedings
EditorsRalf-Detlef Kutsche, Herbert Weber
Number of pages18
ISBN (Electronic)978-3-540-45923-1
ISBN (Print)978-3-540-43353-8
Publication statusPublished - 2002
Externally publishedYes
Event5th International Conference on Fundamental Approaches to Software Engineering, FASE 2002 - Grenoble, France
Duration: 8 Apr 200212 Apr 2002
Conference number: 5

Publication series

NameLecture Notes in Computer Science


Conference5th International Conference on Fundamental Approaches to Software Engineering, FASE 2002
Abbreviated titleFASE 2002


Dive into the research topics of 'Compositional Verification of Secure Applet Interactions'. Together they form a unique fingerprint.

Cite this